# HG changeset patch
# User blanchet
# Date 1361370379 -3600
# Node ID 265dca70d8b545b2e41e54edcfebcaccab3ce303
# Parent  20f6d400cc68ee2c6669d3471cd464e6b4c56960
upgraded to Alt-Ergo 0.95

diff -r 20f6d400cc68 -r 265dca70d8b5 src/Doc/Sledgehammer/document/root.tex
--- 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
diff -r 20f6d400cc68 -r 265dca70d8b5 src/HOL/Tools/ATP/atp_systems.ML
--- 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 =