# HG changeset patch
# User blanchet
# Date 1343293696 -7200
# Node ID 2307efbfc554d87a3be1b70796058ab60f8e2d12
# Parent  5ada9fd7507bdb232ffc1a0f0bba30838e26fe1d
Z3 prints so many warnings that the very informative abnormal termination exception hardly ever gets raised -- better be more aggressive here

diff -r 5ada9fd7507b -r 2307efbfc554 src/HOL/Tools/SMT/smt_solver.ML
--- a/src/HOL/Tools/SMT/smt_solver.ML	Thu Jul 26 11:07:27 2012 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Thu Jul 26 11:08:16 2012 +0200
@@ -99,7 +99,7 @@
     val ls = rev (snd (chop_while (equal "") (rev res)))
     val _ = SMT_Config.trace_msg ctxt (pretty "Result:") ls
 
-    val _ = null ls andalso return_code <> 0 andalso
+    val _ = return_code <> 0 andalso
       raise SMT_Failure.SMT (SMT_Failure.Abnormal_Termination return_code)
   in ls end