# HG changeset patch
# User blanchet
# Date 1396538162 -7200
# Node ID 9bb2856cc8451400a97afb988865063b2c27b70a
# Parent  d8ecce5d51cdcd3706ececdf4fc19abf6167f883
don't pass Vampire option that doesn't exist anymore (and that wasn't strictly necessary with older Vampires)

diff -r d8ecce5d51cd -r 9bb2856cc845 src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Thu Apr 03 17:00:14 2014 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Thu Apr 03 17:16:02 2014 +0200
@@ -208,7 +208,7 @@
 versions might not work well with Sledgehammer. Ideally,
 you should also set \texttt{E\_VERSION}, \texttt{LEO2\_VERSION},
 \texttt{SATALLAX\_VERSION}, \texttt{SPASS\_VERSION}, or
-\texttt{VAMPIRE\_VERSION} to the prover's version number (e.g., ``1.8'').
+\texttt{VAMPIRE\_VERSION} to the prover's version number (e.g., ``3.0'').
 
 Similarly, if you want to build CVC3, or found a
 Yices or Z3 executable somewhere (e.g.,
@@ -897,7 +897,7 @@
 \cite{riazanov-voronkov-2002}. To use Vampire, set the environment variable
 \texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{vampire}
 executable and \texttt{VAMPIRE\_VERSION} to the version number (e.g.,
-``2.6''). Sledgehammer has been tested with versions 0.6 to 3.0.
+``3.0''). Sledgehammer has been tested with versions 0.6 to 3.0.
 Versions strictly above 1.8 support the TPTP typed first-order format (TFF0).
 
 \item[\labelitemi] \textbf{\textit{yices}:} Yices is an SMT solver developed at
diff -r d8ecce5d51cd -r 9bb2856cc845 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Thu Apr 03 17:00:14 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu Apr 03 17:16:02 2014 +0200
@@ -559,7 +559,7 @@
 
 (* Vampire *)
 
-(* Vampire 1.8 has TFF support, but the support was buggy until revision
+(* Vampire 1.8 has TFF0 support, but the support was buggy until revision
    1435 (or shortly before). *)
 fun is_vampire_at_least_1_8 () = string_ord (getenv "VAMPIRE_VERSION", "1.8") <> LESS
 fun is_vampire_beyond_1_8 () = string_ord (getenv "VAMPIRE_VERSION", "1.8") = GREATER
@@ -574,9 +574,8 @@
        " --proof tptp --output_axiom_names on" ^
        (if is_vampire_at_least_1_8 () then
           (* Cf. p. 20 of http://www.complang.tuwien.ac.at/lkovacs/Cade23_Tutorial_Slides/Session2_Slides.pdf *)
-          " --forced_options propositional_to_bdd=off" ^
           (if full_proof then
-             ":splitting=off:equality_proxy=off:general_splitting=off\
+             "--forced_options splitting=off:equality_proxy=off:general_splitting=off\
              \:inequality_splitting=0:naming=0"
            else
              "")