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