aboutsummaryrefslogtreecommitdiffstats
path: root/src/smtlib2
diff options
context:
space:
mode:
authorChantal Keller <Chantal.Keller@inria.fr>2020-06-30 13:03:56 +0200
committerChantal Keller <Chantal.Keller@inria.fr>2020-06-30 13:03:56 +0200
commit26c639d438169530275ff7e48a55355deb7047df (patch)
tree79f5f51cd54880d87be699f07280a764ce8eca12 /src/smtlib2
parent29dcd6133fd1f6f90d099e605759140fa1b52a1c (diff)
downloadsmtcoq-26c639d438169530275ff7e48a55355deb7047df.tar.gz
smtcoq-26c639d438169530275ff7e48a55355deb7047df.zip
Cannot print stderr when calling CVC4
Diffstat (limited to 'src/smtlib2')
-rw-r--r--src/smtlib2/smtlib2_solver.ml24
1 files changed, 13 insertions, 11 deletions
diff --git a/src/smtlib2/smtlib2_solver.ml b/src/smtlib2/smtlib2_solver.ml
index 8ae7202..aee9a81 100644
--- a/src/smtlib2/smtlib2_solver.ml
+++ b/src/smtlib2/smtlib2_solver.ml
@@ -95,7 +95,7 @@ let read_check_result s =
let send_command s cmd read =
eprintf "%s@." cmd;
- let err_p1 = Unix.((fstat s.stderr).st_size) in
+ (* let err_p1 = Unix.((fstat s.stderr).st_size) in *)
try
let in_ch = Unix.out_channel_of_descr s.stdin in
let fmt = formatter_of_out_channel in_ch in
@@ -103,16 +103,18 @@ let send_command s cmd read =
pp_print_newline fmt ();
read s
with e ->
- let err_p2 = Unix.((fstat s.stderr).st_size) in
- let len = err_p2 - err_p1 in
- (* Was something written to stderr? *)
- if len <> 0 then begin
- let buf = Bytes.create err_p2 in
- Unix.read s.stderr buf 0 err_p2 |> ignore;
- let err_msg = Bytes.sub_string buf err_p1 len in
- Structures.error ("Solver error: "^err_msg);
- end
- else (kill s; raise e)
+ (* After the exception, the file descriptor is invalid *)
+ (* let err_p2 = Unix.((fstat s.stderr).st_size) in
+ * let len = err_p2 - err_p1 in
+ * (\* Was something written to stderr? *\)
+ * if len <> 0 then begin
+ * let buf = Bytes.create err_p2 in
+ * Unix.read s.stderr buf 0 err_p2 |> ignore;
+ * let err_msg = Bytes.sub_string buf err_p1 len in
+ * Structures.error ("Solver error: "^err_msg);
+ * end
+ * else (kill s; raise e) *)
+ kill s; raise e
let set_option s name b =