BitVec usage question.

Jan 16, 2015 at 7:58 AM
In [1]: from z3 import *

In [2]: a = BitVec("a", 8)

In [3]: b = BitVec("b", 16)

In [4]: solve(a + 1 = 100)

In [5]: solve(a + 1 == 100)
[a = 99]

In [6]: solve(a + 1 == 1000)
[a = 231] // WTF?

In [7]: solve(b + 1 == 1000)
[b = 999]

in line number 6, I want to get a message 'unsat' but i can't.

what is the matter??
Coordinator
Jan 16, 2015 at 5:11 PM
The `solve' command will only consider all the arguments, but not the ones in previous or subsequent calls to solve(). For this purpose, we either need to provide all the constraints to a single call to solve(), or set up a solver object that tracks the assertions. For example:
from z3 import * 
a = BitVec("a", 8) 
b = BitVec("b", 16) 

solve(a + 1 == 100, a + 1 == 1000) # reports "no solution"

s = Solver()
s.add(a + 1 == 100) 
s.add(a + 1 == 1000) 
print s.check() # reports "unsat"