# HG changeset patch
# User blanchet
# Date 1300985367 -3600
# Node ID 062381c5f9f8b2d88ef1d80640a33bf8fa067932
# Parent  447fa058ab222c1ce906dbe34c3dddcabf961568
more precise failure reporting in Sledgehammer/SMT

diff -r 447fa058ab22 -r 062381c5f9f8 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Mar 24 17:49:27 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Mar 24 17:49:27 2011 +0100
@@ -495,7 +495,9 @@
 val smt_failures =
   remote_smt_failures @ z3_wrapper_failures @ z3_failures @ unix_failures
 
-fun failure_from_smt_failure (SMT_Failure.Counterexample _) = Unprovable
+
+fun failure_from_smt_failure (SMT_Failure.Counterexample {is_real_cex, ...}) =
+    if is_real_cex then Unprovable else IncompleteUnprovable
   | failure_from_smt_failure SMT_Failure.Time_Out = TimedOut
   | failure_from_smt_failure (SMT_Failure.Abnormal_Termination code) =
     (case AList.lookup (op =) smt_failures code of