z3py unconstrainted variables

[DavidPratten]

In SMT-LIB the following is straight forward but how to introduce unconstrained variables to the z3py Solver()?

(declare-const a Int)
(declare-const b Int)
(assert (> a 10))
(check-sat)
(get-model)

returning

sat
(
  (define-fun a () Int
    11)
  (define-fun b () Int
    0)
)

In z3py we have

    a = Int('a')
    b = Int('b')
    s = Solver()
    s.add(a>10)
    s.check()
    print(s.model())

which is not the same because it returns just

[a = 11]

Ideas on how to introduce unconstrained variables into Solver()?

Thanks

David

[DavidPratten]

This is related to this C++ API question. https://stackoverflow.com/questions/24457469/z3-c-api-get-value-of-a-const-with-no-constraints

I'm curious as to the Python solution.

David

[DavidPratten]

Here is the answer:

a = Int('a')
b = Int('b')
s1=Solver()
s1.add(a>10)
s1.check()
# Curious eval() updates the model to force a value for that variable!
s1.model().eval(a,True)
s1.model().eval(b,True)
print(s1.model())

results in

[a = 11, b = 0]