# HG changeset patch
# User blanchet
# Date 1423662486 -3600
# Node ID 49ca7836ae818bd52d7b023c3736310af03b42f1
# Parent  b468e0f8da2adb0bc9d080d6ab29263dbc976a4e
tuned default provers

diff -r b468e0f8da2a -r 49ca7836ae81 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Wed Feb 11 12:01:56 2015 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Wed Feb 11 14:48:06 2015 +0100
@@ -27,7 +27,8 @@
 open Sledgehammer_MaSh
 open Sledgehammer
 
-(* val cvc3N = "cvc3" *)
+val cvc4N = "cvc4"
+val veritN = "verit"
 val z3N = "z3"
 
 val runN = "run"
@@ -180,7 +181,7 @@
 
 (* The first ATP of the list is used by Auto Sledgehammer. *)
 fun default_provers_param_value mode ctxt =
-  [eN, spassN, z3N, vampireN, e_sineN]
+  [spassN, cvc4N, vampireN, eN, z3N, veritN, e_sineN]
   |> map_filter (remotify_prover_if_not_installed ctxt)
   (* In "try" mode, leave at least one thread to another slow tool (e.g. Nitpick) *)
   |> take (Multithreading.max_threads_value () - (if mode = Try then 1 else 0))