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?
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.
For others who are concerned by this, this appears to have been solved at some point. I just re-ran this example with the latest version of z3 (a few years after initial post), and it does return 7,7.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With