# HG changeset patch
# User desharna
# Date 1632818838 -7200
# Node ID d8dc8fdc46fc913da9fbd257ca21c4bb189431db
# Parent  3301c0d8b56032577e6bcadf9538b3c0fa8b7f3d
prefer veriT over Z3 in sledgehammer

diff -r 3301c0d8b560 -r d8dc8fdc46fc src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Tue Sep 28 10:38:36 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Tue Sep 28 10:47:18 2021 +0200
@@ -177,7 +177,7 @@
 
 (* The first ATP of the list is used by Auto Sledgehammer. *)
 fun default_provers_param_value mode ctxt =
-  [cvc4N, vampireN, z3N, eN, spassN, veritN, zipperpositionN]
+  [cvc4N, vampireN, veritN, eN, spassN, z3N, zipperpositionN]
   |> 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 () - (if mode = Try then 1 else 0))
diff -r 3301c0d8b560 -r d8dc8fdc46fc src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Tue Sep 28 10:38:36 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Tue Sep 28 10:47:18 2021 +0200
@@ -189,9 +189,8 @@
 
     val smt_methodss =
       if smt_proofs then
-        [SMT_Method SMT_Z3 ::
-         map (fn strategy => SMT_Method (SMT_Verit strategy))
-           (Verit_Proof.all_veriT_stgies (Context.Proof ctxt))]
+        [map (SMT_Method o SMT_Verit) (Verit_Proof.all_veriT_stgies (Context.Proof ctxt)),
+         [SMT_Method SMT_Z3]]
       else
         []
   in