Check overflow with Z3

Question

I am new to Z3 and I have been studying the python online tutorial.

Then I thought that I could check the overflow behavior in BitVecs.

I wrote this code:

x = BitVec('x', 3) y = Int('y') solve(BV2Int(x) == y, Not(BV2Int(x + 1) == (y + 1))) 

and I expected [y = 7, x = 7] (that is, when the values ​​are equal and the successors are not because x + 1 will be 0, but y + 1 will be 8)

But Z3 answers [y = 0, x = 0].

What am I doing wrong?

Answer 1

I do not think that you are doing something wrong, it seems that BV2Int is an error:

  x = BitVec('x', 3) prove(x <= 3) prove(BV2Int(x) <= 3) 

Z3py proves the first, but gives a counter example x=0 for the second. It doesn’t sound like that. (The only explanation might be some weird thing in Python, but I don't see how.)

Also note that the model you get will depend on whether the + bit vector is treated as a signed number in Python bindings, which I believe is the case. However, BV2Int may not do this, treating it as an unsigned value. This will further complicate the situation.

In any case, it looks like BV2Int not exactly kosher; I would stay away from him until the official response from the Z3 people.

Answer 2

For others who are concerned about this, this seems to have been resolved at some point. I just repeated this example with the latest version of z3 (a few years after the initial post) and it returns 7.7.