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