Skip to content

Commit 8a30152

Browse files
committed
tests/specs/lemmas/lemmas-spec.k: add failing test of address reprojection
1 parent 1779028 commit 8a30152

File tree

1 file changed

+4
-0
lines changed

1 file changed

+4
-0
lines changed

tests/specs/functional/lemmas-spec.k

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -66,6 +66,10 @@ module LEMMAS-SPEC
6666
=> doneLemma(368263281805664599098893944405654396525700029268) ... </k>
6767
requires #rangeUInt(256, X)
6868

69+
claim [address-insertion-1]: <k> runLemma(368263281805664599098893944405654396525700029268 |Int (notMaxUInt160 &Int #lookup(ACCT_STORAGE:Map, 8)))
70+
=> doneLemma(368263281805664599098893944405654396525700029268) ... </k>
71+
requires #lookup(ACCT_STORAGE, 8) <Int pow160
72+
6973
// Buffer write simplifications
7074
// ----------------------------
7175

0 commit comments

Comments
 (0)