1.1 --- a/doc-src/Sledgehammer/sledgehammer.tex	Wed Apr 18 10:53:27 2012 +0200
     1.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex	Wed Apr 18 10:53:27 2012 +0200
     1.3 @@ -195,7 +195,7 @@
     1.4  \texttt{LEO2\_HOME}, \texttt{SATALLAX\_HOME}, \texttt{SPASS\_HOME}, or
     1.5  \texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{eproof},
     1.6  \texttt{leo}, \texttt{satallax}, \texttt{SPASS}, or \texttt{vampire} executable.
     1.7 -Sledgehammer has been tested with E 1.0 to 1.4, LEO-II 1.2.9, Satallax 2.2,
     1.8 +Sledgehammer has been tested with E 1.0 to 1.4, LEO-II 1.2.9, Satallax 2.2 and 2.3,
     1.9  SPASS 3.5 and 3.7, and Vampire 0.6, 1.0, and 1.8%
    1.10  \footnote{Following the rewrite of Vampire, the counter for version numbers was
    1.11  reset to 0; hence the (new) Vampire versions 0.6, 1.0, and 1.8 are more recent
    1.12 @@ -213,7 +213,7 @@
    1.13  set the environment variable \texttt{CVC3\_\allowbreak SOLVER},
    1.14  \texttt{YICES\_SOLVER}, or \texttt{Z3\_SOLVER} to the complete path of
    1.15  the executable, \emph{including the file name}. Sledgehammer has been tested
    1.16 -with Alt-Ergo 0.93, CVC3 2.2, Yices 1.0.28, and Z3 3.0 to 3.2.
    1.17 +with Alt-Ergo 0.93, CVC3 2.2 and 2.4.1, Yices 1.0.28 and 1.0.33, and Z3 3.0 to 3.2.
    1.18  Since the SMT solvers' output formats are somewhat unstable, other
    1.19  versions of the solvers might not work well with Sledgehammer. Ideally,
    1.20  also set \texttt{CVC3\_VERSION}, \texttt{YICES\_VERSION}, or
    1.21 @@ -633,7 +633,7 @@
    1.22  \item[\labelitemi] \textbf{\textit{messages}:} Redisplays recent messages issued
    1.23  by Sledgehammer. This allows you to examine results that might have been lost
    1.24  due to Sledgehammer's asynchronous nature. The \qty{num} argument specifies a
    1.25 -limit on the number of messages to display (5 by default).
    1.26 +limit on the number of messages to display (10 by default).
    1.27  
    1.28  \item[\labelitemi] \textbf{\textit{supported\_provers}:} Prints the list of
    1.29  automatic provers supported by Sledgehammer. See \S\ref{installation} and