Mercurial Mercurial > wneuper > isa / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | bz2 | gz | help
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 495492307efbfc554
parent 49548 5ada9fd7507b
child 49550 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 
     1.1 --- a/src/HOL/Tools/SMT/smt_solver.ML	Thu Jul 26 11:07:27 2012 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_solver.ML	Thu Jul 26 11:08:16 2012 +0200
     1.3 @@ -99,7 +99,7 @@
     1.4      val ls = rev (snd (chop_while (equal "") (rev res)))
     1.5      val _ = SMT_Config.trace_msg ctxt (pretty "Result:") ls
     1.6  
     1.7 -    val _ = null ls andalso return_code <> 0 andalso
     1.8 +    val _ = return_code <> 0 andalso
     1.9        raise SMT_Failure.SMT (SMT_Failure.Abnormal_Termination return_code)
    1.10    in ls end
    1.11
wneuper/isa