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