temporary fix

runtimeverification · Jan 13, 2025 · 741fbc2 · 741fbc2
1 parent 4aa718f
commit 741fbc2
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 5 deletions.
diff --git a/deps/z3 b/deps/z3
@@ -1 +1 @@
-4.13.0
+4.13.4
diff --git a/tests/specs/examples/sum-to-n-spec.k b/tests/specs/examples/sum-to-n-spec.k
@@ -13,8 +13,6 @@ module VERIFICATION
 
     rule chop(I) => I requires #rangeUInt(256, I) [simplification]
 
-    rule 0 <=Int #sizeWordStack ( _ , _ ) => true [simplification, smt-lemma]
-
     syntax Bytes ::= "sumToN" [macro]
  // -------------------------------------
     rule sumToN
@@ -66,10 +64,10 @@ module SUM-TO-N-SPEC
           <pc>  3 => 21                         </pc>
           <gas> G => G -Int (52 *Int I +Int 21) </gas>
           <wordStack> I : S                               : WS
-                   => 0 : S +Int I *Int (I +Int 1) /Int 2 : WS </wordStack>
+                   => 0 : S +Int I *Int (I +Int 1) divInt 2 : WS </wordStack>
       requires I >=Int 0
        andBool S >=Int 0
-       andBool S +Int I *Int (I +Int 1) /Int 2 <Int pow256
+       andBool S +Int I *Int (I +Int 1) divInt 2 <Int pow256
        andBool #sizeWordStack(WS) <Int 1021
        andBool G >=Int 52 *Int I +Int 21
       [circularity]