CODEWITHSUNDEEP
z3z3py
user6537
user6537

Reputation: 3

Z3 - how assumptions works

I have the following code in Z3py

    import z3
    x = z3.BitVec('x', 32)
    a = z3.BitVec('a', 32)
    solver=z3.Solver()
    solver.set(unsat_core=True)
    d=z3.Bool('d')
    solver.assert_and_track(x!=a,d)
    solver.add(x==a)
    print solver.check(d)
    print solver.check(z3.Not(d))

I would expect it to print unsat and sat. However it prints always unsat. Should the call solver.check(z3.Not(d)) effectively disable the assertion x!=a?

Upvotes: 0

Views: 1226

Answers (1)

alias
alias

Reputation: 30418

assert_and_track simply associates the answer-literal d with the formula x!=a in your example. Since the context contains x==a and x!=a at the same time, it is unsat. No assumptions will make it satisfiable.

But I do agree that this is very confusing. I think the issue goes back to the fact that assert_and_track is not really intended for what you are trying to do, but merely to make unsat-core-extraction possible. See the discussion here: https://stackoverflow.com/a/14565535/936310

To really achieve what you want, simply assert the implication yourself. That is, use:

solver.add(Implies(d, x!=a))

For instance, the following script:

from z3 import *

x = z3.BitVec('x', 32)
a = z3.BitVec('a', 32)

solver=z3.Solver()
solver.set(unsat_core=True)
d=z3.Bool('d')

solver.add(Implies(d, x!=a))
solver.add(x==a)

print solver.check(d)
print solver.unsat_core()
print solver.check(z3.Not(d))
print solver.model()

produces:

unsat
[d]
sat
[a = 0, d = False, x = 0]

which is what you are trying to achieve, I believe.

Upvotes: 4

Related Questions