--- a/src/Doc/Sledgehammer/document/root.tex Sat Nov 22 15:34:00 2014 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex Mon Nov 24 12:35:13 2014 +0100
@@ -216,9 +216,9 @@
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.2, veriT smtcomp2014, 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
+with CVC3 2.2 and 2.4.1, CVC4 1.5-prerelease, veriT smtcomp2014, 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
\texttt{Z3\_NEW\_VERSION} to the solver's version number (e.g., ``4.3.2'').
\end{enum}
@@ -794,7 +794,7 @@
CVC3. To use CVC4, set the environment variable \texttt{CVC4\_SOLVER} to the
complete path of the executable, including the file name, or install the
prebuilt CVC4 package from \download. Sledgehammer has been tested with version
-1.2.
+1.5-prerelease.
\item[\labelitemi] \textbf{\textit{e}:} E is a first-order resolution prover
developed by Stephan Schulz \cite{schulz-2002}. To use E, set the environment