Merge branch 'master' into _update-deps/runtimeverification/evm-seman…

…tics
runtimeverification · Jan 14, 2025 · 42fae6f · 42fae6f
2 parents 2ecce15 + 3603b67
commit 42fae6f
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/deps/z3 b/deps/z3
@@ -1 +1 @@
-4.13.0
+4.13.4
diff --git a/src/tests/integration/test-data/lemmas.k b/src/tests/integration/test-data/lemmas.k
@@ -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 
@@ -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