# HG changeset patch
# User desharna
# Date 1648743272 -7200
# Node ID 136f79711c2a33340182b5b57a3b5c7edb276c50
# Parent  1bad148d894fdf71ce30992268a84439736af2ae
tuned sledgehammer to suggest (smt (verit)) on failing smt preplay for all but Z3

diff -r 1bad148d894f -r 136f79711c2a src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Tue Mar 29 13:31:45 2022 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Thu Mar 31 18:14:32 2022 +0200
@@ -142,7 +142,7 @@
           val _ = found_proof name;
           val preferred =
             if smt_proofs then
-              SMT_Method (if name = "verit" then SMT_Verit "default" else SMT_Z3)
+              SMT_Method (if name = "z3" then SMT_Z3 else SMT_Verit "default")
             else
               Metis_Method (NONE, NONE);
           val methss = bunches_of_proof_methods ctxt try0 smt_proofs false liftingN;