--- a/src/Doc/Sledgehammer/document/root.tex Wed Feb 20 15:12:38 2013 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex Wed Feb 20 15:26:19 2013 +0100
@@ -223,7 +223,7 @@
for Alt-Ergo, set the
environment variable \texttt{WHY3\_HOME} to the directory that contains the
\texttt{why3} executable.
-Sledgehammer has been tested with Alt-Ergo 0.93 and 0.94, CVC3 2.2 and 2.4.1,
+Sledgehammer has been tested with Alt-Ergo 0.95, 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
formats are somewhat unstable, other versions of the solvers might not work well
with Sledgehammer. Ideally, also set \texttt{CVC3\_VERSION},
@@ -843,7 +843,7 @@
It supports the TPTP polymorphic typed first-order format (TFF1) via Why3
\cite{why3}. It is included for experimental purposes. To use Alt-Ergo, set the
environment variable \texttt{WHY3\_HOME} to the directory that contains the
-\texttt{why3} executable. Sledgehammer has been tested with Alt-Ergo 0.93 and an
+\texttt{why3} executable. Sledgehammer has been tested with Alt-Ergo 0.95 and an
unidentified development version of Why3.
\item[\labelitemi] \textbf{\textit{cvc3}:} CVC3 is an SMT solver developed by
--- a/src/HOL/Tools/ATP/atp_systems.ML Wed Feb 20 15:12:38 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML Wed Feb 20 15:26:19 2013 +0100
@@ -207,7 +207,7 @@
val alt_ergo_config : atp_config =
{exec = (["WHY3_HOME"], ["why3"]),
arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
- "--format tff1 --prover alt-ergo --timelimit " ^
+ "--format tptp --prover 'Alt-Ergo,0.95,' --timelimit " ^
string_of_int (to_secs 1 timeout) ^ " " ^ file_name,
proof_delims = [],
known_failures =