more doctest fixes

LeventErkok · Sep 16, 2024 · 3a121fb · 3a121fb
1 parent eb464ef
commit 3a121fb
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 7 deletions.
diff --git a/Documentation/SBV/Examples/Misc/LambdaArray.hs b/Documentation/SBV/Examples/Misc/LambdaArray.hs
@@ -45,11 +45,12 @@ memsetExample = prove $ do
 --
 -- >>> outOfInit
 -- Satisfiable. Model:
---   Read = 1 :: Integer
---   lo   = 0 :: Integer
---   hi   = 0 :: Integer
---   zero = 0 :: Integer
---   idx  = 1 :: Integer
+--   Read =       1 :: Integer
+--   mem  = ([], 1) :: Array Integer Integer
+--   lo   =       0 :: Integer
+--   hi   =       0 :: Integer
+--   zero =       0 :: Integer
+--   idx  =       1 :: Integer
 outOfInit :: IO SatResult
 outOfInit = sat $ do
    mem  <- sArray "mem"

diff --git a/Documentation/SBV/Examples/WeakestPreconditions/Sum.hs b/Documentation/SBV/Examples/WeakestPreconditions/Sum.hs
@@ -208,8 +208,8 @@ is an example:
 Following proof obligation failed:
 ==================================
   Invariant for loop "i < n" is not maintained by the body:
-    Before: SumS {n = 3, i = 1, s = 1}
-    After : SumS {n = 3, i = 2, s = 3}
+    Before: SumS {n = 2, i = 1, s = 1}
+    After : SumS {n = 2, 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