src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML

 
     val (preferred_methss, message) =
       (case outcome of
         NONE =>
         let
+          val smt_method = smt_proofs <> SOME false
           val preferred_methss =
-            (SMT_Method, bunches_of_proof_methods try0 (smt_proofs <> SOME false) false liftingN)
+            (if smt_method then SMT_Method else Metis_Method (NONE, NONE),
+             bunches_of_proof_methods try0 smt_method false liftingN)
         in
           (preferred_methss,
            fn preplay =>
              let
                val _ = if verbose then Output.urgent_message "Generating proof text..." else ()