diff --git a/deps/z3 b/deps/z3
index 813b83b653..32d3e23b48 100644
--- 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
index 2ebeeaca83..767f778985 100644
--- 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]