diff -r eeaa59fb5ad8 -r 47ff261431c4 src/HOL/Tools/SMT/smt_solver.ML
--- a/src/HOL/Tools/SMT/smt_solver.ML	Tue Nov 30 00:12:29 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Tue Nov 30 18:22:43 2010 +0100
@@ -19,7 +19,7 @@
     interface: interface,
     outcome: string -> string list -> outcome * string list,
     cex_parser: (Proof.context -> SMT_Translate.recon -> string list ->
-      term list) option,
+      term list * term list) option,
     reconstruct: (Proof.context -> SMT_Translate.recon -> string list ->
       (int list * thm) * Proof.context) option }
 
@@ -65,7 +65,7 @@
   interface: interface,
   outcome: string -> string list -> outcome * string list,
   cex_parser: (Proof.context -> SMT_Translate.recon -> string list ->
-    term list) option,
+    term list * term list) option,
   reconstruct: (Proof.context -> SMT_Translate.recon -> string list ->
     (int list * thm) * Proof.context) option }
 
@@ -260,9 +260,14 @@
         then the reconstruct ctxt recon ls
         else (([], ocl ()), ctxt)
     | (result, ls) =>
-        let val ts = (case cex_parser of SOME f => f ctxt recon ls | _ => [])
-        in
-          raise SMT_Failure.SMT (SMT_Failure.Counterexample (result = Sat, ts))
+        let
+          val (ts, us) =
+            (case cex_parser of SOME f => f ctxt recon ls | _ => ([], []))
+         in
+          raise SMT_Failure.SMT (SMT_Failure.Counterexample {
+            is_real_cex = (result = Sat),
+            free_constraints = ts,
+            const_defs = us})
         end)
 
   val cfalse = Thm.cterm_of @{theory} (@{const Trueprop} $ @{const False})
@@ -351,15 +356,14 @@
     let
       fun solve irules = snd (smt_solver NONE ctxt' irules)
       val tag = "Solver " ^ C.solver_of ctxt' ^ ": "
-      val str_of = SMT_Failure.string_of_failure ctxt'
+      val str_of = prefix tag o 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 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))
+              (C.verbose_msg ctxt' str_of fail; NONE)
+          | SMT_Failure.SMT fail => (C.trace_msg ctxt' str_of fail; NONE))
     in
       safe_solve (map (pair ~1) (rules @ prems))
       |> (fn SOME thm => Tactic.rtac thm 1 | _ => Tactical.no_tac)