== BEGIN: "Makefile" ================
# Makefile for fib2. 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: fib2_driver

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

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

fib2_driver: fib2.o fib2_driver.o
	${CC} ${CCFLAGS} $^ -o $@

clean:
	rm -f *.o

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

#ifndef __fib2__HEADER_INCLUDED__
#define __fib2__HEADER_INCLUDED__

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

/* The boolean type */
typedef bool SBool;

/* The float type */
typedef float SFloat;

/* The double type */
typedef double SDouble;

/* Unsigned bit-vectors */
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 fib2(const SWord64 n);

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

#include <inttypes.h>
#include <stdint.h>
#include <stdbool.h>
#include <math.h>
#include <stdio.h>
#include "fib2.h"

int main(void)
{
  const SWord64 __result = fib2(0x0000000000000014ULL);

  printf("fib2(0x0000000000000014ULL) = 0x%016"PRIx64"ULL\n", __result);

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

#include <inttypes.h>
#include <stdint.h>
#include <stdbool.h>
#include <math.h>
#include "fib2.h"

SWord64 fib2(const SWord64 n)
{
  const SWord64 s0 = n;
  static const SWord64 table0[] = {
      0x0000000000000000ULL, 0x0000000000000001ULL,
      0x0000000000000001ULL, 0x0000000000000002ULL,
      0x0000000000000003ULL, 0x0000000000000005ULL,
      0x0000000000000008ULL, 0x000000000000000dULL,
      0x0000000000000015ULL, 0x0000000000000022ULL,
      0x0000000000000037ULL, 0x0000000000000059ULL,
      0x0000000000000090ULL, 0x00000000000000e9ULL,
      0x0000000000000179ULL, 0x0000000000000262ULL,
      0x00000000000003dbULL, 0x000000000000063dULL,
      0x0000000000000a18ULL, 0x0000000000001055ULL,
      0x0000000000001a6dULL, 0x0000000000002ac2ULL,
      0x000000000000452fULL, 0x0000000000006ff1ULL,
      0x000000000000b520ULL, 0x0000000000012511ULL,
      0x000000000001da31ULL, 0x000000000002ff42ULL,
      0x000000000004d973ULL, 0x000000000007d8b5ULL,
      0x00000000000cb228ULL, 0x0000000000148addULL,
      0x0000000000213d05ULL, 0x000000000035c7e2ULL,
      0x00000000005704e7ULL, 0x00000000008cccc9ULL,
      0x0000000000e3d1b0ULL, 0x0000000001709e79ULL,
      0x0000000002547029ULL, 0x0000000003c50ea2ULL,
      0x0000000006197ecbULL, 0x0000000009de8d6dULL,
      0x000000000ff80c38ULL, 0x0000000019d699a5ULL,
      0x0000000029cea5ddULL, 0x0000000043a53f82ULL,
      0x000000006d73e55fULL, 0x00000000b11924e1ULL,
      0x000000011e8d0a40ULL, 0x00000001cfa62f21ULL,
      0x00000002ee333961ULL, 0x00000004bdd96882ULL,
      0x00000007ac0ca1e3ULL, 0x0000000c69e60a65ULL,
      0x0000001415f2ac48ULL, 0x000000207fd8b6adULL,
      0x0000003495cb62f5ULL, 0x0000005515a419a2ULL,
      0x00000089ab6f7c97ULL, 0x000000dec1139639ULL,
      0x000001686c8312d0ULL, 0x000002472d96a909ULL,
      0x000003af9a19bbd9ULL, 0x000005f6c7b064e2ULL, 0x000009a661ca20bbULL
  };
  const SWord64 s65 = s0 >= 65 ? 0x0000000000000000ULL : table0[s0];

  return s65;
}
== END: "fib2.c" ==================