Fix for incomplete proofs due to hypothesis not proved

sat/sat.ml

@@ -141,6 +141,7 @@ module Make(Log : Log_intf.S) = struct
   let eval = SatSolver.eval
 
   let get_proof () =
+    SatSolver.Proof.learn (SatSolver.hyps ());
     SatSolver.Proof.learn (SatSolver.history ());
     match SatSolver.unsat_conflict () with
     | None -> assert false

smt/mcsat.ml

@@ -135,6 +135,7 @@ module Make(Dummy:sig end) = struct
     with SmtSolver.Unsat -> ()
 
   let get_proof () =
+    SmtSolver.Proof.learn (SmtSolver.hyps ());
     SmtSolver.Proof.learn (SmtSolver.history ());
     match SmtSolver.unsat_conflict () with
     | None -> assert false

smt/smt.ml

@@ -84,6 +84,7 @@ module Make(Dummy:sig end) = struct
     with SmtSolver.Unsat -> ()
 
   let get_proof () =
+    SmtSolver.Proof.learn (SmtSolver.hyps ());
     SmtSolver.Proof.learn (SmtSolver.history ());
     match SmtSolver.unsat_conflict () with
     | None -> assert false

solver/mcsolver.ml

@@ -875,6 +875,8 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
     let truth = var.tag.pa.is_true in
     if negated then not truth else truth
 
+  let hyps () = env.clauses
+
   let history () = env.learnts
 
   let unsat_conflict () = env.unsat_conflict

solver/mcsolver.mli

@@ -33,6 +33,10 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
   (** Returns the valuation of a formula in the current state
       of the sat solver. *)
 
+  val hyps : unit -> St.clause Vec.t
+  (** Returns the vector of assumptions used by the solver. May be slightly different
+      from the clauses assumed because of top-level simplification of clauses. *)
+
   val history : unit -> St.clause Vec.t
   (** Returns the history of learnt clauses, in the right order. *)
 

solver/solver.ml

@@ -737,6 +737,8 @@ module Make (L : Log_intf.S)(F : Formula_intf.S)
     let truth = var.pa.is_true in
     if negated then not truth else truth
 
+  let hyps () = env.clauses
+
   let history () = env.learnts
 
   let unsat_conflict () = env.unsat_conflict

solver/solver.mli

@@ -40,6 +40,10 @@ module Make (L : Log_intf.S)(F : Formula_intf.S)
   (** Returns the valuation of a formula in the current state
       of the sat solver. *)
 
+  val hyps : unit -> St.clause Vec.t
+  (** Returns the vector of assumptions used by the solver. May be slightly different
+      from the clauses assumed because of top-level simplification of clauses. *)
+
   val history : unit -> St.clause Vec.t
   (** Returns the history of learnt clauses, in the right order. *)