gistfile1.txt

// cbmc cmbc.c ref.c jepler.c -DBUFSIZE=1 -DCMBC
#include "nibble.h"
#include <assert.h>
#include <inttypes.h>
#include <string.h>

uint64_t nondet_u64(); 
void main() {
    setup_jepler();
    uint64_t ref[BUFSIZE], res[BUFSIZE];
    int i;
    for(i=0; i<BUFSIZE; i++) ref[i] = res[i] = nondet_u64();
    nibble_sort_ref(ref);
    nibble_sort_jepler(res);
    for(i=0; i<BUFSIZE; i++) assert(ref[i] == res[i]);
}