With some external solvers (like Boolector), the memory for the countermodels comes back as a big lambda term consisting of a bunch of if-then-else cases for each address.
Obviously, this is very unreadable for the user. Not only that, WP will fail to construct the refuted goals when the memory model is in this form.
This PR fixes the way we parse the output from the external solver, turning it into a sequence of array stores.
With some external solvers (like Boolector), the memory for the countermodels comes back as a big lambda term consisting of a bunch of if-then-else cases for each address.
Obviously, this is very unreadable for the user. Not only that, WP will fail to construct the refuted goals when the memory model is in this form.
This PR fixes the way we parse the output from the external solver, turning it into a sequence of array stores.