diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/constraint.ml | 13 |
1 files changed, 10 insertions, 3 deletions
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 |