From c7511b2934aad37c9548e78e3c4fb85ce0007e1d Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Mon, 27 Sep 2021 12:18:37 -0400
Subject: [PATCH] fix compilation error

---
 src/sat/Solver.ml   | 12 ++++++------
 src/util/Vec_sig.ml |  7 +++++++
 2 files changed, 13 insertions(+), 6 deletions(-)

diff --git a/src/sat/Solver.ml b/src/sat/Solver.ml
index a686ceff..4f962f71 100644
--- a/src/sat/Solver.ml
+++ b/src/sat/Solver.ml
@@ -1169,18 +1169,18 @@ module Make(Plugin : PLUGIN)
    (* minimize conflict by removing atoms whose propagation history
       is ultimately self-subsuming with [lits] *)
    let minimize_conflict (self:t) (_c_level:int)
-       (learnt: atom Vec.t) : unit =
+       (learnt: AVec.t) : unit =
      let store = self.store in
 
      (* abstraction of the levels involved in the conflict at all,
         as logical "or" of each literal's approximate level *)
      let abstract_levels =
-       Vec.fold (fun lvl a -> lvl lor abstract_level_ self (Atom.var a)) 0 learnt
+       AVec.fold_left (fun lvl a -> lvl lor abstract_level_ self (Atom.var a)) 0 learnt
      in
 
      let j = ref 1 in
-     for i=1 to Vec.size learnt - 1 do
-       let a = Vec.get learnt i in
+     for i=1 to AVec.size learnt - 1 do
+       let a = AVec.get learnt i in
        let keep =
          begin match Atom.reason store a with
            | Some Decision -> true (* always keep decisions *)
@@ -1190,13 +1190,13 @@ module Make(Plugin : PLUGIN)
          end
        in
        if keep then (
-         Vec.set learnt !j a;
+         AVec.set learnt !j a;
          incr j
        ) else (
          Stat.incr self.n_minimized_away;
        )
      done;
-     Vec.shrink learnt !j;
+     AVec.shrink learnt !j;
      ()
 
   (* result of conflict analysis, containing the learnt clause and some
diff --git a/src/util/Vec_sig.ml b/src/util/Vec_sig.ml
index e1e21f63..8f3a0025 100644
--- a/src/util/Vec_sig.ml
+++ b/src/util/Vec_sig.ml
@@ -44,6 +44,8 @@ module type EXTENSIONS = sig
 
   val to_array : t -> elt array
 
+  val fold_left : ('a -> elt -> 'a) -> 'a -> t -> 'a
+
   val pp : elt CCFormat.printer -> t CCFormat.printer
 end
 
@@ -69,6 +71,11 @@ module Make_extensions(B: BASE_RO)
       a
     )
 
+  let fold_left f acc self =
+    let r = ref acc in
+    iter self ~f:(fun x -> r := f !r x);
+    !r
+
   let pp ppx out self =
     Format.fprintf out "[@[";
     iteri self