Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.10

2 files changed, 14 insertions, 12 deletions

diff --git a/src/smtlib2/smtlib2_genConstr.ml b/src/smtlib2/smtlib2_genConstr.ml
index f938671..7e58aa3 100644
--- a/src/smtlib2/smtlib2_genConstr.ml
+++ b/src/smtlib2/smtlib2_genConstr.ml
@@ -111,7 +111,7 @@ let declare_sort rt sym = declare_sort_from_name rt (string_of_symbol sym)
 
 let declare_fun_from_name rt ro s tyl ty =
   let coqTy = List.fold_right (fun typ c ->
-      Term.mkArrow (interp_to_coq rt typ) c)
+      Structures.mkArrow (interp_to_coq rt typ) c)
       tyl (interp_to_coq rt ty) in
   let cons_v = Structures.declare_new_variable (Structures.mkId ("Smt_var_"^s)) coqTy in
   let op = Op.declare ro cons_v (Array.of_list tyl) ty None in
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 =