From 6cbf7c5dd95e6e9ba1bbe8d8a606938f5565426e Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Thu, 14 Mar 2019 13:15:38 +0000
Subject: Report when the SMT solver fails badly

---
 src/constraint.ml | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

(limited to 'src')

diff --git a/src/constraint.ml b/src/constraint.ml
index 5402f6f7..79702340 100644
--- a/src/constraint.ml
+++ b/src/constraint.ml
@@ -290,18 +290,25 @@ let call_smt' l vars constraints : smt_result =
       in
       output_string tmp_chan smt_file;
       close_out tmp_chan;
-      let smt_output =
+      let status, smt_output =
         try
           let smt_out, smt_in, smt_err = Unix.open_process_full (!opt_solver.command ^ " " ^ input_file) (Unix.environment ()) in
           let smt_output =
             try List.combine problems (input_lines smt_out (List.length problems)) with
             | End_of_file -> List.combine problems ["unknown"]
           in
-          let _ = Unix.close_process_full (smt_out, smt_in, smt_err) in
-          smt_output
+          let status = Unix.close_process_full (smt_out, smt_in, smt_err) in
+          status, smt_output
         with
         | exn -> raise (Reporting.err_general l ("Error when calling smt: " ^ Printexc.to_string exn))
       in
+      let _ = match status with
+        | Unix.WEXITED 0 -> ()
+        | Unix.WEXITED n ->
+           raise (Reporting.err_general l ("SMT solver returned unexpected status " ^ string_of_int n))
+        | Unix.WSIGNALED n | Unix.WSTOPPED n ->
+           raise (Reporting.err_general l ("SMT solver killed by signal " ^ string_of_int n))
+      in
       Sys.remove input_file;
       try
         let (problem, _) = List.find (fun (_, result) -> result = "unsat") smt_output in
-- 
cgit v1.2.3