Z3 solver produces contradicting solution states with the Java API and the smtlib interface
Problem Description
When launching the DSE of the attached AF3 file with the two present
RuleSets selected, the solver reports that the problem is unsolvable.
The correctness of the UI message has been verified by debugging the
returned state from the Z3 solver object.
However, if the problem is dumped as a SMTLib file and passed to z3
through the command line, the problem is reported as being solvable.
There is no difference in this result if the SMTLib dump is generated by
the debug flag DSE_DEBUG_VERBOSE=true or the via the CLI. The two
generated files were also diffed against each other and they are
de-facto equivalent (besides the need to move two statement blocks,
which is irrelevant).
NB:
- The same Z3 version was used on the command line as we use in AF3. Updating the command-line z3 did not change the behavior.
- CVC4 reports the same result as the Z3 command line.
- For testing a dumped file from the DSE flag, you have to add the
statement
(check-sat)
at the beginning of the dumped file to obtain asat/unsat
return value.
(from redmine: issue id 4077, created on 2020-10-22, closed on 2020-11-10)