Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
don't be so verbose about SMT solver failures
authorblanchet
Tue, 10 Sep 2013 15:56:51 +0200
changeset 53500 53b9326196fe
parent 53499 abec1d118bc9
child 53501 b49bfa77958a
don't be so verbose about SMT solver failures
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Sep 10 14:02:49 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Sep 10 15:56:51 2013 +0200
@@ -1122,7 +1122,7 @@
               (if show_filter then " " ^ quote fact_filter else "") ^
               " fact" ^ plural_s num_facts
             val _ =
-              if verbose andalso is_some outcome then
+              if debug then
                 quote name ^ " invoked with " ^
                 num_of_facts fact_filter num_facts ^ ": " ^
                 string_of_failure (failure_of_smt_failure (the outcome)) ^
isabelle