Experiments with prophecy variables for symbolic model checking.
The code is a modification of ic3ia from https://es-static.fbk.eu/people/griggio/ic3ia/ic3ia.tar.gz, which uses mathsat bindings downloaded from https://es-static.fbk.eu/tools/nb/
We are adding an abstraction refinement loop for solving transition systems containing arrays.