From 2047f81d05ba46c82d9c503358c4eec17dff7d27 Mon Sep 17 00:00:00 2001
From: Chantal Keller <Chantal.Keller@inria.fr>
Date: Tue, 30 Jun 2020 09:27:08 +0200
Subject: Update required version of OCaml (fixes #73)

---
 INSTALL.md | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

diff --git a/INSTALL.md b/INSTALL.md
index fac167e..e4646ae 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -15,13 +15,13 @@ you want to use.
 
 ## Requirements
 
-You need to have OCaml version >= 4.04.0 and Coq version 8.9.0.
+You need to have OCaml version >= 4.09.0 and Coq version 8.9.0.
 The easiest way to install these two pieces of software is through opam.
 
 > **Warning**: The version of Coq that you plan to use must have been compiled
 > with the same version of OCaml that you are going to use to compile
 > SMTCoq. In particular this means you want a version of Coq that was compiled
-> with OCaml version >= 4.04.0.
+> with OCaml version >= 4.09.0.
 
 If you want to use SMTCoq with high performance to check large proof
 certificates, you need to use the [version of Coq with native
@@ -67,11 +67,10 @@ eval `opam config env`
 
 #### Install OCaml
 
-Now you can install an OCaml compiler (we recommend 4.04.0 or the latest
-release):
+Now you can install an OCaml compiler (we recommend 4.09.0):
 
 ```bash
-opam switch 4.04.0
+opam switch create ocaml-base-compiler.4.09.0
 ```
 
 #### Install Coq
@@ -110,7 +109,7 @@ make install
 wget https://github.com/coq/coq/archive/V8.9.0.tar.gz
 ```
    and compile it by following the instructions available in the
-   repository (make sure you use OCaml 4.04.0 for that). We recommand
+   repository (make sure you use OCaml 4.09.0 for that). We recommand
    that you do not install it, but only compile it in local:
 ```bash
 ./configure -local
-- 
cgit 


From 29dcd6133fd1f6f90d099e605759140fa1b52a1c Mon Sep 17 00:00:00 2001
From: Chantal Keller <Chantal.Keller@inria.fr>
Date: Tue, 30 Jun 2020 13:02:54 +0200
Subject: Empty bit-vectors are not valid in SMT (fixes #76)

---
 src/trace/smtAtom.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml
index c20a75d..ae44b8d 100644
--- a/src/trace/smtAtom.ml
+++ b/src/trace/smtAtom.ml
@@ -649,7 +649,7 @@ module Atom =
         to_smt_atom (atom h)
 
       and to_smt_atom = function
-        | Acop (CO_BV bv) -> Format.fprintf fmt "#b%a" bv_to_smt bv
+        | Acop (CO_BV bv) -> if List.length bv = 0 then Structures.error "Empty bit-vectors are not valid in SMT" else Format.fprintf fmt "#b%a" bv_to_smt bv
         | Acop _ as a -> to_smt_int fmt (compute_int a)
         | Auop (op,h) -> to_smt_uop op h
         | Abop (op,h1,h2) -> to_smt_bop op h1 h2
-- 
cgit 


From 26c639d438169530275ff7e48a55355deb7047df Mon Sep 17 00:00:00 2001
From: Chantal Keller <Chantal.Keller@inria.fr>
Date: Tue, 30 Jun 2020 13:03:56 +0200
Subject: Cannot print stderr when calling CVC4

---
 src/smtlib2/smtlib2_solver.ml | 24 +++++++++++++-----------
 1 file 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 =
-- 
cgit