Update z3 tested date and match new z3 output

Documentation/SBV/Examples/Puzzles/HexPuzzle.hs

@@ -130,8 +130,8 @@ search initial final = runSMT $ do emptyGrid :: Grid <- newArray "emptyGrid" (Ju
 -- Searching at depth: 4
 -- Searching at depth: 5
 -- Searching at depth: 6
--- Found: [10,10,9,11,14,6]
 -- Found: [10,10,11,9,14,6]
+-- Found: [10,10,9,11,14,6]
 -- There are no more solutions.
 example :: IO ()
 example = search initBoard finalBoard

SBVTestSuite/GoldFiles/query1.gold

@@ -77,7 +77,7 @@
 [SEND] (get-info :reason-unknown)
 [RECV] (:reason-unknown "state of the most recent check-sat command is not known")
 [SEND] (get-info :version)
-[RECV] (:version "4.12.6")
+[RECV] (:version "4.13.0")
 [SEND] (get-info :status)
 [RECV] (:status sat)
 [GOOD] (define-fun s16 () Int 4)
@@ -108,7 +108,7 @@
 [SEND] (get-info :reason-unknown)
 [RECV] (:reason-unknown "unknown")
 [SEND] (get-info :version)
-[RECV] (:version "4.12.6")
+[RECV] (:version "4.13.0")
 [SEND] (get-info :memory)
 [RECV] unsupported
 [SEND] (get-info :time)
@@ -152,18 +152,18 @@
 [RECV] ((set-logic ALL)
        (proof
        (let (($x268 (<= s0 6)))
-        (let (($x269 (not $x268)))
-        (let (($x276 (or (not bey) $x269)))
-        (let ((@x274 (monotonicity (rewrite (= (> s0 6) $x269)) (= (=> bey (> s0 6)) (=> bey $x269)))))
-        (let ((@x280 (trans @x274 (rewrite (= (=> bey $x269) $x276)) (= (=> bey (> s0 6)) $x276))))
-        (let ((@x281 (mp (asserted (=> bey (> s0 6))) @x280 $x276)))
-        (let (($x293 (>= s0 6)))
-        (let (($x292 (not $x293)))
-        (let (($x300 (or (not hey) $x292)))
-        (let ((@x291 (trans (rewrite (= (< s0 6) (not (<= 6 s0)))) (rewrite (= (not (<= 6 s0)) $x292)) (= (< s0 6) $x292))))
-        (let ((@x304 (trans (monotonicity @x291 (= (=> hey (< s0 6)) (=> hey $x292))) (rewrite (= (=> hey $x292) $x300)) (= (=> hey (< s0 6)) $x300))))
-        (let ((@x305 (mp (asserted (=> hey (< s0 6))) @x304 $x300)))
-        (unit-resolution ((_ th-lemma arith farkas 1 1) (or $x293 $x268)) (unit-resolution @x305 (asserted hey) $x292) (unit-resolution @x281 (asserted bey) $x269) false)))))))))))))))
+       (let (($x269 (not $x268)))
+       (let (($x276 (or (not bey) $x269)))
+       (let ((@x274 (monotonicity (rewrite (= (> s0 6) $x269)) (= (=> bey (> s0 6)) (=> bey $x269)))))
+       (let ((@x280 (trans @x274 (rewrite (= (=> bey $x269) $x276)) (= (=> bey (> s0 6)) $x276))))
+       (let ((@x281 (mp (asserted (=> bey (> s0 6))) @x280 $x276)))
+       (let (($x293 (>= s0 6)))
+       (let (($x292 (not $x293)))
+       (let (($x300 (or (not hey) $x292)))
+       (let ((@x291 (trans (rewrite (= (< s0 6) (not (<= 6 s0)))) (rewrite (= (not (<= 6 s0)) $x292)) (= (< s0 6) $x292))))
+       (let ((@x304 (trans (monotonicity @x291 (= (=> hey (< s0 6)) (=> hey $x292))) (rewrite (= (=> hey $x292) $x300)) (= (=> hey (< s0 6)) $x300))))
+       (let ((@x305 (mp (asserted (=> hey (< s0 6))) @x304 $x300)))
+       (unit-resolution ((_ th-lemma arith farkas 1 1) (or $x293 $x268)) (unit-resolution @x305 (asserted hey) $x292) (unit-resolution @x281 (asserted bey) $x269) false)))))))))))))))
 [SEND, TimeOut: 90000ms] (get-assertions)
 
 [RECV] ((! s7 :named |a > 0|)

SMTSolverVersions.md

@@ -33,7 +33,7 @@ report any issues you might see with newer releases.
       * Version 2.6.2 as downloaded from the above site on Apr 7, 2020
   * Z3:
       * http://github.com/Z3Prover/z3
-      * Version as downloaded from the above site on Feb 20th, 2024
+      * Version as downloaded from the above site on Mar 15th, 2024
       * SBV typically relies on latest features of z3, so compiling directly
         from the sources is recommended. If that's not possible, you should
         always use their latest release.