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?

Accepted Answer

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.

Check overflow with Z3

Solution

Problem