diff --git a/SBVTestSuite/GoldFiles/allSat8.gold b/SBVTestSuite/GoldFiles/allSat8.gold index 24aba83db..67f67defe 100644 --- a/SBVTestSuite/GoldFiles/allSat8.gold +++ b/SBVTestSuite/GoldFiles/allSat8.gold @@ -61,4 +61,4 @@ EXCEPTION CAUGHT: *** NB. If this is a use case you'd like SBV to support, please get in touch! CallStack (from HasCallStack): - error, called at ./Data/SBV/Control/Utils.hs:1660:57 in sbv-10.7-inplace:Data.SBV.Control.Utils + error, called at ./Data/SBV/Control/Utils.hs:1660:57 in sbv-10.8-inplace:Data.SBV.Control.Utils diff --git a/SBVTestSuite/GoldFiles/nested1.gold b/SBVTestSuite/GoldFiles/nested1.gold index 8a04f7f07..c0972cbb3 100644 --- a/SBVTestSuite/GoldFiles/nested1.gold +++ b/SBVTestSuite/GoldFiles/nested1.gold @@ -11,4 +11,4 @@ Data.SBV: Mismatched contexts detected. *** See https://github.com/LeventErkok/sbv/issues/71 for several examples. CallStack (from HasCallStack): - error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.7-inplace:Data.SBV.Core.Symbolic \ No newline at end of file + error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.8-inplace:Data.SBV.Core.Symbolic \ No newline at end of file diff --git a/SBVTestSuite/GoldFiles/nested2.gold b/SBVTestSuite/GoldFiles/nested2.gold index 8a04f7f07..c0972cbb3 100644 --- a/SBVTestSuite/GoldFiles/nested2.gold +++ b/SBVTestSuite/GoldFiles/nested2.gold @@ -11,4 +11,4 @@ Data.SBV: Mismatched contexts detected. *** See https://github.com/LeventErkok/sbv/issues/71 for several examples. CallStack (from HasCallStack): - error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.7-inplace:Data.SBV.Core.Symbolic \ No newline at end of file + error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.8-inplace:Data.SBV.Core.Symbolic \ No newline at end of file diff --git a/SBVTestSuite/GoldFiles/nested3.gold b/SBVTestSuite/GoldFiles/nested3.gold index 37ca23bfb..932be97b3 100644 --- a/SBVTestSuite/GoldFiles/nested3.gold +++ b/SBVTestSuite/GoldFiles/nested3.gold @@ -37,4 +37,4 @@ Data.SBV: Mismatched contexts detected. *** See https://github.com/LeventErkok/sbv/issues/71 for several examples. CallStack (from HasCallStack): - error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.7-inplace:Data.SBV.Core.Symbolic \ No newline at end of file + error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.8-inplace:Data.SBV.Core.Symbolic \ No newline at end of file diff --git a/SBVTestSuite/GoldFiles/nested4.gold b/SBVTestSuite/GoldFiles/nested4.gold index fbabd6d95..615f3dd6b 100644 --- a/SBVTestSuite/GoldFiles/nested4.gold +++ b/SBVTestSuite/GoldFiles/nested4.gold @@ -11,4 +11,4 @@ Data.SBV: Mismatched contexts detected. *** See https://github.com/LeventErkok/sbv/issues/71 for several examples. CallStack (from HasCallStack): - error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.7-inplace:Data.SBV.Core.Symbolic \ No newline at end of file + error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.8-inplace:Data.SBV.Core.Symbolic \ No newline at end of file diff --git a/SBVTestSuite/GoldFiles/query1.gold b/SBVTestSuite/GoldFiles/query1.gold index c976a3de4..d6a6c4ec5 100644 --- a/SBVTestSuite/GoldFiles/query1.gold +++ b/SBVTestSuite/GoldFiles/query1.gold @@ -77,7 +77,7 @@ [SEND] (get-info :reason-unknown) [RECV] (:reason-unknown "state of the most recent check-sat command is not known") [SEND] (get-info :version) -[RECV] (:version "4.13.0") +[RECV] (:version "4.13.1") [SEND] (get-info :status) [RECV] (:status sat) [GOOD] (define-fun s16 () Int 4) @@ -108,7 +108,7 @@ [SEND] (get-info :reason-unknown) [RECV] (:reason-unknown "unknown") [SEND] (get-info :version) -[RECV] (:version "4.13.0") +[RECV] (:version "4.13.1") [SEND] (get-info :memory) [RECV] unsupported [SEND] (get-info :time) diff --git a/SMTSolverVersions.md b/SMTSolverVersions.md index 0ecf10fa3..add9e17c5 100644 --- a/SMTSolverVersions.md +++ b/SMTSolverVersions.md @@ -33,7 +33,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 Mar 23rd, 2024 + * Version as downloaded from the above site on April 5th, 2024 * 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.