# HG changeset patch
# User blanchet
# Date 1570719577 -7200
# Node ID ed89f20de7abb9e7b20bf87d6b0f832e2528f5ad
# Parent  13d6b561b0ea4583cb2a2624dd68009e3054cbb3
updated veriT part of Sledgehammer documentation

diff -r 13d6b561b0ea -r ed89f20de7ab src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Thu Oct 10 16:37:52 2019 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Thu Oct 10 16:59:37 2019 +0200
@@ -158,10 +158,10 @@
 \begin{sloppy}
 \begin{enum}
 \item[\labelitemi] If you installed an official Isabelle package, it should
-already include properly setup executables for CVC4, E, SPASS, Vampire, veriT,
-and Z3, ready to use. To use Vampire, you must confirm that you are a
-noncommercial user, as indicated by the message that is displayed when
-Sledgehammer is invoked the first time.
+already include properly setup executables for CVC4, E, SPASS, Vampire, and Z3,
+ready to use. To use Vampire, you must confirm that you are a noncommercial
+user, as indicated by the message that is displayed when Sledgehammer is
+invoked the first time.
 
 \item[\labelitemi] Alternatively, you can download the Isabelle-aware CVC3,
 CVC4, E, SPASS, Vampire, and Z3 binary packages from \download. Extract the
@@ -200,7 +200,7 @@
 variable \texttt{CVC3\_\allowbreak SOLVER}, \texttt{CVC4\_\allowbreak SOLVER},
 \texttt{VERIT\_\allowbreak SOLVER}, or \texttt{Z3\_SOLVER} to the complete path
 of the executable, \emph{including the file name}. Sledgehammer has been tested
-with CVC3 2.2 and 2.4.1, CVC4 1.5-prerelease, veriT smtcomp2014, and Z3 4.3.2.
+with CVC3 2.2 and 2.4.1, CVC4 1.5-prerelease, veriT smtcomp2019, and Z3 4.3.2.
 Since Z3's output format is somewhat unstable, other versions of the solver
 might not work well with Sledgehammer. Ideally, also set
 \texttt{CVC3\_VERSION}, \texttt{CVC4\_VERSION}, \texttt{VERIT\_VERSION}, or
@@ -833,7 +833,7 @@
 It is specifically designed to produce detailed proofs for reconstruction in
 proof assistants. To use veriT, set the environment variable
 \texttt{VERIT\_SOLVER} to the complete path of the executable, including the
-file name. Sledgehammer has been tested with version smtcomp2014.
+file name. Sledgehammer has been tested with version smtcomp2019.
 
 \item[\labelitemi] \textbf{\textit{z3}:} Z3 is an SMT solver developed at
 Microsoft Research \cite{z3}. To use Z3, set the environment variable