From 59a0b1478e2350e4c78c0f7f1bbbe8822bfb5e99 Mon Sep 17 00:00:00 2001
From: Levent Erkok <erkokl@gmail.com>
Date: Fri, 25 Aug 2023 18:24:13 -0700
Subject: [PATCH] Match new z3 output

---
 Data/SBV.hs                                   | 20 +++----
 .../Examples/Existentials/CRCPolynomial.hs    |  2 +-
 Documentation/SBV/Examples/Misc/Floating.hs   | 56 +++++++++----------
 Documentation/SBV/Examples/Misc/Newtypes.hs   |  6 +-
 .../SBV/Examples/Misc/ProgramPaths.hs         | 40 ++++++-------
 .../SBV/Examples/Uninterpreted/Multiply.hs    | 12 ++--
 SBVTestSuite/GoldFiles/charConstr08.gold      |  3 +-
 SBVTestSuite/GoldFiles/query_uisatex1.gold    |  8 +--
 SBVTestSuite/GoldFiles/query_uisatex2.gold    |  4 +-
 SBVTestSuite/GoldFiles/set_tupleSet.gold      |  5 +-
 SBVTestSuite/GoldFiles/set_uninterp1.gold     |  2 +-
 SBVTestSuite/GoldFiles/sumBimapPlus.gold      |  4 +-
 SBVTestSuite/GoldFiles/sumMaybe.gold          |  4 +-
 SBVTestSuite/GoldFiles/validate_1.gold        |  8 +--
 SBVTestSuite/GoldFiles/validate_2.gold        |  8 +--
 SMTSolverVersions.md                          |  2 +-
 16 files changed, 91 insertions(+), 93 deletions(-)

diff --git a/Data/SBV.hs b/Data/SBV.hs
index cd36b6e62..666d2c662 100644
--- a/Data/SBV.hs
+++ b/Data/SBV.hs
@@ -1295,15 +1295,15 @@ Q.E.D.
 Q.E.D.
 >>> prove $ roundTrip @Int32
 Falsifiable. Counter-example:
-  s0 = RoundNearestTiesToAway :: RoundingMode
-  s1 =             -740395022 :: Int32
+  s0 = RoundNearestTiesToEven :: RoundingMode
+  s1 =              -16891903 :: Int32
 
 Note how we get a failure on `Int32`. The counter-example value is not representable exactly as a single precision float:
 
->>> toRational (-740395022 :: Float)
-(-740395008) % 1
+>>> toRational (-16891903 :: Float)
+(-16891904) % 1
 
-Note how the numerator is different, it is off by 14. This is hardly surprising, since floats become sparser as
+Note how the numerator is different, it is off by 1. This is hardly surprising, since floats become sparser as
 the magnitude increases to be able to cover all the integer values representable.
 
 >>> :{
@@ -1325,16 +1325,16 @@ Q.E.D.
 Q.E.D.
 >>> prove $ roundTrip @Int64
 Falsifiable. Counter-example:
-  s0 = RoundTowardPositive :: RoundingMode
-  s1 = 1152921504606846896 :: Int64
+  s0 = RoundNearestTiesToEven :: RoundingMode
+  s1 =    -144678154135535600 :: 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 (1152921504606846896 :: Int64) :: Double)
-1152921504606846848 % 1
+>>> toRational (fromIntegral (-144678154135535600 :: Int64) :: Double)
+(-144678154135535616) % 1
 
-In this case the numerator is off by 48.
+In this case the numerator is off by 16.
 -}
 
 -- | An implementation of rotate-left, using a barrel shifter like design. Only works when both
diff --git a/Documentation/SBV/Examples/Existentials/CRCPolynomial.hs b/Documentation/SBV/Examples/Existentials/CRCPolynomial.hs
index f39b2d47c..9e9bc9ad9 100644
--- a/Documentation/SBV/Examples/Existentials/CRCPolynomial.hs
+++ b/Documentation/SBV/Examples/Existentials/CRCPolynomial.hs
@@ -69,7 +69,7 @@ genPoly hd maxCnt = do res <- allSatWith defaultSMTCfg{allSatMaxModelCount = Jus
 -- We have:
 --
 -- >>> findHD4Polynomials 2
--- Polynomial #1. x^16 + x^3 + x^2 + 1
+-- Polynomial #1. x^16 + x^6 + x^3 + 1
 -- Polynomial #2. x^16 + x^2 + x + 1
 -- Found: 2 polynomial(s).
 --
diff --git a/Documentation/SBV/Examples/Misc/Floating.hs b/Documentation/SBV/Examples/Misc/Floating.hs
index a481b6520..fed73b671 100644
--- a/Documentation/SBV/Examples/Misc/Floating.hs
+++ b/Documentation/SBV/Examples/Misc/Floating.hs
@@ -66,19 +66,19 @@ assocPlus x y z = x + (y + z) .== (x + y) + z
 --
 -- >>> assocPlusRegular
 -- Falsifiable. Counter-example:
---   x =  2097149.9 :: Float
---   y =  13.999817 :: Float
---   z = -1.9998167 :: Float
+--   x = -1.1529219e18 :: Float
+--   y =  5.8411555e11 :: Float
+--   z = -3.5919253e19 :: Float
 --
 -- Indeed, we have:
 --
--- >>> let x =  2097149.9 :: Float
--- >>> let y =  13.999817 :: Float
--- >>> let z = -1.9998167 :: Float
+-- >>> let x = -1.1529219e18 :: Float
+-- >>> let y =  5.8411555e11 :: Float
+-- >>> let z = -3.5919253e19 :: Float
 -- >>> x + (y + z)
--- 2097162.0
+-- -3.7072176e19
 -- >>> (x + y) + z
--- 2097161.8
+-- -3.707217e19
 --
 -- Note the difference in the results!
 assocPlusRegular :: IO ThmResult
@@ -100,13 +100,13 @@ assocPlusRegular = prove $ do [x, y, z] <- sFloats ["x", "y", "z"]
 --
 -- >>> nonZeroAddition
 -- Falsifiable. Counter-example:
---   a =   -7.441692e23 :: Float
---   b = -7.5039685e-27 :: Float
+--   a = 1.4495462e-36 :: Float
+--   b =       4.5e-44 :: Float
 --
 -- Indeed, we have:
 --
--- >>> let a =   -7.441692e23 :: Float
--- >>> let b = -7.5039685e-27 :: Float
+-- >>> let a = 1.4495462e-36 :: Float
+-- >>> let b =       4.5e-44 :: Float
 -- >>> a + b == a
 -- True
 -- >>> b == 0
@@ -129,13 +129,13 @@ nonZeroAddition = prove $ do [a, b] <- sFloats ["a", "b"]
 --
 -- >>> multInverse
 -- Falsifiable. Counter-example:
---   a = -5.69379e-39 :: Float
+--   a = -1.7414917e38 :: Float
 --
 -- Indeed, we have:
 --
--- >>> let a = -5.69379e-39 :: Float
+-- >>> let a = -1.7414917e38 :: Float
 -- >>> a * (1/a)
--- 0.99999994
+-- 0.9999999
 multInverse :: IO ThmResult
 multInverse = prove $ do a <- sFloat "a"
                          constrain $ fpIsPoint a
@@ -155,28 +155,28 @@ multInverse = prove $ do a <- sFloat "a"
 --
 -- >>> roundingAdd
 -- Satisfiable. Model:
---   rm = RoundTowardZero :: RoundingMode
---   x  =  -1.0579198e-37 :: Float
---   y  =   4.7017266e-38 :: Float
+--   rm = RoundTowardPositive :: RoundingMode
+--   x  =                -2.0 :: Float
+--   y  =       1.2621775e-29 :: Float
 --
 -- (Note that depending on your version of Z3, you might get a different result.)
 -- Unfortunately Haskell floats do not allow computation with arbitrary rounding modes, but SBV's
 -- 'SFloatingPoint' type does. We have:
 --
--- >>> fpAdd sRoundTowardZero (-1.0579198e-37) (4.7017266e-38) :: SFPSingle
--- -5.87747119e-38 :: SFloatingPoint 8 24
--- >>> fpAdd sRoundNearestTiesToEven (-1.0579198e-37) (4.7017266e-38) :: SFPSingle
--- -5.87747175e-38 :: SFloatingPoint 8 24
+-- >>> fpAdd sRoundTowardPositive (-2.0) (1.2621775e-29) :: SFPSingle
+-- -1.99999988 :: SFloatingPoint 8 24
+-- >>> fpAdd sRoundNearestTiesToEven (-2.0) (1.2621775e-29) :: SFPSingle
+-- -2.0 :: SFloatingPoint 8 24
 --
--- We can see why these two results are indeed different: The 'RoundTowardZero'
--- (which rounds towards zero) produces a larger result, closer to 0. Indeed, if we treat these numbers
+-- We can see why these two results are indeed different: The 'RoundTowardPositive'
+-- (which rounds towards positive infinity) produces a larger result, closer to 0. Indeed, if we treat these numbers
 -- as 'Double' values, we get:
 --
--- >>> (-1.0579198e-37) + (4.7017266e-38) :: Double
--- -5.8774714e-38
+-- >>> (-2.0) + 1.2621775e-29 :: Double
+-- -2.0
 --
--- we see that the "more precise" result is larger than what the 'Float' value is, justifying the
--- larger value with 'RoundTowardZero'. A more detailed study is beyond our current scope, so we'll
+-- we see that the "more precise" result is smaller than what the 'Float' value is, justifying the
+-- larger value with 'RoundTowardPositive'. A more detailed study is beyond our current scope, so we'll
 -- merely note that floating point representation and semantics is indeed a thorny
 -- subject, and point to <http://ece.uwaterloo.ca/~dwharder/NumericalAnalysis/02Numerics/Double/paper.pdf> as
 -- an excellent guide.
diff --git a/Documentation/SBV/Examples/Misc/Newtypes.hs b/Documentation/SBV/Examples/Misc/Newtypes.hs
index 4b51b0519..ab3006612 100644
--- a/Documentation/SBV/Examples/Misc/Newtypes.hs
+++ b/Documentation/SBV/Examples/Misc/Newtypes.hs
@@ -81,12 +81,12 @@ ceilingHighEnoughForHuman ceiling humanHeight = humanHeight' .< ceiling'
 --
 -- >>> sat problem
 -- Satisfiable. Model:
---   floorToCeiling =  16 :: Integer
---   humanheight    = 255 :: Word16
+--   floorToCeiling =   3 :: Integer
+--   humanheight    = 272 :: Word16
 problem :: Predicate
 problem = do
     ceiling     :: SMetres          <- free "floorToCeiling"
     humanHeight :: SHumanHeightInCm <- free "humanheight"
-    constrain $ humanHeight .<= tallestHumanEver
+    constrain $ humanHeight .== tallestHumanEver
 
     return $ ceilingHighEnoughForHuman ceiling humanHeight
diff --git a/Documentation/SBV/Examples/Misc/ProgramPaths.hs b/Documentation/SBV/Examples/Misc/ProgramPaths.hs
index 7ab2b46fd..33bd7cab0 100644
--- a/Documentation/SBV/Examples/Misc/ProgramPaths.hs
+++ b/Documentation/SBV/Examples/Misc/ProgramPaths.hs
@@ -48,36 +48,36 @@ d4 x y = d1 x y + d2 y + d3 x y
 --
 -- >>> paths
 -- Solution #1:
---   x =   7 :: Integer
+--   x =  -2 :: Integer
 --   y =   4 :: Integer
---   r = 217 :: Integer
+--   r = 112 :: Integer
 -- Solution #2:
---   x =   4 :: Integer
---   y =   0 :: Integer
---   r = 257 :: Integer
--- Solution #3:
---   x =   3 :: Integer
---   y =  -1 :: Integer
---   r = 157 :: Integer
--- Solution #4:
---   x =  -1 :: Integer
+--   x =   0 :: Integer
 --   y =   3 :: Integer
---   r = 152 :: Integer
--- Solution #5:
+--   r = 252 :: Integer
+-- Solution #3:
 --   x =  -1 :: Integer
 --   y =   4 :: Integer
 --   r = 212 :: Integer
+-- Solution #4:
+--   x =   3 :: Integer
+--   y =   0 :: Integer
+--   r = 257 :: Integer
+-- Solution #5:
+--   x =   2 :: Integer
+--   y =  -1 :: Integer
+--   r = 157 :: Integer
 -- Solution #6:
---   x =   0 :: Integer
---   y =   3 :: Integer
---   r = 252 :: Integer
--- Solution #7:
---   x =  -2 :: Integer
+--   x =   7 :: Integer
 --   y =   4 :: Integer
---   r = 112 :: Integer
+--   r = 217 :: Integer
+-- Solution #7:
+--   x =   0 :: Integer
+--   y =   0 :: Integer
+--   r = 152 :: Integer
 -- Found 7 different solutions.
 paths :: IO AllSatResult
 paths = allSat $ do
   x <- sInteger "x"
   y <- sInteger "y"
-  partition "r" $ d4 x y
\ No newline at end of file
+  partition "r" $ d4 x y
diff --git a/Documentation/SBV/Examples/Uninterpreted/Multiply.hs b/Documentation/SBV/Examples/Uninterpreted/Multiply.hs
index 920591543..5b96bf498 100644
--- a/Documentation/SBV/Examples/Uninterpreted/Multiply.hs
+++ b/Documentation/SBV/Examples/Uninterpreted/Multiply.hs
@@ -47,12 +47,12 @@ mul22 (a1, a0) (b1, b0) = (mul22_hi, mul22_lo)
 -- >>> sat synthMul22
 -- Satisfiable. Model:
 --   mul22_hi :: Bool -> Bool -> Bool -> Bool -> Bool
---   mul22_hi True  False False True  = True
---   mul22_hi True  True  False True  = True
 --   mul22_hi False True  True  True  = True
---   mul22_hi True  False True  True  = True
+--   mul22_hi True  True  False True  = True
+--   mul22_hi True  False False True  = True
 --   mul22_hi False True  True  False = True
 --   mul22_hi True  True  True  False = True
+--   mul22_hi True  False True  True  = True
 --   mul22_hi _     _     _     _     = False
 -- <BLANKLINE>
 --   mul22_lo :: Bool -> Bool -> Bool
@@ -67,12 +67,12 @@ mul22 (a1, a0) (b1, b0) = (mul22_hi, mul22_lo)
 --
 -- >>> :{
 -- mul22_hi :: (SBool, SBool, SBool, SBool) -> SBool
--- mul22_hi params = params `sElem` [ (sTrue,  sFalse, sFalse, sTrue)
+-- mul22_hi params = params `sElem` [ (sFalse, sTrue,  sTrue,  sTrue)
 --                                  , (sTrue,  sTrue,  sFalse, sTrue)
---                                  , (sFalse, sTrue,  sTrue,  sTrue)
---                                  , (sTrue,  sFalse, sTrue,  sTrue)
+--                                  , (sTrue,  sFalse, sFalse, sTrue)
 --                                  , (sFalse, sTrue,  sTrue,  sFalse)
 --                                  , (sTrue,  sTrue,  sTrue,  sFalse)
+--                                  , (sTrue,  sFalse, sTrue,  sTrue)
 --                                  ]
 -- :}
 --
diff --git a/SBVTestSuite/GoldFiles/charConstr08.gold b/SBVTestSuite/GoldFiles/charConstr08.gold
index 53683f85a..038c36e21 100644
--- a/SBVTestSuite/GoldFiles/charConstr08.gold
+++ b/SBVTestSuite/GoldFiles/charConstr08.gold
@@ -36,8 +36,7 @@
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (s0))
-[RECV] ((s0 (lambda ((x!1 String))
-         (and (not (and (not (= x!1 "A")) (not (= x!1 "B")))) (not (= x!1 "B"))))))
+[RECV] ((s0 (lambda ((x!1 String)) (= x!1 "A"))))
 
 MODEL: SMTModel {modelObjectives = [], modelBindings = Nothing, modelAssocs = [("x",{'A'} :: {Char})], modelUIFuns = []}
 DONE.*** Solver   : Z3
diff --git a/SBVTestSuite/GoldFiles/query_uisatex1.gold b/SBVTestSuite/GoldFiles/query_uisatex1.gold
index 9dfbdd5f7..a8b59961f 100644
--- a/SBVTestSuite/GoldFiles/query_uisatex1.gold
+++ b/SBVTestSuite/GoldFiles/query_uisatex1.gold
@@ -117,12 +117,12 @@
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (s0))
-[RECV] ((s0 (- 1)))
+[RECV] ((s0 0))
 [GOOD] (set-option :pp.max_depth      4294967295)
 [GOOD] (set-option :pp.min_alias_size 4294967295)
 [GOOD] (set-option :model.inline_def  true      )
 [SEND] (get-value (q1))
-[RECV] ((q1 (store (store (store ((as const (Array Int Int)) 12) 3 75) (- 3) 9) (- 1) 0)))
+[RECV] ((q1 (store (store (store ((as const (Array Int Int)) 12) 3 75) (- 3) 9) 0 1)))
 [SEND] (get-value (q2))
 [RECV] ((q2 (store (store ((as const (Array Bool Int Int)) 5) false 7 6) false 12 3)))
 [SEND] (get-value (q3))
@@ -164,10 +164,10 @@
 
  FINAL:
 Satisfiable. Model:
-  s0 = -1 :: Integer
+  s0 = 0 :: Integer
 
   q1 :: Integer -> Integer
-  q1 (-1) = 0 
+  q1 0    = 1 
   q1 (-3) = 9 
   q1 3    = 75
   q1 _    = 12
diff --git a/SBVTestSuite/GoldFiles/query_uisatex2.gold b/SBVTestSuite/GoldFiles/query_uisatex2.gold
index 804e09417..9cb558cb6 100644
--- a/SBVTestSuite/GoldFiles/query_uisatex2.gold
+++ b/SBVTestSuite/GoldFiles/query_uisatex2.gold
@@ -119,7 +119,7 @@
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (q1))
-[RECV] ((q1 (store (store (store ((as const (Array Int Int)) 12) 3 75) (- 3) 9) (- 1) 0)))
+[RECV] ((q1 (store (store (store ((as const (Array Int Int)) 12) 3 75) (- 3) 9) 0 1)))
 [SEND] (get-value (q2))
 [RECV] ((q2 (store (store ((as const (Array Bool Int Int)) 5) false 7 6) false 12 3)))
 [SEND] (get-value (q3))
@@ -162,5 +162,5 @@
 *** Exit code: ExitSuccess
 
  FINAL:
-(Right ([(-1,0),(-3,9),(3,75)],12),Right ([((False,12),3),((False,7),6)],5),Right ([((9.6,False,8),Infinity),((9.6,True,121),-0.0)],8.6),Right ([(('r',"foo"),3.5),(('c',"tey"),92.0)],78.0),Right ([(([5],[8.2,0.0]),210),(([9,5],[8.2,9.0]),21)],7),Right ([],False))
+(Right ([(0,1),(-3,9),(3,75)],12),Right ([((False,12),3),((False,7),6)],5),Right ([((9.6,False,8),Infinity),((9.6,True,121),-0.0)],8.6),Right ([(('r',"foo"),3.5),(('c',"tey"),92.0)],78.0),Right ([(([5],[8.2,0.0]),210),(([9,5],[8.2,9.0]),21)],7),Right ([],False))
 DONE!
diff --git a/SBVTestSuite/GoldFiles/set_tupleSet.gold b/SBVTestSuite/GoldFiles/set_tupleSet.gold
index 5371553ee..acbb9985c 100644
--- a/SBVTestSuite/GoldFiles/set_tupleSet.gold
+++ b/SBVTestSuite/GoldFiles/set_tupleSet.gold
@@ -34,12 +34,11 @@
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (s0))
-[RECV] ((s0 (mkSBVTuple2 ((as const (Array Bool Bool)) true)
-                    (store ((as const (Array Bool Bool)) false) false true))))
+[RECV] ((s0 (mkSBVTuple2 ((as const (Array Bool Bool)) true) (lambda ((x!1 Bool)) x!1))))
 *** Solver   : Z3
 *** Exit code: ExitSuccess
 
 FINAL:
 Satisfiable. Model:
-  s0 = (U,{False}) :: ({Bool}, {Bool})
+  s0 = (U,{True}) :: ({Bool}, {Bool})
 DONE!
diff --git a/SBVTestSuite/GoldFiles/set_uninterp1.gold b/SBVTestSuite/GoldFiles/set_uninterp1.gold
index e349faa07..3c02ddd44 100644
--- a/SBVTestSuite/GoldFiles/set_uninterp1.gold
+++ b/SBVTestSuite/GoldFiles/set_uninterp1.gold
@@ -104,7 +104,7 @@ Fast allSat, Looking for solution 8
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (s0))
-[RECV] ((s0 (store (store ((as const (Array E Bool)) false) B true) C true)))
+[RECV] ((s0 (store (store ((as const (Array E Bool)) false) C true) B true)))
 [GOOD] (push 1)
 [GOOD] (define-fun s22 () (Array E Bool) (store (store ((as const (Array E Bool)) false) C true) B true))
 [GOOD] (define-fun s23 () Bool (= s0 s22))
diff --git a/SBVTestSuite/GoldFiles/sumBimapPlus.gold b/SBVTestSuite/GoldFiles/sumBimapPlus.gold
index cc6e182e8..c55178488 100644
--- a/SBVTestSuite/GoldFiles/sumBimapPlus.gold
+++ b/SBVTestSuite/GoldFiles/sumBimapPlus.gold
@@ -48,8 +48,8 @@
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (s0))
-[RECV] ((s0 (left_SBVEither (- 1))))
+[RECV] ((s0 (left_SBVEither 0)))
 
-MODEL: SMTModel {modelObjectives = [], modelBindings = Nothing, modelAssocs = [("x",Left -1 :: Either Integer Integer)], modelUIFuns = []}
+MODEL: SMTModel {modelObjectives = [], modelBindings = Nothing, modelAssocs = [("x",Left 0 :: Either Integer Integer)], modelUIFuns = []}
 DONE.*** Solver   : Z3
 *** Exit code: ExitSuccess
diff --git a/SBVTestSuite/GoldFiles/sumMaybe.gold b/SBVTestSuite/GoldFiles/sumMaybe.gold
index d7d62a557..23822189c 100644
--- a/SBVTestSuite/GoldFiles/sumMaybe.gold
+++ b/SBVTestSuite/GoldFiles/sumMaybe.gold
@@ -54,8 +54,8 @@
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (s0))
-[RECV] ((s0 (just_SBVMaybe (- 1))))
+[RECV] ((s0 (just_SBVMaybe 0)))
 
-MODEL: SMTModel {modelObjectives = [], modelBindings = Nothing, modelAssocs = [("x",Just -1 :: Maybe Integer)], modelUIFuns = []}
+MODEL: SMTModel {modelObjectives = [], modelBindings = Nothing, modelAssocs = [("x",Just 0 :: Maybe Integer)], modelUIFuns = []}
 DONE.*** Solver   : Z3
 *** Exit code: ExitSuccess
diff --git a/SBVTestSuite/GoldFiles/validate_1.gold b/SBVTestSuite/GoldFiles/validate_1.gold
index e7d062305..62e282e31 100644
--- a/SBVTestSuite/GoldFiles/validate_1.gold
+++ b/SBVTestSuite/GoldFiles/validate_1.gold
@@ -29,11 +29,11 @@
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (s0))
-[RECV] ((s0 (fp #b1 #xfe #b11111111111111111111111)))
+[RECV] ((s0 (_ -zero 8 24)))
 *** Solver   : Z3
 *** Exit code: ExitSuccess
 [VALIDATE] Validating the model. Assignment:
-[VALIDATE]       x = -3.4028235e38 :: Float
+[VALIDATE]       x = -0.0 :: Float
 [VALIDATE] There are no constraints to check.
 [VALIDATE] Validating outputs.
 
@@ -42,7 +42,7 @@ FINAL OUTPUT:
 *** 
 *** Assignment:
 *** 
-***       x = -3.4028235e38 :: Float
+***       x = -0.0 :: Float
 *** 
 *** Not all floating point operations are supported concretely.
 *** 
@@ -52,4 +52,4 @@ FINAL OUTPUT:
 *** Alleged model:
 ***
 *** Satisfiable. Model:
-***   x = -3.4028235e38 :: Float
+***   x = -0.0 :: Float
diff --git a/SBVTestSuite/GoldFiles/validate_2.gold b/SBVTestSuite/GoldFiles/validate_2.gold
index e9e976da8..75827f02f 100644
--- a/SBVTestSuite/GoldFiles/validate_2.gold
+++ b/SBVTestSuite/GoldFiles/validate_2.gold
@@ -29,11 +29,11 @@
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (s0))
-[RECV] ((s0 (_ -zero 8 24)))
+[RECV] ((s0 (fp #b0 #x00 #b11111111111111111011000)))
 *** Solver   : Z3
 *** Exit code: ExitSuccess
 [VALIDATE] Validating the model. Assignment:
-[VALIDATE]       x = -0.0 :: Float
+[VALIDATE]       x = 1.1754887e-38 :: Float
 [VALIDATE] There are no constraints to check.
 [VALIDATE] Validating outputs.
 
@@ -42,7 +42,7 @@ FINAL OUTPUT:
 *** 
 *** Assignment:
 *** 
-***       x = -0.0 :: Float
+***       x = 1.1754887e-38 :: Float
 *** 
 *** Floating point FMA operation is not supported concretely.
 *** 
@@ -52,4 +52,4 @@ FINAL OUTPUT:
 *** Alleged model:
 ***
 *** Satisfiable. Model:
-***   x = -0.0 :: Float
+***   x = 1.1754887e-38 :: Float
diff --git a/SMTSolverVersions.md b/SMTSolverVersions.md
index ddf659015..085232880 100644
--- a/SMTSolverVersions.md
+++ b/SMTSolverVersions.md
@@ -30,7 +30,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 Jun 30th, 2023
+      * Version as downloaded from the above site on Aug 25th, 2023
       * 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.