--- a/src/Doc/Sledgehammer/document/root.tex Wed Apr 08 18:47:38 2015 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Wed Apr 08 18:48:56 2015 +0200
@@ -167,12 +167,6 @@
already include properly setup executables for CVC4, E, SPASS, and Z3, ready to use.%
\footnote{Vampire's license prevents us from doing the same for
this otherwise remarkable tool.}
-For Z3, you must additionally set the variable
-\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.
\item[\labelitemi] Alternatively, you can download the Isabelle-aware CVC3,
CVC4, E, SPASS, and Z3 binary packages from \download. Extract the archives,
@@ -221,7 +215,7 @@
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'').
+\texttt{Z3\_VERSION} to the solver's version number (e.g., ``4.4.0'').
\end{enum}
\end{sloppy}
@@ -867,13 +861,8 @@
\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\_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
-a pre-release version of 4.3.2.
+\texttt{Z3\_SOLVER} to the complete path of the executable, including the
+file name. Sledgehammer has been tested with a pre-release version of 4.4.0.
\item[\labelitemi] \textbf{\textit{z3\_tptp}:} This version of Z3 pretends to be
an ATP, exploiting Z3's support for the TPTP untyped and typed first-order