== BEGIN: "Makefile" ================
# Makefile for fib1. Automatically generated by SBV. Do not edit!

CC=gcc
CCFLAGS=-Wall -O3 -DNDEBUG -fomit-frame-pointer

all: fib1_driver

fib1.o: fib1.c fib1.h
	${CC} ${CCFLAGS} -c $< -o $@

fib1_driver.o: fib1_driver.c
	${CC} ${CCFLAGS} -c $< -o $@

fib1_driver: fib1.o fib1_driver.o
	${CC} ${CCFLAGS} $^ -o $@

clean:
	rm -f *.o

veryclean: clean
	rm -f fib1_driver
== END: "Makefile" ==================
== BEGIN: "fib1.h" ================
/* Header file for fib1. Automatically generated by SBV. Do not edit! */

#ifndef __fib1__HEADER_INCLUDED__
#define __fib1__HEADER_INCLUDED__

#include <inttypes.h>
#include <stdint.h>

/* Unsigned bit-vectors */
typedef uint8_t  SBool  ;
typedef uint8_t  SWord8 ;
typedef uint16_t SWord16;
typedef uint32_t SWord32;
typedef uint64_t SWord64;

/* Signed bit-vectors */
typedef int8_t  SInt8 ;
typedef int16_t SInt16;
typedef int32_t SInt32;
typedef int64_t SInt64;

/* Entry point prototype: */
SWord32 fib1(const SWord32 n);

#endif /* __fib1__HEADER_INCLUDED__ */
== END: "fib1.h" ==================
== BEGIN: "fib1_driver.c" ================
/* Example driver program for fib1. */
/* Automatically generated by SBV. Edit as you see fit! */

#include <inttypes.h>
#include <stdint.h>
#include <stdio.h>
#include "fib1.h"

int main(void)
{
  const SWord32 __result = fib1(0x0000000cUL);
  
  printf("fib1(0x0000000cUL) = 0x%08"PRIx32"UL\n", __result);

  return 0;
}
== END: "fib1_driver.c" ==================
== BEGIN: "fib1.c" ================
/* File: "fib1.c". Automatically generated by SBV. Do not edit! */

#include <inttypes.h>
#include <stdint.h>
#include "fib1.h"

SWord32 fib1(const SWord32 n)
{
  const SWord32 s0 = n;
  const SBool   s2 = s0 == 0x00000000UL;
  const SBool   s4 = s0 == 0x00000001UL;
  const SBool   s6 = s0 == 0x00000002UL;
  const SBool   s8 = s0 == 0x00000003UL;
  const SBool   s10 = s0 == 0x00000004UL;
  const SBool   s12 = s0 == 0x00000005UL;
  const SBool   s14 = s0 == 0x00000006UL;
  const SBool   s17 = s0 == 0x00000007UL;
  const SBool   s19 = s0 == 0x00000008UL;
  const SBool   s22 = s0 == 0x00000009UL;
  const SBool   s25 = s0 == 0x0000000aUL;
  const SBool   s28 = s0 == 0x0000000bUL;
  const SBool   s31 = s0 == 0x0000000cUL;
  const SBool   s33 = s0 == 0x0000000dUL;
  const SBool   s36 = s0 == 0x0000000eUL;
  const SBool   s39 = s0 == 0x0000000fUL;
  const SBool   s42 = s0 == 0x00000010UL;
  const SBool   s45 = s0 == 0x00000011UL;
  const SBool   s48 = s0 == 0x00000012UL;
  const SBool   s51 = s0 == 0x00000013UL;
  const SBool   s54 = s0 == 0x00000014UL;
  const SBool   s56 = s0 == 0x00000015UL;
  const SBool   s59 = s0 == 0x00000016UL;
  const SBool   s62 = s0 == 0x00000017UL;
  const SBool   s65 = s0 == 0x00000018UL;
  const SBool   s68 = s0 == 0x00000019UL;
  const SBool   s71 = s0 == 0x0000001aUL;
  const SBool   s74 = s0 == 0x0000001bUL;
  const SBool   s77 = s0 == 0x0000001cUL;
  const SBool   s80 = s0 == 0x0000001dUL;
  const SBool   s83 = s0 == 0x0000001eUL;
  const SBool   s86 = s0 == 0x0000001fUL;
  const SBool   s89 = s0 == 0x00000020UL;
  const SBool   s92 = s0 == 0x00000021UL;
  const SBool   s94 = s0 == 0x00000022UL;
  const SBool   s97 = s0 == 0x00000023UL;
  const SBool   s100 = s0 == 0x00000024UL;
  const SBool   s103 = s0 == 0x00000025UL;
  const SBool   s106 = s0 == 0x00000026UL;
  const SBool   s109 = s0 == 0x00000027UL;
  const SBool   s112 = s0 == 0x00000028UL;
  const SBool   s115 = s0 == 0x00000029UL;
  const SBool   s118 = s0 == 0x0000002aUL;
  const SBool   s121 = s0 == 0x0000002bUL;
  const SBool   s124 = s0 == 0x0000002cUL;
  const SBool   s127 = s0 == 0x0000002dUL;
  const SBool   s130 = s0 == 0x0000002eUL;
  const SBool   s133 = s0 == 0x0000002fUL;
  const SBool   s136 = s0 == 0x00000030UL;
  const SBool   s139 = s0 == 0x00000031UL;
  const SBool   s142 = s0 == 0x00000032UL;
  const SBool   s145 = s0 == 0x00000033UL;
  const SBool   s148 = s0 == 0x00000034UL;
  const SBool   s151 = s0 == 0x00000035UL;
  const SBool   s154 = s0 == 0x00000036UL;
  const SBool   s156 = s0 == 0x00000037UL;
  const SBool   s159 = s0 == 0x00000038UL;
  const SBool   s162 = s0 == 0x00000039UL;
  const SBool   s165 = s0 == 0x0000003aUL;
  const SBool   s168 = s0 == 0x0000003bUL;
  const SBool   s171 = s0 == 0x0000003cUL;
  const SBool   s174 = s0 == 0x0000003dUL;
  const SBool   s177 = s0 == 0x0000003eUL;
  const SBool   s180 = s0 == 0x0000003fUL;
  const SWord32 s183 = s180 ? 0xc7b064e2UL : 0x61ca20bbUL;
  const SWord32 s184 = s177 ? 0x9a19bbd9UL : s183;
  const SWord32 s185 = s174 ? 0x2d96a909UL : s184;
  const SWord32 s186 = s171 ? 0x6c8312d0UL : s185;
  const SWord32 s187 = s168 ? 0xc1139639UL : s186;
  const SWord32 s188 = s165 ? 0xab6f7c97UL : s187;
  const SWord32 s189 = s162 ? 0x15a419a2UL : s188;
  const SWord32 s190 = s159 ? 0x95cb62f5UL : s189;
  const SWord32 s191 = s156 ? 0x7fd8b6adUL : s190;
  const SWord32 s192 = s154 ? 0x15f2ac48UL : s191;
  const SWord32 s193 = s151 ? 0x69e60a65UL : s192;
  const SWord32 s194 = s148 ? 0xac0ca1e3UL : s193;
  const SWord32 s195 = s145 ? 0xbdd96882UL : s194;
  const SWord32 s196 = s142 ? 0xee333961UL : s195;
  const SWord32 s197 = s139 ? 0xcfa62f21UL : s196;
  const SWord32 s198 = s136 ? 0x1e8d0a40UL : s197;
  const SWord32 s199 = s133 ? 0xb11924e1UL : s198;
  const SWord32 s200 = s130 ? 0x6d73e55fUL : s199;
  const SWord32 s201 = s127 ? 0x43a53f82UL : s200;
  const SWord32 s202 = s124 ? 0x29cea5ddUL : s201;
  const SWord32 s203 = s121 ? 0x19d699a5UL : s202;
  const SWord32 s204 = s118 ? 0x0ff80c38UL : s203;
  const SWord32 s205 = s115 ? 0x09de8d6dUL : s204;
  const SWord32 s206 = s112 ? 0x06197ecbUL : s205;
  const SWord32 s207 = s109 ? 0x03c50ea2UL : s206;
  const SWord32 s208 = s106 ? 0x02547029UL : s207;
  const SWord32 s209 = s103 ? 0x01709e79UL : s208;
  const SWord32 s210 = s100 ? 0x00e3d1b0UL : s209;
  const SWord32 s211 = s97 ? 0x008cccc9UL : s210;
  const SWord32 s212 = s94 ? 0x005704e7UL : s211;
  const SWord32 s213 = s92 ? 0x0035c7e2UL : s212;
  const SWord32 s214 = s89 ? 0x00213d05UL : s213;
  const SWord32 s215 = s86 ? 0x00148addUL : s214;
  const SWord32 s216 = s83 ? 0x000cb228UL : s215;
  const SWord32 s217 = s80 ? 0x0007d8b5UL : s216;
  const SWord32 s218 = s77 ? 0x0004d973UL : s217;
  const SWord32 s219 = s74 ? 0x0002ff42UL : s218;
  const SWord32 s220 = s71 ? 0x0001da31UL : s219;
  const SWord32 s221 = s68 ? 0x00012511UL : s220;
  const SWord32 s222 = s65 ? 0x0000b520UL : s221;
  const SWord32 s223 = s62 ? 0x00006ff1UL : s222;
  const SWord32 s224 = s59 ? 0x0000452fUL : s223;
  const SWord32 s225 = s56 ? 0x00002ac2UL : s224;
  const SWord32 s226 = s54 ? 0x00001a6dUL : s225;
  const SWord32 s227 = s51 ? 0x00001055UL : s226;
  const SWord32 s228 = s48 ? 0x00000a18UL : s227;
  const SWord32 s229 = s45 ? 0x0000063dUL : s228;
  const SWord32 s230 = s42 ? 0x000003dbUL : s229;
  const SWord32 s231 = s39 ? 0x00000262UL : s230;
  const SWord32 s232 = s36 ? 0x00000179UL : s231;
  const SWord32 s233 = s33 ? 0x000000e9UL : s232;
  const SWord32 s234 = s31 ? 0x00000090UL : s233;
  const SWord32 s235 = s28 ? 0x00000059UL : s234;
  const SWord32 s236 = s25 ? 0x00000037UL : s235;
  const SWord32 s237 = s22 ? 0x00000022UL : s236;
  const SWord32 s238 = s19 ? 0x00000015UL : s237;
  const SWord32 s239 = s17 ? 0x0000000dUL : s238;
  const SWord32 s240 = s14 ? 0x00000008UL : s239;
  const SWord32 s241 = s12 ? 0x00000005UL : s240;
  const SWord32 s242 = s10 ? 0x00000003UL : s241;
  const SWord32 s243 = s8 ? 0x00000002UL : s242;
  const SWord32 s244 = s6 ? 0x00000001UL : s243;
  const SWord32 s245 = s4 ? 0x00000001UL : s244;
  const SWord32 s246 = s2 ? 0x00000000UL : s245;
  
  return s246;
}
== END: "fib1.c" ==================