Eldarica 2.0.4-heap

Identical to Eldarica 2.0.4 with additional support for the theory of heap.

/heap-theory-examples/ folder contains some examples given in SMT-LIB, translated from C using TriCera except one hand-written example: motivating-example.smt2.

The examples can either be ran in batch mode using

/heap-theory-examples/runexamples

or by passing the files as an argument to Eldarica using one of the methods shown below:

./eld heap-theory-examples/typecastSafe-001.smt2
[...]
sat

or

java -jar target/scala-2.11/Eldarica-assembly-2.0.4-heap.jar heap-theory-examples/motivating-example.smt2
[...]
sat

-cex parameter can also be provided in order to display the counterexamples when the result is unsat. -ssol parameter displays the solution when the result is sat; however, the displayed solutions might currently be difficult to read.

Note that only .smt2 files should be passed to Eldarica. The .c files under /heap-theory-examples/ are provided only for reference in order to show where the encodings came from, and should not be directly passed to Eldarica. This will result in an error as Eldarica does not have support for C programs with heap interactions (see TriCera for this, but note that it is also quite experimental at this point).