CODEWITHSUNDEEP
pythonz3
user311703
user311703

Reputation: 1133

Z3: why this array theory usage returns Unsat?

i am trying to model memory access with Array theory. i have a simple code like below (Z3 python)

Mem = Array('Mem', BitVecSort(32), BitVecSort(32))

F = True
tmp = BitVec('tmp', 32)
tmp3 = BitVec('tmp3', 32)
F = And(F, tmp3 == Select(Mem, tmp))
tmp4 = BitVec('tmp4', 32)
F = And(F, tmp4 == (tmp3 - 1))
F = And(F, Mem == Store(Mem, tmp, tmp4))

s = Solver()
s.add(F)
print s.check()

i want the 'Sat' result, but this script returns 'Unsat'.

i think this is because i read out from Mem, then write different value to it. is this really the reason i get 'Unsat'?

if so, how can i model memory access using Array theory? how to fix the above script, so it returns 'Sat'?

thanks so much.

Upvotes: 0

Views: 223

Answers (1)

alias
alias

Reputation: 30485

Why do you expect this query to return Sat?

Your query comes down to asking Z3 to find values for Mem and t such that Mem[t] = Mem[t] - 1, which is clearly not true of any value of Mem and t you can think of; so Z3 responds Unsat.

If you can tell us what property you're trying to satisfy, we can help you formulate it correctly.

Upvotes: 1

Related Questions