/* Automatically generated by SBV. Do not edit! */

#include <stdio.h>
#include <inttypes.h>
#include <stdint.h>
#include <stdbool.h>
#include <string.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;

typedef struct {
  struct {
    SWord32 i0;
    SWord32 i1;
  } input;
  struct {
    SWord32 o0;
    SWord32 o1;
    SWord32 o2;
  } output;
} CTestTestVector;

CTestTestVector CTest[] = {
      {{0xfcbe0fdbUL, 0xd321df04UL}, {0xcfdfeedfUL, 0x299c30d7UL, 0x0f03046cUL}}
    , {{0x7e037b43UL, 0xf66d083bUL}, {0x7470837eUL, 0x87967308UL, 0x042e8071UL}}
    , {{0xce482a70UL, 0x66b7c768UL}, {0x34fff1d8UL, 0x67906308UL, 0xdc5e4d80UL}}
    , {{0xec1eda04UL, 0x465a32a9UL}, {0x32790cadUL, 0xa5c4a75bUL, 0xa45ab4a4UL}}
    , {{0x61f89467UL, 0x00d8fb06UL}, {0x62d18f6dUL, 0x611f9961UL, 0x3c3c776aUL}}
    , {{0x30e2d88cUL, 0x10ea31cdUL}, {0x41cd0a59UL, 0x1ff8a6bfUL, 0x4112341cUL}}
    , {{0x4bf1b3fdUL, 0x2124dc8bUL}, {0x6d169088UL, 0x2accd772UL, 0xdf7e265fUL}}
    , {{0x96885656UL, 0x60a8c5caUL}, {0xf7311c20UL, 0x35df908cUL, 0x9a744ddcUL}}
    , {{0xc2bac856UL, 0xe5a9367cUL}, {0xa863fed2UL, 0xdd1191daUL, 0xe7812da8UL}}
    , {{0x8b10b4f2UL, 0xf010d50fUL}, {0x7b218a01UL, 0x9affdfe3UL, 0x3ba7f42eUL}}
};

int CTestLength = 10;

/* Stub driver showing the test values, replace with code that uses the test vectors. */
int main(void)
{
  int i;
  for(i = 0; i < CTestLength; ++i)
  {
    printf("%*d. 0x%08"PRIx32"UL 0x%08"PRIx32"UL -> 0x%08"PRIx32"UL 0x%08"PRIx32"UL 0x%08"PRIx32"UL\n", 1, i
           , CTest[i].input.i0
           , CTest[i].input.i1
           , CTest[i].output.o0
           , CTest[i].output.o1
           , CTest[i].output.o2);
  }

  return 0;
}