Release 9.8.2

CHANGES.md

@@ -1,7 +1,11 @@
 * Hackage: <http://hackage.haskell.org/package/sbvPlugin>
 * GitHub:  <http://github.com/LeventErkok/sbvPlugin>
 
-* Latest Hackage released version: 9.8.1, 2024-01-05
+* Latest Hackage released version: 9.8.2, 2024-03-23
+
+### Version 9.8.2, 2024-01-05
+  * Changes required to compile with GHC 9.8.2
+  * Bump up sbv dependence to >= 10.7
 
 ### Version 9.8.1, 2024-01-05
   * Changes required to compile with GHC 9.8.1

Makefile

@@ -33,7 +33,7 @@ docs:
 	cabal new-haddock --haddock-for-hackage --enable-doc --haddock-option="--optghc=-DHADDOCK"
 
 upload-docs-to-hackage:
-	cabal upload -d --publish ./dist-newstyle/sbvPlugin-9.8.1-docs.tar.gz
+	cabal upload -d --publish ./dist-newstyle/sbvPlugin-9.8.2-docs.tar.gz
 
 # use this as follows: make gold TGT=T49
 gold:

sbvPlugin.cabal

@@ -1,6 +1,6 @@
 Cabal-Version     : 2.2
 Name              : sbvPlugin
-Version           : 9.8.1
+Version           : 9.8.2
 Category          : Formal methods, Theorem provers, Math, SMT, Symbolic Computation
 Synopsis          : Formally prove properties of Haskell programs using SBV/SMT
 Description       : GHC plugin for proving properties over Haskell functions using SMT solvers, based
@@ -18,7 +18,7 @@ Maintainer        : Levent Erkok ([email protected])
 Build-Type        : Simple
 Extra-Source-Files: INSTALL, README.md, COPYRIGHT, CHANGES.md
 
-Tested-With       : GHC==9.8.1
+Tested-With       : GHC==9.8.2
 
 source-repository head
     type:       git
@@ -34,8 +34,8 @@ Library
                   , Data.SBV.Plugin.Examples.MergeSort
                   , Data.SBV.Plugin.Examples.MicroController
   build-depends   : base >= 4.19 && < 5
-                  , sbv      >= 10.3
-                  , ghc      >= 9.8.1
+                  , sbv      >= 10.7
+                  , ghc      >= 9.8.2
                   , ghc-prim
                   , containers
                   , mtl

tests/GoldFiles/T16.hs.golden

@@ -2,8 +2,8 @@ Loaded package environment from test-modified path
 
 [SBV] tests/T16.hs:11:1 Proving "f", using Z3.
 [Z3] Falsifiable. Counter-example:
-  ds_daqd =         0 :: Int64
+  ds_dap7 =         0 :: Int64
   age     = Age!val!0 :: Age
 [SBV] Counter-example might be bogus due to uninterpreted constant:
-  [<no location info>] ds_daqd :: Int
+  [<no location info>] ds_dap7 :: Int
 [SBV] Failed. (Use option 'IgnoreFailure' to continue.)

tests/GoldFiles/T46.hs.golden

@@ -2,17 +2,17 @@ Loaded package environment from test-modified path
 
 [SBV] tests/T46.hs:22:1-10 Proving "filtLenBad", using Z3.
 [Z3] Falsifiable. Counter-example:
-  xs_1 =  1898904026880687412 :: Int64
-  xs_2 = -1898904026880687413 :: Int64
-  xs_3 =   967593163855872713 :: Int64
-  xs_4 =  1892166082921774645 :: Int64
-  xs_5 = -3384346643702766540 :: Int64
+  xs_1 =  1896580642610626484 :: Int64
+  xs_2 = -1896580642610626485 :: Int64
+  xs_3 =  2122839034131759177 :: Int64
+  xs_4 =  1896667638314056885 :: Int64
+  xs_5 = -3347824179180231500 :: Int64
 
   f :: Int64 -> Bool
-  f 967593163855872713  = True 
-  f 1892166082921774645 = True 
-  f 1898904026880687412 = True 
-  f _                   = False
+  f (-3347824179180231500) = True 
+  f 1896667638314056885    = True 
+  f 1896580642610626484    = True 
+  f _                      = False
 
 [SBV] tests/T46.hs:26:1-11 Proving "filtLenGood", using Z3.
 [Z3] Q.E.D.