CODEWITHSUNDEEP
z3
Jonah Kagan
Jonah Kagan

Reputation: 457

Asserting definition from z3 model yields unsat

I have a certain set of assertions that I give to z3 which are satisfiable. When I call (check-sat), z3 returns sat. I then call (get-model), and look at the definition for a specific variable, %%P2_*_143. It looks like this:

(define-fun %%P2_*_143 () JS (NUM 2.0))

If I take this definition, turn it into the assertion

(assert (= %%P2_*_143 (NUM 2.0)))

and call (check-sat) again, z3 returns unsat. Furthermore, if I then call (get-unsat-core), z3 returns ().

My understanding is that the model produced by z3 gives a satisfying assignment to all variables, so asserting that assignment should also be satisfiable. Is this incorrect, or do I have a bug elsewhere?

The entire set of assertions is in this gist: https://gist.github.com/2966738. The added assertion is at the very bottom.

I am using Z3 version 3.2, on Mac OS X 10.7.4. I was also able to reproduce this behavior using the online interface at http://rise4fun.com/z3.

Upvotes: 1

Views: 233

Answers (1)

Leonardo de Moura
Leonardo de Moura

Reputation: 21475

A similar bug has been reported a couple of days ago. There is a bug in the model construction in the linear real arithmetic package. The bug has been fixed. Z3 uses infinitesimals to handle strict inequalities, the details are described in the following paper: http://research.microsoft.com/en-us/um/people/leonardo/cav06.pdf

Note that the bug does not affect the soundness of the solver. That is, the sat/unsat answers are correct. However, the model is not. The second query in your example is unsat because the model is incorrect. If you need, I can make a new binary available that fixes this issue. In the meantime, you can workaround the bug, by adding the following commands in your script:

(declare-fun delta () Real)
(assert (< 0.0000001 delta))
(assert (< delta 0.0000002))

Upvotes: 1

Related Questions