Update dependency: deps/z3 (#2675)

* deps/z3: Set Version 4.13.4

* Experimental: double smt timeout, retry limit for `examples/sum-to-n-spec.k`

* temporary fix

* Revert timeout bump

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: Palina <[email protected]>
Co-authored-by: Petar Maksimovic <[email protected]>

Author: 4 people

deps/z3

@@ -1 +1 @@
-4.13.0
+4.13.4

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]