Z3Py Bool variables cast to Int in the model

Question

I am using the python API for Z3 to build a tool for my research. I am having the following issue: I am generating a set of Z3 constraints using a Python script. Since the set might be inconsistent, I am tracking each formula using assert_and_check. For example,

s.assert_and_track(occWrites_1== True, 'p16')

Of course, occWrites is declared to be Boolean:

occWrites_1 = Bool('occWrites_1')

However, in the model, Z3 reports occWrites as an Integer. Why is this happening? Shouldn't the value of occWrites in the model be either True or False?

Answer 1

I can't reproduce the problem you described. In the following example, the value of occWrites_1 is true in the model produced by Z3. It is also available online here. Note that, the value is a Z3 expression, and it is not a Python True value. Perhaps this is the source of the confusion. The method sexpr() pretty prints the value using the Z3 internal format.

from z3 import *

s = Solver()
occWrites_1 = Bool('occWrites_1')
s.assert_and_track(occWrites_1 == True, 'p16')
print s.check()
m = s.model()
print m[occWrites_1]
print m[occWrites_1].sexpr()

The produced output is:

sat
True
true