z3py - Check overflow with Z3

Question

I'm new to Z3 and I was checking the online python tutorial.

Then I thought I could check 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 was expecting [y = 7, x = 7] (i.e. when values are equal but successors are not because x + 1 will be 0 and y + 1 will be 8)

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

What am I doing wrong?

Answer 1

I don't think you're doing anything wrong, looks like BV2Int is buggy:

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

Z3py proves the first one, but gives the counter-example x=0 for the second. That doesn't sound right. (The only explanation might be some weird Python thing, but I don't see how.)

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

In any case, looks like BV2Int is not quite kosher; I'd stay away from it until there's an official answer from the Z3 folks.