Controlla overflow con Z3

Question

Sono nuovo di Z3 e stavo controllando il tutorial online su Python.

Quindi ho pensato di poter controllare il comportamento di overflow in BitVecs.

Ho scritto questo codice:

x = BitVec('x', 3) 
y = Int('y') 

solve(BV2Int(x) == y, Not(BV2Int(x + 1) == (y + 1))) 

e mi aspettavo [y = 7, x = 7] (cioè quando i valori sono uguali ma successori non sono perché x + 1 sarà 0 e y + 1 sarà 8)

Ma Z3 risponde [y = 0, x = 0].

Cosa sto sbagliando?

Answer 1

Non credo che stai facendo qualcosa di sbagliato, sembra BV2Int è buggy:

x = BitVec('x', 3) 
prove(x <= 3) 
prove(BV2Int(x) <= 3) 

Z3py dimostra il primo, ma dà il contro-esempio x=0 per il secondo. Non sembra giusto. (L'unica spiegazione potrebbe essere qualche cosa Python strano, ma non vedo come.)

Si noti inoltre che il modello si ottiene dipenderà se + tratta il vettore di bit come un numero firmato nei binding Python, che credo sia il caso. Tuttavia, BV2Int potrebbe non farlo, trattandolo come un valore senza segno. Ciò complicherebbe ulteriormente le cose.

In ogni caso, l'aspetto BV2Int non è abbastanza kosher; Me ne starò lontano finché non ci sarà una risposta ufficiale da parte degli Z3.

Answer 2

Per gli altri che sono preoccupati di questo, questo sembra essere stato risolto ad un certo punto. Ho appena rieseguito questo esempio con l'ultima versione di z3 (alcuni anni dopo il post iniziale) e restituisce 7,7.