Skolemizer for AE-formulas in LIA/LRA based on the SeaHorn verification framework and the Z3 SMT solver. This is the main computational engine used in the Incremental Model Checking (LPAR'15, CAV'16) and in the Program Synthesis from Assume-Guarantee contracts (preprint).
cd aeval ; mkdir build ; cd buildcmake ../maketo build dependencies (Z3 and LLVM)maketo build AE-VAL
The binary of AE-VAL can be found in build/tools/aeval/
To check equivalence between two programs, run
equiv <program1> <program2> [unroll1 unroll2]