Project

General

Profile

Bug #4077

Z3 solver produces contradicting solution states with the Java API and the smtlib interface

Added by Alexander Diewald about 1 month ago. Updated 17 days ago.

Status:
Closed
Priority:
Normal
Assignee:
-
Category:
SMT
Start date:
10/22/2020
Due date:
% Done:

0%

Estimated time:

Description

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 a sat/unsat return value.

History

#1 Updated by Johannes Eder 17 days ago

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

MR: https://git.fortiss.org/af3/af3/-/merge_requests/386

Testing:
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.

#4 Updated by Johannes Eder 17 days ago

  • Status changed from Feedback to Resolved

Great that this could be solved so fast!

FYI, I was using Z3 4.5.0.

Reviewed and merged.

#5 Updated by Johannes Eder 17 days ago

  • Status changed from Resolved to Closed
  • Assignee deleted (Johannes Eder)

Also available in: Atom PDF