Überlauf mit Z3 prüfen

Question

Jul 23, 2013, 11:20 PM

Ich bin neu in Z3 und habe das Online-Python-Tutorial gelesen.

Dann dachte ich, ich könnte das Überlaufverhalten in BitVecs überprüfen.

Ich habe diesen Code geschrieben:

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

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

und ich habe [y = 7, x = 7] erwartet (d. h. wenn die Werte gleich sind, die Nachfolger jedoch nicht, weil x + 1 0 und y + 1 8 sein werden)

Aber Z3 antwortet [y = 0, x = 0].

Was mache ich falsch?

Antworten auf die Frage(2)

Wo installiere ich die von mir geschriebenen Perl-Module?

Ersetzen Sie den String in der Textdatei mit PHP

Produkt-Meta in Bestellpositionstabelle in Bestelldetails anzeigen

Android: Wie geleert man den App-Cache und speichert Benutzerdaten über ADB?

Auf der Suche nach einer Recherche: PNG Sprite vs SVG Sprite vs Icon-Schriften