Z3 solver produces contradicting solution states with the Java API and the smtlib interface
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).
- 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 a
#1 Updated by Johannes Eder 17 days ago
- File DSE_Generated_TestCase_1_2020-10-22-102342_console_output_z3 DSE_Generated_TestCase_1_2020-10-22-102342_console_output_z3 added
- Status changed from New to Feedback
- Assignee changed from Johannes Eder to Alexander Diewald
Comment: the (check-sat) statement must always be at the end of the file. Can be seen as a script where you tell the programm in the end to check satisfiability.
Both SMT2 Files produce a SAT on my machine, however, the solutions are not valid because loads of errors are produced (see attached file). It is unclear to me why Z3 then still says SAT. So I would guess that the SMTlib dump is somehow erroneous.
#2 Updated by Alexander Diewald 17 days ago
- Assignee changed from Alexander Diewald to Johannes Eder
Thanks a lot for the hint about moving the (check-sat) statement. That did the trick. On my machine, the result obtained by the command-line tools (z3 and cvc4) now agree with AF3.
The errors you are observing might be related to the z3 version you are using. From my little experience: I observed similar messages when I used some older Z3 version.
I'd propose to fix the smt-lib file creation in the CMD line interface such that the (check-sat) statement is placed in the correct location.
#3 Updated by Alexander Diewald 17 days ago
1. Place the AF3 file in your runtime workspace.
2. Add "--dump-smtlib DSE_Generated_TestCase_1/Generated_DSE_1/Deployment" (without quotes) to the arguments tab of your launch cfg.
3. Verify that the generated SMTLib file has the "(set-logic ALL)" at the beginning, whereas the "(check-sat)" statement is placed at the end of the file.