CODEWITHSUNDEEP
pythonfunctionz3z3pyforall
Aa17Cc
Aa17Cc

Reputation: 123

Z3 finds model inconsistent with the axioms

When running this code on Python 3.6.7 with the z3-solver module (4.8.0.0), the model returned by z3 seems not valid with the axioms.

f = z3.Function('f', z3.IntSort(), z3.IntSort(), z3.IntSort())
x = z3.Int('x')
s = z3.Solver()
s.add(f(1, 10) == 42)
s.add(z3.ForAll([x], f(2, x) == f(1, x)))
s.check()
m = s.model()
print(m.eval(f(1, 10)))  # print 0
print(m.eval(f(2, 10)))  # print 0

Why didn't we get 42 as we can expect ? Is there a problem with the axioms or the function ?

Upvotes: 2

Views: 85

Answers (1)

alias
alias

Reputation: 30418

Looks like your installation might be busted, as I cannot replicate this:

$ cat a.py
import z3
f = z3.Function('f', z3.IntSort(), z3.IntSort(), z3.IntSort())
x = z3.Int('x')
s = z3.Solver()
s.add(f(1, 10) == 42)
s.add(z3.ForAll([x], f(2, x) == f(1, x)))
print s.sexpr()
s.check()
m = s.model()
print(m.eval(f(1, 10)))  # print 0
print(m.eval(f(2, 10)))  # print 0

$ python a.py
(declare-fun f (Int Int) Int)
(assert (= (f 1 10) 42))
(assert (forall ((x Int)) (= (f 2 x) (f 1 x))))

42
42

Note that I added print s.sexpr() to your code and it nicely printed the generated SMTLib. Do you see the same?

Upvotes: 1

Related Questions