
diff -r 9d5662acb19c -r c5cfead18464 src/Doc/Sledgehammer/document/root.tex
--- 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




