Fix doctests

CHANGES.md

@@ -5,7 +5,7 @@
 
 ### Version 10.2.5, Not yet released
 
-  * Clean-up GHC extensions required in the cabal file
+  * Clean-up GHC extensions required in the cabal file, and changes required to compile cleanly with GHC 9.8.1
 
   * Add 'partition', which allows for partitioning all-sat search spaces when models are generated.
 

Data/SBV/Tools/Overflow.hs

@@ -68,7 +68,7 @@ class ArithOverflow a where
   -- | Bit-vector division. Unsigned division neither underflows nor overflows. Signed division can only overflow. In fact, for each
   -- signed bitvector type, there's precisely one pair that overflows, when @x@ is @minBound@ and @y@ is @-1@:
   --
-  -- >>> allSat $ \x y -> snd (x `bvDivO` (y::SInt8))
+  -- >>> allSat $ \x y -> x `bvDivO` (y::SInt8)
   -- Solution #1:
   --   s0 = -128 :: Int8
   --   s1 =   -1 :: Int8
@@ -78,7 +78,7 @@ class ArithOverflow a where
   -- | Bit-vector negation. Unsigned negation neither underflows nor overflows. Signed negation can only overflow, when the argument is
   -- @minBound@:
   --
-  -- >>> prove $ \x -> x .== minBound .<=> snd (bvNegO (x::SInt16))
+  -- >>> prove $ \x -> x .== minBound .<=> bvNegO (x::SInt16)
   -- Q.E.D.
   bvNegO :: a -> SBool
 

Documentation/SBV/Examples/BitPrecise/BrokenSearch.hs

@@ -26,15 +26,15 @@ import Data.SBV.Tools.Overflow
 --
 -- >>> checkArithOverflow midPointBroken
 -- ./Documentation/SBV/Examples/BitPrecise/BrokenSearch.hs:39:32:+!: SInt32 addition overflows: Violated. Model:
---   low  = 2147475456 :: Int32
---   high = 2147483646 :: Int32
+--   low  = 1073741832 :: Int32
+--   high = 1107296257 :: Int32
 --
 -- Indeed:
 --
--- >>> (2147475456 + 2147483646) `div` (2::Int32)
--- -4097
+-- >>> (1073741832 + 1107296257) `div` (2::Int32)
+-- -1056964604
 --
--- giving us a negative mid-point value!
+-- giving us quite a large negative mid-point value!
 midPointBroken :: SInt32 -> SInt32 -> SInt32
 midPointBroken low high = (low +! high) /! 2