# HG changeset patch
# User blanchet
# Date 1319193860 -7200
# Node ID 5509362b924bf8801cd64af6606904696e218baa
# Parent  28b076e0bea8f59e4497fb57353a1db0d8443787
disable Vampire's BDD optimization, which sometimes yields so huge proofs that this causes problems for reconstruction

diff -r 28b076e0bea8 -r 5509362b924b src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Fri Oct 21 11:17:16 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Fri Oct 21 12:44:20 2011 +0200
@@ -344,7 +344,8 @@
    required_execs = [],
    arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
      "--mode casc -t " ^ string_of_int (to_secs 1 timeout) ^
-     " --proof tptp --output_axiom_names on \
+     " --proof tptp --output_axiom_names on\
+     \ --forced_options propositional_to_bdd=off\
      \ --thanks \"Andrei and Krystof\" --input_file"
      |> sos = sosN ? prefix "--sos on ",
    proof_delims =