# HG changeset patch
# User blanchet
# Date 1626683894 -7200
# Node ID 462d652ad9101fbf2d4201763b6b97afc72f4ffe
# Parent  302994f5a3c22fa863aebb90d0862ce71460ecd7
use Vampire's clausifier with iProver, now that E's is no longer supported

diff -r 302994f5a3c2 -r 462d652ad910 src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Mon Jul 19 10:37:48 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Mon Jul 19 10:38:14 2021 +0200
@@ -319,8 +319,8 @@
 val iprover_config : atp_config =
   {exec = (["IPROVER_HOME"], ["iproveropt", "iprover"]),
    arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => fn _ =>
-     ["--clausifier \"$E_HOME\"/eprover " ^
-      "--clausifier_options \"--tstp-format --silent --cnf\" " ^
+     ["--clausifier \"$VAMPIRE_HOME\"/vampire " ^
+      "--clausifier_options \"--mode clausify\" " ^
       "--time_out_real " ^ string_of_real (Time.toReal timeout) ^ " " ^ File.bash_path problem],
    proof_delims = tstp_proof_delims,
    known_failures =