# HG changeset patch
# User blanchet
# Date 1354564532 -3600
# Node ID 20c69b00e73c470c0c61b1bd588e645dc5370609
# Parent  2c7479865e07f441ea0d1f68bf10b872f06f046c
tweak SPASS default a tiny bit, so that a more interesting heuristic is chosen when "slicing=false" (for experiments)

diff -r 2c7479865e07 -r 20c69b00e73c src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Mon Dec 03 20:43:40 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Mon Dec 03 20:55:32 2012 +0100
@@ -437,10 +437,11 @@
 (* SPASS *)
 
 val spass_H1SOS = "-Heuristic=1 -SOS"
+val spass_H2 = "-Heuristic=2"
 val spass_H2LR0LT0 = "-Heuristic=2 -LR=0 -LT=0"
-val spass_H2SOS = "-Heuristic=2 -SOS"
 val spass_H2NuVS0 = "-Heuristic=2 -RNuV=1 -Sorts=0"
 val spass_H2NuVS0Red2 = "-Heuristic=2 -RNuV=1 -Sorts=0 -RFRew=2 -RBRew=2 -RTaut=2"
+val spass_H2SOS = "-Heuristic=2 -SOS"
 
 (* FIXME: Make "SPASS_NEW_HOME" legacy. *)
 val spass_config : atp_config =
@@ -469,7 +470,7 @@
       (0.1000, ((1000, DFG Monomorphic, "mono_native", liftingN, true), spass_H1SOS)),
       (0.1000, ((150, DFG Monomorphic, "poly_guards??", liftingN, false), spass_H2NuVS0Red2)),
       (0.1000, ((300, DFG Monomorphic, "mono_native", combsN, true), spass_H2SOS)),
-      (0.1000, ((100, DFG Monomorphic, "mono_native", combs_and_liftingN, true), ""))],
+      (0.1000, ((100, DFG Monomorphic, "mono_native", combs_and_liftingN, true), spass_H2))],
    best_max_mono_iters = default_max_mono_iters,
    best_max_new_mono_instances = default_max_new_mono_instances}