Baier D.
Baier D.
An example would be the query `(assert var)`, with missing variable declaration.
Fixed in the parser update of 0.4.0. It now throws a proper `IllegalArgumentException`.
I asked around for question 1: I've asked the MathSAT5 devs (but he is currently not available till August, i guess vacation). I also created a [issue for Z3](https://github.com/Z3Prover/z3/issues/6826). And...
Z3 might support the feature requests for Q1. We @lembergerth should test this.
I've already added a possible implementation in a [branch](https://github.com/sosy-lab/java-smt/tree/322-feature-request-clone-proverenvironment-with-stack). I've added 2 methods to the context to copy a prover with and without interpolation enabled. The context was chosen by...
On a broader note: we should have tests for this and some other basic cases. @rsoegtrop can you take a look at this issue and add some tests that cover...
Would it be possible to merge this? I am effected by this issue on my Windows machine.
@kfriedberger @PhilippWendler we have 3 warnings from Spotbugs that are empty in this PR. Do you happen to know the reason for this or how to find out?
Thanks for the help! I guess we are currently not synced to the java project template of SoSy. I'm gonna update it this week!
Results of running this branch in CPAchecker using Newton refinement in Predicate Abstraction look good and perform on-par and sometimes better than native QE. (I can't upload for some reason)