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.
Z3 prints so many warnings that the very informative abnormal termination exception hardly ever gets raised -- better be more aggressive here
authorblanchet
Thu, 26 Jul 2012 11:08:16 +0200
changeset 48534 2307efbfc554
parent 48533 5ada9fd7507b
child 48535 619531d87ce4
Z3 prints so many warnings that the very informative abnormal termination exception hardly ever gets raised -- better be more aggressive here
src/HOL/Tools/SMT/smt_solver.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle