#include <string.h>
#include <stdint.h>

#include "klee.h"

// CRC-64-ECMA in https://en.wikipedia.org/wiki/Cyclic_redundancy_check
uint64_t crc64(uint64_t crc, unsigned char *buf, int len)
{
	int k;

	crc = ~crc;
	while (len--)
	{
		crc ^= *buf++;
		for (k = 0; k < 8; k++)
			crc = crc & 1 ? (crc >> 1) ^ 0xC96C5795D7870F42 : crc >> 1;
	}
	return ~crc;
}

int main()
{
#define BUF_SIZE 13

	char buf[BUF_SIZE];

        klee_make_symbolic(buf, sizeof buf, "buf");

        for (int i=0; i<BUF_SIZE; i++)
                klee_assume (buf[i]>='a' && buf[i]<='z');

        klee_assume (crc64 (0, buf, BUF_SIZE)==0x811265a32d6ac13a);
}