src/HOL/SMT/Tools/z3_solver.ML

     val (ls, l) = the_default ([], "") (try split_last (filter_out jnk output))
   in
     if String.isPrefix "unsat" l then ls
     else if String.isPrefix "sat" l then raise_cex true recon ls
     else if String.isPrefix "unknown" l then raise_cex false recon ls
-    else error (solver_name ^ " failed")
+    else raise SMT_Solver.SMT (solver_name ^ " failed")
   end
 
 fun core_oracle ({output, recon, ...} : SMT_Solver.proof_data) =
   check_unsat recon output
   |> K @{cprop False}