README-z3

crest-z3: CREST extension that supports non-linear arithmetic.

Heechul Yun <heechul@illinois.edu>

Original CREST does not support non-linear arithmetic operations
as well as division and mod operators. One example of such program
is as follows.

#include <crest.h>
#include <stdio.h>

int main(int argc, char *argv[])
{
	int x, y;

	CREST_int(x);
	CREST_int(y);

	if ( (y*y)%50 == x) {
		if (x>y+10) {
			printf("GOAL x=%d, y=%d\n", x, y);
		}
	}
	return 0;
}


In original version, CREST will fail to find "GOAL" execution path
because of y*y is not linear arithmetic and % is not supported operator.

This extension, crest-z3, supports this example. More examples that
can be explored by crest-z3 can be found in test/prj_test*.c

All the usuage is the same as original CREST as all the changes are
internal and not visible to users.


SETUP
=====

CREST-z3 depends on Z3, an SMT solver tool and library available at
http://research.microsoft.com/en-us/um/redmond/projects/z3/download.html

CREST-z3 includes 32bit binary version of z3 4.0 installation under z3/
directory. To use different version of z3, you can simply replace the
directory.

Other setup is the same as original CREST. So simply "make" under src/
directory.