diff -r 402afc68f2f9 -r e732c98b02e6 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Mon Nov 30 22:00:23 2020 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Tue Dec 01 15:29:54 2020 +0100
@@ -202,7 +202,7 @@
           val _ = found_proof ();
           val preferred =
             if smt_proofs then
-              SMT_Method (if name = "verit" then SMT_Verit "default" else SMT_Default)
+              SMT_Method (if name = "verit" then SMT_Verit "default" else SMT_Z3)
             else
               Metis_Method (NONE, NONE);
           val methss = bunches_of_proof_methods ctxt try0 smt_proofs false liftingN;