Skip to content

Commit

Permalink
HolSmt: update docs wrt tested solver versions
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
someplaceguy authored and mn200 committed Jan 24, 2024
1 parent 63a6b23 commit 29d5e1c
Show file tree
Hide file tree
Showing 2 changed files with 4 additions and 4 deletions.
4 changes: 2 additions & 2 deletions Manual/Description/HolSmt.tex
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 2 additions & 2 deletions Manual/Translations/IT/Description/HolSmt.tex
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 29d5e1c

Please sign in to comment.