fib1.gold

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

# include any user-defined .mk file in the current directory.
-include *.mk

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: */
SWord64 fib1(const SWord64 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 SWord64 __result = fib1(0x000000000000000cULL);
  
  printf("fib1(0x000000000000000cULL) = 0x%016"PRIx64"ULL\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"

SWord64 fib1(const SWord64 n)
{
  const SWord64 s0 = n;
  const SBool   s2 = s0 == 0x0000000000000000ULL;
  const SBool   s4 = s0 == 0x0000000000000001ULL;
  const SBool   s6 = s0 == 0x0000000000000002ULL;
  const SBool   s8 = s0 == 0x0000000000000003ULL;
  const SBool   s10 = s0 == 0x0000000000000004ULL;
  const SBool   s12 = s0 == 0x0000000000000005ULL;
  const SBool   s14 = s0 == 0x0000000000000006ULL;
  const SBool   s17 = s0 == 0x0000000000000007ULL;
  const SBool   s19 = s0 == 0x0000000000000008ULL;
  const SBool   s22 = s0 == 0x0000000000000009ULL;
  const SBool   s25 = s0 == 0x000000000000000aULL;
  const SBool   s28 = s0 == 0x000000000000000bULL;
  const SBool   s31 = s0 == 0x000000000000000cULL;
  const SBool   s33 = s0 == 0x000000000000000dULL;
  const SBool   s36 = s0 == 0x000000000000000eULL;
  const SBool   s39 = s0 == 0x000000000000000fULL;
  const SBool   s42 = s0 == 0x0000000000000010ULL;
  const SBool   s45 = s0 == 0x0000000000000011ULL;
  const SBool   s48 = s0 == 0x0000000000000012ULL;
  const SBool   s51 = s0 == 0x0000000000000013ULL;
  const SBool   s54 = s0 == 0x0000000000000014ULL;
  const SBool   s56 = s0 == 0x0000000000000015ULL;
  const SBool   s59 = s0 == 0x0000000000000016ULL;
  const SBool   s62 = s0 == 0x0000000000000017ULL;
  const SBool   s65 = s0 == 0x0000000000000018ULL;
  const SBool   s68 = s0 == 0x0000000000000019ULL;
  const SBool   s71 = s0 == 0x000000000000001aULL;
  const SBool   s74 = s0 == 0x000000000000001bULL;
  const SBool   s77 = s0 == 0x000000000000001cULL;
  const SBool   s80 = s0 == 0x000000000000001dULL;
  const SBool   s83 = s0 == 0x000000000000001eULL;
  const SBool   s86 = s0 == 0x000000000000001fULL;
  const SBool   s89 = s0 == 0x0000000000000020ULL;
  const SBool   s92 = s0 == 0x0000000000000021ULL;
  const SBool   s94 = s0 == 0x0000000000000022ULL;
  const SBool   s97 = s0 == 0x0000000000000023ULL;
  const SBool   s100 = s0 == 0x0000000000000024ULL;
  const SBool   s103 = s0 == 0x0000000000000025ULL;
  const SBool   s106 = s0 == 0x0000000000000026ULL;
  const SBool   s109 = s0 == 0x0000000000000027ULL;
  const SBool   s112 = s0 == 0x0000000000000028ULL;
  const SBool   s115 = s0 == 0x0000000000000029ULL;
  const SBool   s118 = s0 == 0x000000000000002aULL;
  const SBool   s121 = s0 == 0x000000000000002bULL;
  const SBool   s124 = s0 == 0x000000000000002cULL;
  const SBool   s127 = s0 == 0x000000000000002dULL;
  const SBool   s130 = s0 == 0x000000000000002eULL;
  const SBool   s133 = s0 == 0x000000000000002fULL;
  const SBool   s136 = s0 == 0x0000000000000030ULL;
  const SBool   s139 = s0 == 0x0000000000000031ULL;
  const SBool   s142 = s0 == 0x0000000000000032ULL;
  const SBool   s145 = s0 == 0x0000000000000033ULL;
  const SBool   s148 = s0 == 0x0000000000000034ULL;
  const SBool   s151 = s0 == 0x0000000000000035ULL;
  const SBool   s154 = s0 == 0x0000000000000036ULL;
  const SBool   s156 = s0 == 0x0000000000000037ULL;
  const SBool   s159 = s0 == 0x0000000000000038ULL;
  const SBool   s162 = s0 == 0x0000000000000039ULL;
  const SBool   s165 = s0 == 0x000000000000003aULL;
  const SBool   s168 = s0 == 0x000000000000003bULL;
  const SBool   s171 = s0 == 0x000000000000003cULL;
  const SBool   s174 = s0 == 0x000000000000003dULL;
  const SBool   s177 = s0 == 0x000000000000003eULL;
  const SBool   s180 = s0 == 0x000000000000003fULL;
  const SWord64 s183 = s180 ? 0x000005f6c7b064e2ULL : 0x000009a661ca20bbULL;
  const SWord64 s184 = s177 ? 0x000003af9a19bbd9ULL : s183;
  const SWord64 s185 = s174 ? 0x000002472d96a909ULL : s184;
  const SWord64 s186 = s171 ? 0x000001686c8312d0ULL : s185;
  const SWord64 s187 = s168 ? 0x000000dec1139639ULL : s186;
  const SWord64 s188 = s165 ? 0x00000089ab6f7c97ULL : s187;
  const SWord64 s189 = s162 ? 0x0000005515a419a2ULL : s188;
  const SWord64 s190 = s159 ? 0x0000003495cb62f5ULL : s189;
  const SWord64 s191 = s156 ? 0x000000207fd8b6adULL : s190;
  const SWord64 s192 = s154 ? 0x0000001415f2ac48ULL : s191;
  const SWord64 s193 = s151 ? 0x0000000c69e60a65ULL : s192;
  const SWord64 s194 = s148 ? 0x00000007ac0ca1e3ULL : s193;
  const SWord64 s195 = s145 ? 0x00000004bdd96882ULL : s194;
  const SWord64 s196 = s142 ? 0x00000002ee333961ULL : s195;
  const SWord64 s197 = s139 ? 0x00000001cfa62f21ULL : s196;
  const SWord64 s198 = s136 ? 0x000000011e8d0a40ULL : s197;
  const SWord64 s199 = s133 ? 0x00000000b11924e1ULL : s198;
  const SWord64 s200 = s130 ? 0x000000006d73e55fULL : s199;
  const SWord64 s201 = s127 ? 0x0000000043a53f82ULL : s200;
  const SWord64 s202 = s124 ? 0x0000000029cea5ddULL : s201;
  const SWord64 s203 = s121 ? 0x0000000019d699a5ULL : s202;
  const SWord64 s204 = s118 ? 0x000000000ff80c38ULL : s203;
  const SWord64 s205 = s115 ? 0x0000000009de8d6dULL : s204;
  const SWord64 s206 = s112 ? 0x0000000006197ecbULL : s205;
  const SWord64 s207 = s109 ? 0x0000000003c50ea2ULL : s206;
  const SWord64 s208 = s106 ? 0x0000000002547029ULL : s207;
  const SWord64 s209 = s103 ? 0x0000000001709e79ULL : s208;
  const SWord64 s210 = s100 ? 0x0000000000e3d1b0ULL : s209;
  const SWord64 s211 = s97 ? 0x00000000008cccc9ULL : s210;
  const SWord64 s212 = s94 ? 0x00000000005704e7ULL : s211;
  const SWord64 s213 = s92 ? 0x000000000035c7e2ULL : s212;
  const SWord64 s214 = s89 ? 0x0000000000213d05ULL : s213;
  const SWord64 s215 = s86 ? 0x0000000000148addULL : s214;
  const SWord64 s216 = s83 ? 0x00000000000cb228ULL : s215;
  const SWord64 s217 = s80 ? 0x000000000007d8b5ULL : s216;
  const SWord64 s218 = s77 ? 0x000000000004d973ULL : s217;
  const SWord64 s219 = s74 ? 0x000000000002ff42ULL : s218;
  const SWord64 s220 = s71 ? 0x000000000001da31ULL : s219;
  const SWord64 s221 = s68 ? 0x0000000000012511ULL : s220;
  const SWord64 s222 = s65 ? 0x000000000000b520ULL : s221;
  const SWord64 s223 = s62 ? 0x0000000000006ff1ULL : s222;
  const SWord64 s224 = s59 ? 0x000000000000452fULL : s223;
  const SWord64 s225 = s56 ? 0x0000000000002ac2ULL : s224;
  const SWord64 s226 = s54 ? 0x0000000000001a6dULL : s225;
  const SWord64 s227 = s51 ? 0x0000000000001055ULL : s226;
  const SWord64 s228 = s48 ? 0x0000000000000a18ULL : s227;
  const SWord64 s229 = s45 ? 0x000000000000063dULL : s228;
  const SWord64 s230 = s42 ? 0x00000000000003dbULL : s229;
  const SWord64 s231 = s39 ? 0x0000000000000262ULL : s230;
  const SWord64 s232 = s36 ? 0x0000000000000179ULL : s231;
  const SWord64 s233 = s33 ? 0x00000000000000e9ULL : s232;
  const SWord64 s234 = s31 ? 0x0000000000000090ULL : s233;
  const SWord64 s235 = s28 ? 0x0000000000000059ULL : s234;
  const SWord64 s236 = s25 ? 0x0000000000000037ULL : s235;
  const SWord64 s237 = s22 ? 0x0000000000000022ULL : s236;
  const SWord64 s238 = s19 ? 0x0000000000000015ULL : s237;
  const SWord64 s239 = s17 ? 0x000000000000000dULL : s238;
  const SWord64 s240 = s14 ? 0x0000000000000008ULL : s239;
  const SWord64 s241 = s12 ? 0x0000000000000005ULL : s240;
  const SWord64 s242 = s10 ? 0x0000000000000003ULL : s241;
  const SWord64 s243 = s8 ? 0x0000000000000002ULL : s242;
  const SWord64 s244 = s6 ? 0x0000000000000001ULL : s243;
  const SWord64 s245 = s4 ? 0x0000000000000001ULL : s244;
  const SWord64 s246 = s2 ? 0x0000000000000000ULL : s245;
  
  return s246;
}
== END: "fib1.c" ==================