# HG changeset patch
# User boehmes
# Date 1289573770 -3600
# Node ID 25f2661442062748abfd189449dde7f8fcec2769
# Parent  db5f14910dceeec901b53c9e57aedaddc631f850
turned SMT counterexamples into verbose messages (they had been swallowed before, following the state of smt_trace -- which is off by default), because they might be useful for the user

diff -r db5f14910dce -r 25f266144206 src/HOL/Tools/SMT/smt_failure.ML
--- a/src/HOL/Tools/SMT/smt_failure.ML	Fri Nov 12 15:56:08 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_failure.ML	Fri Nov 12 15:56:10 2010 +0100
@@ -26,7 +26,9 @@
 
 fun string_of_failure ctxt (Counterexample (real, ex)) =
       let
-        val msg = (if real then "C" else "Potential c") ^ "ounterexample found"
+        val msg =
+          if real then "Counterexample found (possibly spurious)"
+          else "Potential counterexample found"
       in
         if null ex then msg
         else Pretty.string_of (Pretty.big_list (msg ^ ":")
diff -r db5f14910dce -r 25f266144206 src/HOL/Tools/SMT/smt_solver.ML
--- a/src/HOL/Tools/SMT/smt_solver.ML	Fri Nov 12 15:56:08 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Fri Nov 12 15:56:10 2010 +0100
@@ -342,8 +342,12 @@
       val str_of = SMT_Failure.string_of_failure ctxt'
       fun safe_solve irules =
         if pass_exns then SOME (solve irules)
-        else (SOME (solve irules) handle SMT_Failure.SMT fail =>
-          (C.trace_msg ctxt' (prefix tag o str_of) fail; NONE))
+        else (SOME (solve irules)
+          handle
+            SMT_Failure.SMT (fail as SMT_Failure.Counterexample _) =>
+              (C.verbose_msg ctxt' (prefix tag o str_of) fail; NONE)
+          | SMT_Failure.SMT fail =>
+              (C.trace_msg ctxt' (prefix tag o str_of) fail; NONE))
     in
       safe_solve (map (pair ~1) (rules @ prems))
       |> (fn SOME thm => Tactic.rtac thm 1 | _ => Tactical.no_tac)