I am using Z3 for proving the robustness of schedules obtained for real time task systems. When I check this script http://www.cs.ru.nl/~georgeta/script.smt2 I get an unsat response. However, when I use the PROOF_MODE=1 option, the response is sat. What could possibly go wrong in the former case?
2
votes
1 Answers
2
votes
I downloaded your example. The specified logic is incorrect, command:
(set-logic QF_AUFLIA)
This logic specifies that the script will contain only arrays, uninterpreted functions and integer variables, and no quantifiers. However, it contains Real variables. If you remove this command, you will get the correct answer (sat) in both cases. You got a different answer when using PROOF_MODE=1 because some preprocessors in Z3 do not support proof generation, then they are disabled when proof generation is turned on.
That being said, we fixed many bugs in Z3 2.19. The new version 3.0 will be released soon. You can already use the pre-release version we submitted to SMT-COMP.
