refactor: modifications asked by @gbury in review

src/backend/Dot.ml

@@ -79,7 +79,7 @@ module Make(S : Msat.S)(A : Arg with type atom := S.atom
 
   let print_edges fmt n =
     match P.(n.step) with
-    | P.Hyper_res {P.hr_steps=[];_} -> () (* NOTE: should never happen *)
+    | P.Hyper_res {P.hr_steps=[];_} -> assert false (* NOTE: should never happen *)
     | P.Hyper_res {P.hr_init; hr_steps=((_,p0)::_) as l} ->
       print_edge fmt (res_np_id n p0) (proof_id hr_init);
       List.iter

src/core/Internal.ml

@@ -610,10 +610,6 @@ module Make(Plugin : PLUGIN)
         let duplicates, res = find_dups c in
         assert (same_lits (Sequence.of_list res) (Clause.atoms_seq conclusion));
         { conclusion; step = Duplicate (c, duplicates) }
-      | History (c :: ([_] as r)) ->
-        let res, steps = find_pivots c r in
-        assert (same_lits (Sequence.of_list res) (Clause.atoms_seq conclusion));
-        { conclusion; step = Hyper_res { hr_init=c; hr_steps=steps; }; }
       | History (c :: r) ->
         let res, steps = find_pivots c r in
         assert (same_lits (Sequence.of_list res) (Clause.atoms_seq conclusion));
@@ -714,7 +710,7 @@ module Make(Plugin : PLUGIN)
 
     let check_empty_conclusion (p:t) =
       if Array.length p.atoms > 0 then (
-        error_res_f "@[<2>Proof.check: non empty conclusion for claus@ %a@]" Clause.debug p;
+        error_res_f "@[<2>Proof.check: non empty conclusion for clause@ %a@]" Clause.debug p;
       )
 
     let check (p:t) = fold (fun () _ -> ()) () p

src/core/Solver_intf.ml

@@ -79,6 +79,16 @@ type ('term, 'formula, 'proof) reason =
   | Consequence of (unit -> 'formula list * 'proof)
   (** [Consequence (l, p)] means that the formulas in [l] imply the propagated
       formula [f]. The proof should be a proof of the clause "[l] implies [f]".
+
+      invariant: in [Consequence (l,p)], all elements of [l] must be true in
+      the current trail.
+
+      note on lazyiness: the justification is suspended (using [unit -> …])
+      to avoid potentially costly computations that might never be used
+      if this literal is backtracked without participating in a conflict.
+      However, if the theory isn't robust wrt backtracking an subsequent changes,
+      it can be easier to produce the explanation eagerly when
+      propagating, and then use [Consequence (fun () -> expl, proof)].
   *)
 (** The type of reasons for propagations of a formula [f]. *)