Skip to content

Commit

Permalink
Update dependency: deps/z3 (#925)
Browse files Browse the repository at this point in the history
* deps/z3: Set Version 4.13.4

* Replace `/Int` with `divInt` in `sumToN`

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: palinatolmach <[email protected]>
  • Loading branch information
3 people authored Jan 14, 2025
1 parent 1c2c78f commit 3603b67
Show file tree
Hide file tree
Showing 2 changed files with 3 additions and 3 deletions.
2 changes: 1 addition & 1 deletion deps/z3
Original file line number Diff line number Diff line change
@@ -1 +1 @@
4.13.0
4.13.4
4 changes: 2 additions & 2 deletions src/tests/integration/test-data/lemmas.k
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,7 @@ module SUM-TO-N-INVARIANT
JUMPDESTS
</jumpDests>
<wordStack>
(S => (S +Int ((N *Int (N +Int 1)) /Int 2)))
(S => (S +Int ((N *Int (N +Int 1)) divInt 2)))
: 0
: (N => 0)
: 459
Expand All @@ -55,7 +55,7 @@ module SUM-TO-N-INVARIANT
</kevm>

requires 0 <Int N
andBool #rangeUInt(256, S +Int ((N *Int (N +Int 1)) /Int 2))
andBool #rangeUInt(256, S +Int ((N *Int (N +Int 1)) divInt 2))
andBool #rangeUInt(256, N)
andBool #rangeUInt(256, S)
andBool GAS_AMT >=Int N *Int 178
Expand Down

0 comments on commit 3603b67

Please sign in to comment.