Match new z3 version output

Data/SBV.hs

@@ -1310,15 +1310,15 @@ Q.E.D.
 Q.E.D.
 >>> prove $ roundTrip @Int32
 Falsifiable. Counter-example:
-  s0 = RoundNearestTiesToEven :: RoundingMode
-  s1 =             -536881504 :: Int32
+  s0 = RoundTowardPositive :: RoundingMode
+  s1 =          1104019333 :: Int32
 
 Note how we get a failure on `Int32`. The counter-example value is not representable exactly as a single precision float:
 
->>> toRational (-536881504 :: Float)
-(-536881536) % 1
+>>> toRational (1104019333 :: Float)
+1104019328 % 1
 
-Note how the numerator is different, it is off by 32. This is hardly surprising, since floats become sparser as
+Note how the numerator is different, it is off by 5. This is hardly surprising, since floats become sparser as
 the magnitude increases to be able to cover all the integer values representable.
 
 >>> :{
@@ -1341,15 +1341,15 @@ Q.E.D.
 >>> prove $ roundTrip @Int64
 Falsifiable. Counter-example:
   s0 = RoundNearestTiesToEven :: RoundingMode
-  s1 =   -9223372036854775538 :: Int64
+  s1 =   -2305843042984656748 :: Int64
 
 Just like in the `SFloat` case, once we reach 64-bits, we no longer can exactly represent the
 integer value for all possible values:
 
->>> toRational (fromIntegral (-9223372036854775538 :: Int64) :: Double)
-(-9223372036854775808) % 1
+>>> toRational (fromIntegral (-2305843042984656748 :: Int64) :: Double)
+(-2305843042984656896) % 1
 
-In this case the numerator is off by 270.
+In this case the numerator is off by 148.
 -}
 
 -- | An implementation of rotate-left, using a barrel shifter like design. Only works when both

Documentation/SBV/Examples/Misc/Floating.hs

@@ -69,19 +69,19 @@ assocPlus x y z = x + (y + z) .== (x + y) + z
 --
 -- >>> assocPlusRegular
 -- Falsifiable. Counter-example:
---   x = 4.4272205e21 :: Float
---   y = 2.9514347e20 :: Float
---   z = 4.4676022e15 :: Float
+--   x =  1.9258643e-34 :: Float
+--   y =  -1.925931e-34 :: Float
+--   z = -3.8518585e-34 :: Float
 --
 -- Indeed, we have:
 --
--- >>> let x = 4.4272205e21 :: Float
--- >>> let y = 2.9514347e20 :: Float
--- >>> let z = 4.4676022e15 :: Float
+-- >>> let x =  1.9258643e-34 :: Float
+-- >>> let y =  -1.925931e-34 :: Float
+-- >>> let z = -3.8518585e-34 :: Float
 -- >>> x + (y + z)
--- 4.722369e21
+-- -3.8519256e-34
 -- >>> (x + y) + z
--- 4.722368e21
+-- -3.851925e-34
 --
 -- Note the significant difference in the results!
 assocPlusRegular :: IO ThmResult

Documentation/SBV/Examples/Puzzles/HexPuzzle.hs

@@ -134,8 +134,8 @@ search initial final = runSMT $ do registerType (Proxy @SColor)
 -- 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

Documentation/SBV/Examples/Puzzles/Murder.hs

@@ -89,8 +89,8 @@ getPerson Person{nm, age, location, sex, role} = Person nm <$> (Const <$> getVal
 -- Alice     48  Bar    Female  Bystander
 -- Husband   47  Beach  Male    Killer
 -- Brother   48  Beach  Male    Victim
--- Daughter  21  Alone  Female  Bystander
--- Son       20  Bar    Male    Bystander
+-- Daughter  20  Alone  Female  Bystander
+-- Son       21  Bar    Male    Bystander
 --
 -- That is, Alice's brother was the victim and Alice's husband was the killer.
 killer :: IO ()

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 Nov 29th, 2024
+      * Version as downloaded from the above site on Dec 30th, 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.