From 29d5e1caf22bc94c7a03e29cb1cb59067522f5d6 Mon Sep 17 00:00:00 2001 From: someplaceguy Date: Tue, 16 Jan 2024 23:12:16 +0000 Subject: [PATCH] HolSmt: update docs wrt tested solver versions The Docker CI update in #1179 is using newer solver versions, so update HolSmt documentation to match those. The Docker CI is actually using the old Z3 2.19 version by default, but I've tested Z3 4.12.4 locally and confirmed the self-tests pass. --- Manual/Description/HolSmt.tex | 4 ++-- Manual/Translations/IT/Description/HolSmt.tex | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) 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