src/HOL/Tools/SMT/smt_solver.ML

 
     val ls = rev (snd (chop_while (equal "") (rev res)))
     val _ = C.trace_msg ctxt (pretty "Result:") ls
 
     val _ = null ls andalso return_code <> 0 andalso
-      raise SMT_Failure.SMT (SMT_Failure.Solver_Crashed return_code)
+      raise SMT_Failure.SMT (SMT_Failure.Abnormal_Termination return_code)
   in ls end
 
 end
 
 fun trace_assms ctxt = C.trace_msg ctxt (Pretty.string_of o