# HG changeset patch
# User boehmes
# Date 1289579323 -3600
# Node ID b8482ff0bc922286a5be06bb2960c30400dbbeee
# Parent  516a367eb38cf311b281ad0e8224a0f185b6fe31
check the return code of the SMT solver and raise an exception if the prover failed

diff -r 516a367eb38c -r b8482ff0bc92 src/HOL/Tools/SMT/smt_failure.ML
--- a/src/HOL/Tools/SMT/smt_failure.ML	Fri Nov 12 15:56:11 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_failure.ML	Fri Nov 12 17:28:43 2010 +0100
@@ -10,6 +10,7 @@
     Counterexample of bool * term list |
     Time_Out |
     Out_Of_Memory |
+    Solver_Crashed of int |
     Other_Failure of string
   val string_of_failure: Proof.context -> failure -> string
   exception SMT of failure
@@ -22,6 +23,7 @@
   Counterexample of bool * term list |
   Time_Out |
   Out_Of_Memory |
+  Solver_Crashed of int |
   Other_Failure of string
 
 fun string_of_failure ctxt (Counterexample (real, ex)) =
@@ -36,6 +38,8 @@
       end
   | string_of_failure _ Time_Out = "Timed out"
   | string_of_failure _ Out_Of_Memory = "Ran out of memory"
+  | string_of_failure _ (Solver_Crashed err) =
+      "Solver crashed with error code " ^ string_of_int err
   | string_of_failure _ (Other_Failure msg) = msg
 
 exception SMT of failure
diff -r 516a367eb38c -r b8482ff0bc92 src/HOL/Tools/SMT/smt_solver.ML
--- a/src/HOL/Tools/SMT/smt_solver.ML	Fri Nov 12 15:56:11 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Fri Nov 12 17:28:43 2010 +0100
@@ -106,24 +106,25 @@
   map File.shell_quote (solver @ args) @
   [File.shell_path problem_path, "2>&1", ">", File.shell_path proof_path])
 
+fun check_return_code {output, redirected_output, return_code} =
+  if return_code <> 0 then
+    raise SMT_Failure.SMT (SMT_Failure.Solver_Crashed return_code)
+  else (redirected_output, output)
+
 fun run ctxt cmd args input =
   (case C.certificates_of ctxt of
-    NONE =>
-      let
-        val {output, redirected_output, ...} =
-          Cache_IO.run (make_cmd (choose cmd) args) input
-      in (redirected_output, output) end 
+    NONE => Cache_IO.run (make_cmd (choose cmd) args) input
   | SOME certs =>
       (case Cache_IO.lookup certs input of
         (NONE, key) =>
-          if Config.get ctxt C.fixed
-          then error ("Bad certificates cache: missing certificate")
-          else Cache_IO.run_and_cache certs key (make_cmd (choose cmd) args)
-            input
+          if Config.get ctxt C.fixed then
+            error ("Bad certificates cache: missing certificate")
+          else
+            Cache_IO.run_and_cache certs key (make_cmd (choose cmd) args) input
       | (SOME output, _) =>
          (tracing ("Using cached certificate from " ^
             File.shell_path (Cache_IO.cache_path_of certs) ^ " ...");
-          output)))
+          output))) |> check_return_code
 
 in
 
diff -r 516a367eb38c -r b8482ff0bc92 src/Tools/cache_io.ML
--- a/src/Tools/cache_io.ML	Fri Nov 12 15:56:11 2010 +0100
+++ b/src/Tools/cache_io.ML	Fri Nov 12 17:28:43 2010 +0100
@@ -9,18 +9,20 @@
   (*IO wrapper*)
   val with_tmp_file: string -> (Path.T -> 'a) -> 'a
   val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
-  val run: (Path.T -> Path.T -> string) -> string ->
-    {output: string list, redirected_output: string list, return_code: int}
+  type result = {
+    output: string list,
+    redirected_output: string list,
+    return_code: int}
+  val run: (Path.T -> Path.T -> string) -> string -> result
 
   (*cache*)
   type cache
   val make: Path.T -> cache
   val cache_path_of: cache -> Path.T
-  val lookup: cache -> string -> (string list * string list) option * string
+  val lookup: cache -> string -> result option * string
   val run_and_cache: cache -> string -> (Path.T -> Path.T -> string) ->
-    string -> string list * string list
-  val run_cached: cache -> (Path.T -> Path.T -> string) -> string ->
-    string list * string list
+    string -> result
+  val run_cached: cache -> (Path.T -> Path.T -> string) -> string -> result
 end
 
 structure Cache_IO : CACHE_IO =
@@ -45,6 +47,11 @@
     val _ = try File.rm_tree path
   in Exn.release x end
 
+type result = {
+  output: string list,
+  redirected_output: string list,
+  return_code: int}
+
 fun run make_cmd str =
   with_tmp_file cache_io_prefix (fn in_path =>
   with_tmp_file cache_io_prefix (fn out_path =>
@@ -98,7 +105,9 @@
       else if i < p + len1 then (i+1, apfst (cons line) xsp)
       else if i < p + len2 then (i+1, apsnd (cons line) xsp)
       else (i, xsp)
-  in pairself rev (snd (File.fold_lines load cache_path (1, ([], [])))) end
+    val (out, err) =
+      pairself rev (snd (File.fold_lines load cache_path (1, ([], []))))
+  in {output=err, redirected_output=out, return_code=0} end
 
 fun lookup (Cache {path=cache_path, table}) str =
   let val key = SHA1.digest str
@@ -110,9 +119,8 @@
 
 fun run_and_cache (Cache {path=cache_path, table}) key make_cmd str =
   let
-    val {output=err, redirected_output=out, ...} = run make_cmd str
-    val res = (out, err)
-    val (l1, l2) = pairself length res
+    val {output=err, redirected_output=out, return_code} = run make_cmd str
+    val (l1, l2) = pairself length (out, err)
     val header = key ^ " " ^ string_of_int l1 ^ " " ^ string_of_int l2
     val lines = map (suffix "\n") (header :: out @ err)
 
@@ -121,7 +129,7 @@
       else
         let val _ = File.append_list cache_path lines
         in (p+l1+l2+1, Symtab.update (key, (p+1, l1, l2)) tab) end)
-  in res end
+  in {output=err, redirected_output=out, return_code=return_code} end
 
 fun run_cached cache make_cmd str =
   (case lookup cache str of