diff --git a/Manual/Description/HolSmt.tex b/Manual/Description/HolSmt.tex
index 1920546733..a4080e7c03 100644
--- a/Manual/Description/HolSmt.tex
+++ b/Manual/Description/HolSmt.tex
@@ -195,8 +195,8 @@ \subsection{Interface}
 
 \subsection{Installing SMT solvers}
 
-\ml{HolSmtLib} has been tested with cvc5~1.0.8, Yices~1.0.29, Z3~2.19
-and Z3~4.8.17. Later versions may or may not work.  (Yices~2 is not
+\ml{HolSmtLib} has been tested with cvc5~1.1.0, Yices~1.0.40, Z3~2.19
+and Z3~4.12.4. Later versions may or may not work.  (Yices~2 is not
 supported.)  To use \ml{HolSmtLib}, you need to install at least one
 of these SMT solvers on your machine.  As mentioned before, Yices
 supports a larger fragment of higher-order logic than Z3, but proof
diff --git a/Manual/Translations/IT/Description/HolSmt.tex b/Manual/Translations/IT/Description/HolSmt.tex
index 1920546733..a4080e7c03 100644
--- a/Manual/Translations/IT/Description/HolSmt.tex
+++ b/Manual/Translations/IT/Description/HolSmt.tex
@@ -195,8 +195,8 @@ \subsection{Interface}
 
 \subsection{Installing SMT solvers}
 
-\ml{HolSmtLib} has been tested with cvc5~1.0.8, Yices~1.0.29, Z3~2.19
-and Z3~4.8.17. Later versions may or may not work.  (Yices~2 is not
+\ml{HolSmtLib} has been tested with cvc5~1.1.0, Yices~1.0.40, Z3~2.19
+and Z3~4.12.4. Later versions may or may not work.  (Yices~2 is not
 supported.)  To use \ml{HolSmtLib}, you need to install at least one
 of these SMT solvers on your machine.  As mentioned before, Yices
 supports a larger fragment of higher-order logic than Z3, but proof