Sprawdź przepełnienie za pomocą Z3
Jestem nowym użytkownikiem Z3 i sprawdzałem samouczek python online.
Wtedy pomyślałem, że mogę sprawdzić zachowanie przepełnienia w BitVecs.
Napisałem ten kod:
x = BitVec('x', 3)
y = Int('y')
solve(BV2Int(x) == y, Not(BV2Int(x + 1) == (y + 1)))
i spodziewałem się [y = 7, x = 7] (tj. gdy wartości są równe, ale następcy nie są, ponieważ x + 1 będzie równe 0, a y + 1 będzie 8)
Ale Z3 odpowiada [y = 0, x = 0].
Co ja robię źle?