Comprobar desbordamiento con Z3
Soy nuevo en Z3 y estaba revisando el tutorial de Python en línea.
Entonces pensé que podía comprobar el comportamiento de desbordamiento en BitVecs.
Escribí este código:
x = BitVec('x', 3)
y = Int('y')
solve(BV2Int(x) == y, Not(BV2Int(x + 1) == (y + 1)))
y esperaba [y = 7, x = 7] (es decir, cuando los valores son iguales pero los sucesores no lo son porque x + 1 será 0 e y + 1 será 8)
Pero Z3 responde [y = 0, x = 0].
¿Qué estoy haciendo mal?