Z3 gives no or wrong solution when there are a right solution

Question

I am writing a problem with BitVecs as I have to do bit-blasting later. I have a sum constraint. To avoid overflow solutions, e.g. x0 = BitVec('x0',2) and x1 = BitVec('x1',2), x0+x1==2 gives the solution 3 and 3 as 3+3%4=2, I add in contraints saying they can be no more than 2.

x0 = BitVec('x0',2)
x1 = BitVec('x1',2)
g = Goal()
g.add(x0 + x1 == 2)
g.add(x0 <= 2)
g.add(x1 <= 2)

This gives no solution

I have also tried the following

x0 = BitVec('x0',3)
x1 = BitVec('x1',3)
g = Goal()
g.add(x0 + x1 == 2)
g.add(x0 <= 2)
g.add(x1 <= 2)

Which gives the wrong solution x0 = 6, x1 = 4

Answer 1

Your first attempt is unsat, because of the domain of 2-bit bit-vectors can only encode -2, -1, 0, and 1:

  Bits|Value
  ----+------
    00| 0
    01| 1
    10|-2
    11|-1

In z3py <= does a signed comparison. So, when you say x0 <= 2, that right hand-side 2 is actually -2 (see the bit pattern above.) So, you restricted the values to be <= -2, and there's only one such value in the domain, i.e., -2. And -2 + -2 = 0 when you do modular arithmetic (modulo 4), i.e., there's no value that satisfies your requirement that x0 + x1 should be 2. So, you get unsat as answer.

Your second try is similar. In this case you have 3-bits, so the valid values are -4, -3, -2, -1, 0, 1, 2, 3. (You should write down the bit-patterns corresponding to this to convince yourself.) I'll let you work-out the details. Note that, unlike what you reported, I see:

[x1 = 2, x0 = 0]

as the answer, and that actually is the correct answer in this case. I'm not sure why you're seeing x0=6, x1=4; maybe you had some other code running.

Remember that in SMTLib, bit-vectors are unsigned, but operations are. In particular, comparisons. If your intention was to simply use unsigned bit-vectors (i.e., a 2-bit vector representing 0,1,2, and 3), then you should use the correct comparison operator:

from z3 import *

x0 = BitVec('x0',2)
x1 = BitVec('x1',2)

s = Solver()
s.add(x0 + x1 == 2)
s.add(ULE(x0, 2))
s.add(ULE(x1, 2))

if s.check() == sat:
  print(s.model())
else:
  print("No solution")

This prints:

[x1 = 0, x0 = 2]

which is probably what you were going for. Note the use of the correct comparison operator ULE, which does unsigned-less-than-or-equal, instead of <=, which does a signed comparison.