Verifique o estouro com Z3
Eu sou novo no Z3 e estava verificando o tutorial online do python.
Então eu pensei que poderia verificar o comportamento de estouro em BitVecs.
Eu escrevi este código:
x = BitVec('x', 3)
y = Int('y')
solve(BV2Int(x) == y, Not(BV2Int(x + 1) == (y + 1)))
e eu estava esperando [y = 7, x = 7] (ou seja, quando os valores são iguais, mas os sucessores não são porque x + 1 será 0 e y + 1 será 8)
Mas Z3 responde [y = 0, x = 0].
O que estou fazendo de errado?