# HG changeset patch
# User blanchet
# Date 1402478926 -7200
# Node ID cc59d49bdf64cd9fd74b3c37eddbdb0e0fdfc9fd
# Parent  5d61d875076a90c2dd03f21a7ae3513ce64cab2d
updated docs w.r.t. Z3

diff -r 5d61d875076a -r cc59d49bdf64 src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Wed Jun 11 11:28:46 2014 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Wed Jun 11 11:28:46 2014 +0200
@@ -221,11 +221,11 @@
 \texttt{YICES\_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,
-Yices 1.0.28 and 1.0.33, and Z3 3.0 to 4.0. Since the SMT solvers' output
+Yices 1.0.28 and 1.0.33, and Z3 4.3.2. Since the SMT solvers' output
 formats are somewhat unstable, other versions of the solvers might not work well
 with Sledgehammer. Ideally, also set \texttt{CVC3\_VERSION},
-\texttt{YICES\_VERSION}, or \texttt{Z3\_VERSION} to the solver's version number
-(e.g., ``4.0'').
+\texttt{YICES\_VERSION}, or \texttt{Z3\_NEW\_VERSION} to the solver's version
+number (e.g., ``4.3.2'').
 \end{enum}
 \end{sloppy}
 
@@ -906,20 +906,13 @@
 
 \item[\labelitemi] \textbf{\textit{z3}:} Z3 is an SMT solver developed at
 Microsoft Research \cite{z3}. To use Z3, set the environment variable
-\texttt{Z3\_SOLVER} to the complete path of the executable, including the file
+\texttt{Z3\_NEW\_SOLVER} to the complete path of the executable, including the file
 name, and set \texttt{Z3\_NON\_COMMERCIAL} to \textit{yes} to confirm that you are a
 noncommercial user---either in the environment in which Isabelle is
 launched, in your \texttt{\$ISABELLE\_HOME\_USER/etc/settings} file, or
 via the ``Z3 Non Commercial'' option under ``Plugins > Plugin Options
 > Isabelle > General'' in Isabelle/jEdit. Sledgehammer has been tested with
-versions 3.0, 3.1, 3.2, and 4.0.
-
-\item[\labelitemi] \textbf{\textit{z3\_new}:} Newer versions of Z3 (e.g., 4.3)
-are treated as a different prover by Isabelle. To use these, set the environment
-variable \texttt{Z3\_NEW\_SOLVER} to the complete path of the executable,
-including the file name. You also need to set \texttt{Z3\_NON\_COMMERCIAL} to
-\textit{yes}, as described above. Sledgehammer has been tested with a pre-release
-version of 4.3.2.
+a pre-release version of 4.3.2.
 \end{enum}
 
 \item[\labelitemi] \textbf{\textit{z3\_tptp}:} This version of Z3 pretends to be