Revert "Revert "Match new z3 output""

This reverts commit 18d849c.
LeventErkok · Nov 20, 2023 · 4b78c12 · 4b78c12
1 parent 8f7aaca
commit 4b78c12
Show file tree

Hide file tree

Showing 6 changed files with 11 additions and 11 deletions.
diff --git a/Data/SBV/List.hs b/Data/SBV/List.hs
@@ -148,7 +148,7 @@ singleton = lift1 SeqUnit (Just (: []))
 -- Q.E.D.
 -- >>> sat $ \(l :: SList Word16) -> length l .>= 2 .&& listToListAt l 0 ./= listToListAt l (length l - 1)
 -- Satisfiable. Model:
---   s0 = [0,16] :: [Word16]
+--   s0 = [0,64] :: [Word16]
 listToListAt :: SymVal a => SList a -> SInteger -> SList a
 listToListAt s offset = subList s offset 1
 

diff --git a/Data/SBV/RegExp.hs b/Data/SBV/RegExp.hs
@@ -87,7 +87,7 @@ import Data.SBV.Char
 -- >>> let phone = pre * "-" * post
 -- >>> sat $ \s -> (s :: SString) `match` phone
 -- Satisfiable. Model:
---   s0 = "200-8000" :: String
+--   s0 = "800-8000" :: String
 class RegExpMatchable a where
    -- | @`match` s r@ checks whether @s@ is in the language generated by @r@.
    match :: a -> RegExp -> SBool

diff --git 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^6 + x^3 + 1
+-- Polynomial #1. x^16 + x^3 + x^2 + 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
@@ -129,13 +129,13 @@ nonZeroAddition = prove $ do [a, b] <- sFloats ["a", "b"]
 --
 -- >>> multInverse
 -- Falsifiable. Counter-example:
---   a = -1.7414917e38 :: Float
+--   a = 7.156233e-24 :: Float
 --
 -- Indeed, we have:
 --
--- >>> let a = -1.7414917e38 :: Float
+-- >>> let a = 7.156233e-24 :: Float
 -- >>> a * (1/a)
--- 0.9999999
+-- 0.99999994
 multInverse :: IO ThmResult
 multInverse = prove $ do a <- sFloat "a"
                          constrain $ fpIsPoint a

diff --git a/Documentation/SBV/Examples/Uninterpreted/Multiply.hs b/Documentation/SBV/Examples/Uninterpreted/Multiply.hs
@@ -47,8 +47,8 @@ mul22 (a1, a0) (b1, b0) = (mul22_hi, mul22_lo)
 -- >>> sat synthMul22
 -- Satisfiable. Model:
 --   mul22_hi :: Bool -> Bool -> Bool -> Bool -> Bool
---   mul22_hi False True  True  True  = True
 --   mul22_hi True  True  False True  = True
+--   mul22_hi False True  True  True  = True
 --   mul22_hi True  False False True  = True
 --   mul22_hi False True  True  False = True
 --   mul22_hi True  True  True  False = True
@@ -67,8 +67,8 @@ mul22 (a1, a0) (b1, b0) = (mul22_hi, mul22_lo)
 --
 -- >>> :{
 -- mul22_hi :: (SBool, SBool, SBool, SBool) -> SBool
--- mul22_hi params = params `sElem` [ (sFalse, sTrue,  sTrue,  sTrue)
---                                  , (sTrue,  sTrue,  sFalse, sTrue)
+-- mul22_hi params = params `sElem` [ (sTrue,  sTrue,  sFalse, sTrue)
+--                                  , (sFalse, sTrue,  sTrue,  sTrue)
 --                                  , (sTrue,  sFalse, sFalse, sTrue)
 --                                  , (sFalse, sTrue,  sTrue,  sFalse)
 --                                  , (sTrue,  sTrue,  sTrue,  sFalse)

diff --git a/Documentation/SBV/Examples/WeakestPreconditions/Sum.hs b/Documentation/SBV/Examples/WeakestPreconditions/Sum.hs
@@ -205,8 +205,8 @@ is an example:
 Following proof obligation failed:
 ==================================
   Invariant for loop "i < n" is not maintained by the body:
-    Before: SumS {n = 2, i = 1, s = 1}
-    After : SumS {n = 2, i = 2, s = 3}
+    Before: SumS {n = 3, i = 1, s = 1}
+    After : SumS {n = 3, i = 2, s = 3}
 
 Here, we posed the extra incorrect invariant that @s <= i@ must be maintained, and SBV found us a reachable state that violates the invariant. The
 /before/ state indeed satisfies @s <= i@, but the /after/ state does not. Note that the proof fails in this case not because the program