/* 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[] = {
      {{0x96962508UL, 0xf3dc6f98UL}, {0x8a7294a0UL, 0xa2b9b570UL, 0xee1474c0UL}}
    , {{0xb4538396UL, 0x8f338d9cUL}, {0x43871132UL, 0x251ff5faUL, 0xe33fcd68UL}}
    , {{0xe017f69fUL, 0xe7510cb7UL}, {0xc7690356UL, 0xf8c6e9e8UL, 0xd1ffbfa9UL}}
    , {{0x9847fd68UL, 0x1e671b39UL}, {0xb6af18a1UL, 0x79e0e22fUL, 0xa4996428UL}}
    , {{0xb9a2eb19UL, 0x6eedc674UL}, {0x2890b18dUL, 0x4ab524a5UL, 0x83ccdd54UL}}
    , {{0x4f576647UL, 0x0058226eUL}, {0x4faf88b5UL, 0x4eff43d9UL, 0xdb8b6082UL}}
    , {{0x24ff2cd8UL, 0x466eb767UL}, {0x6b6de43fUL, 0xde907571UL, 0xa08972e8UL}}
    , {{0x08363d14UL, 0xdcfe4253UL}, {0xe5347f67UL, 0x2b37fac1UL, 0x6f2cf57cUL}}
    , {{0xeefac975UL, 0x45b9cecdUL}, {0x34b49842UL, 0xa940faa8UL, 0x4b7c78b1UL}}
    , {{0x2ee34d81UL, 0xdabd0994UL}, {0x09a05715UL, 0x542643edUL, 0x2b5f5794UL}}
};

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;
}