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