# HG changeset patch # User blanchet # Date 1416828913 -3600 # Node ID c5cfead18464f4a259e74cc66ca8b4d5903fa00e # Parent 9d5662acb19c6d7eca5d0bc5cac14ad104fa6771 update CVC4 version docs 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