tuned sledgehammer to suggest (smt (verit)) on failing smt preplay for all but Z3

--- 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;