diff --git a/Documentation/SBV/Examples/Queries/Abducts.hs b/Documentation/SBV/Examples/Queries/Abducts.hs
index 6d75debdd..ea2ccf908 100644
--- a/Documentation/SBV/Examples/Queries/Abducts.hs
+++ b/Documentation/SBV/Examples/Queries/Abducts.hs
@@ -22,10 +22,10 @@ import Data.SBV.Control
 -- and we want to make @x + y >= 2@. We have:
 --
 -- >>> example
--- Got: (define-fun abd () Bool (= s1 2))
--- Got: (define-fun abd () Bool (<= 2 s1))
--- Got: (define-fun abd () Bool (= (+ s1 s0) 2))
--- Got: (define-fun abd () Bool (= (+ s0 2) s1))
+-- Got: (define-fun abd () Bool (and (= s0 s1) (= s0 1)))
+-- Got: (define-fun abd () Bool (and (= 2 s1) (= s0 1)))
+-- Got: (define-fun abd () Bool (and (= s0 s1) (<= 1 s1)))
+-- Got: (define-fun abd () Bool (= 2 s1))
 --
 -- Note that @s0@ refers to @x@ and @s1@ refers to @y@ above. You can verify
 -- that adding any of these will ensure @x + y >= 2@.
diff --git a/SMTSolverVersions.md b/SMTSolverVersions.md
index 92987f423..d556a24cd 100644
--- a/SMTSolverVersions.md
+++ b/SMTSolverVersions.md
@@ -17,7 +17,7 @@ report any issues you might see with newer releases.
         on Jul 27, 2020.
   * CVC5:
       * https://github.com/cvc5/cvc5
-      * Version 1.0.5, downloaded compiled from GitHub repo above on Mar 13th, 2023.
+      * Version 1.0.8, downloaded compiled from GitHub repo above on Nov 29th, 2023.
   * dReal:
       * http://dreal.github.io/
       * Version installed via `brew tap dreal/dreal; brew rm dreal; brew install dreal --HEAD`
@@ -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 Oct 29th, 2023
+      * Version as downloaded from the above site on Nov 29th, 2023
       * 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.