Nrthugu

I'm experimenting with z3 in python. I have the following model:

(set-option :produce-models true)

(set-logic QF_AUFBV )

(declare-fun a () (Array (_ BitVec 32) (_ BitVec 8) ) )

(declare-fun another () (Array (_ BitVec 32) (_ BitVec 8) ) )

(assert (and  (=  false (=  (_ bv77 32) (concat  (select  a (_ bv3 32) ) (concat  (select  a (_ bv2 32) ) (concat  (select  a (_ bv1 32) ) (select  a (_ bv0 32) ) ) ) ) ) ) (=  false (=  (_ bv12 32) (concat  (select  another (_ bv3 32) ) (concat  (select  another (_ bv2 32) ) (concat  (select  another (_ bv1 32) ) (select  another (_ bv0 32) ) ) ) ) ) ) ) )

I can load it and check that is sat. At this point how can I get an example value for a and another?

import z3

s = z3.Solver()

s.from_file("first.smt")

"""

s

[And(False ==

     (77 == Concat(a[3], Concat(a[2], Concat(a[1], a[0])))),

     False ==

     (12 ==

      Concat(another[3],

             Concat(another[2],

                    Concat(another[1], another[0])))))]

"""

s.check()

"""

sat

"""

m = s.model()

m

[a = Lambda(k!0, 1), another = Lambda(k!0, 1)] 

Thanks

Z3 produces Lambda abstractions for arrays by default; which are useful but hard to see what's going on in a model. I'd recommend turning that off, by putting the following line in your python program:

z3.set_param('model_compress', False)

You should do this right after you import z3.

With this, if you print the model in your program, you get:

>>> m

[a = [3 -> 1, else -> 1],

 another = [1 -> 1, else -> 1],

 k!0 = [3 -> 1, else -> 1],

 k!1 = [1 -> 1, else -> 1]]

which should be more readable. (It's essentially saying both a and another are arrays that map everything to 1; though a bit convoluted.)