# HG changeset patch
# User blanchet
# Date 1428511736 -7200
# Node ID a965060dcbb8a9f48a28fe73ebb7b017f986f01e
# Parent  372ddff012442750c1fc7adbd61dd8555d1884f1
updated docs to Z3 open source

diff -r 372ddff01244 -r a965060dcbb8 src/Doc/Sledgehammer/document/root.tex
--- 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