--- a/doc-src/Sledgehammer/sledgehammer.tex Tue Aug 23 15:15:43 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Tue Aug 23 15:18:46 2011 +0200
@@ -762,12 +762,13 @@
\item[$\bullet$] \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
-name, and set \texttt{Z3\_NON\_COMMERCIAL=yes} to confirm that you are a
+name, and set \texttt{Z3\_NON\_COMMERCIAL} to ``yes'' to confirm that you are a
noncommercial user. Sledgehammer has been tested with versions 2.7 to 2.18.
\item[$\bullet$] \textbf{\textit{z3\_atp}:} This version of Z3 pretends to be an
-ATP, exploiting Z3's undocumented support for the TPTP format. It is included
-for experimental purposes. It requires version 2.18 or above.
+ATP, exploiting Z3's support for the TPTP untyped and many-typed first-order
+formats (FOF and TFF). It is included for experimental purposes. It requires
+version 3.0 or above.
\end{enum}
In addition, the following remote provers are supported: