From 10d394a9c3b168b5885b9cd3775ad07b6c181113 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Mon, 28 May 2018 01:22:58 -0500
Subject: [PATCH] fix(cc): public `add` function must also saturate CC

---
 src/sat/Internal.ml           |  5 +++--
 src/smt/Congruence_closure.ml | 15 +++++++++++----
 2 files changed, 14 insertions(+), 6 deletions(-)

diff --git a/src/sat/Internal.ml b/src/sat/Internal.ml
index 332831d9..24b1c297 100644
--- a/src/sat/Internal.ml
+++ b/src/sat/Internal.ml
@@ -979,7 +979,8 @@ module Make (Th : Theory_intf.S) = struct
     );
     let level = decision_level st in
     Log.debugf 5
-      (fun k->k "(@[sat.enqueue_bool@ :lvl %d@ %a@])" level Atom.debug a);
+      (fun k->k "(@[sat.enqueue_bool@ :lvl %d@ %a@ :reason %a@])"
+          level Atom.debug a Atom.debug_reason (level,Some reason));
     (* backtrack assignment if needed. Trail is backtracked automatically. *)
     assert (not a.is_true && a.var.v_level < 0 && a.var.reason = None);
     a.is_true <- true;
@@ -1428,7 +1429,7 @@ module Make (Th : Theory_intf.S) = struct
       while st.elt_head < Vec.size st.trail do
         let a = Vec.get st.trail st.elt_head in
         incr num_props;
-        Log.debugf 5 (fun k->k "(@[sat.bcp.propagate_atom@ %a@])" Atom.pp a);
+        Log.debugf 5 (fun k->k "(@[sat.bcp.propagate_atom_on_trail@ %a@])" Atom.pp a);
         propagate_atom st a;
         st.elt_head <- st.elt_head + 1;
       done;
diff --git a/src/smt/Congruence_closure.ml b/src/smt/Congruence_closure.ml
index d4acd0ff..89251165 100644
--- a/src/smt/Congruence_closure.ml
+++ b/src/smt/Congruence_closure.ml
@@ -338,7 +338,7 @@ let rec update_pending (cc:t): unit =
               assert (Cst.equal f1 f2);
               assert (IArray.length a1 = IArray.length a2);
               Explanation.mk_merges @@
-              IArray.map2 (fun u1 u2 -> add cc u1, add cc u2) a1 a2
+              IArray.map2 (fun u1 u2 -> add_ cc u1, add_ cc u2) a1 a2
             | If _, _ | App_cst _, _ | Bool _, _
               -> assert false
           in
@@ -445,7 +445,7 @@ and add_new_term cc (t:term) : node =
   in
   (* add sub-term to [cc], and register [n] to its parents *)
   let add_sub_t (u:term) : unit =
-    let n_u = add cc u in
+    let n_u = add_ cc u in
     add_to_parents_of_sub_node n_u
   in
   (* register sub-terms, add [t] to their parent list *)
@@ -470,11 +470,18 @@ and add_new_term cc (t:term) : node =
   n
 
 (* add a term *)
-and[@inline] add cc t : node =
+and[@inline] add_ cc t : node =
   try Term.Tbl.find cc.tbl t
   with Not_found -> add_new_term cc t
 
-let[@inline] add_seq cc seq = seq (fun t -> ignore @@ add cc t)
+let add cc t : node =
+  let n = add_ cc t in
+  update_pending cc;
+  n
+
+let add_seq cc seq =
+  seq (fun t -> ignore @@ add_ cc t);
+  update_pending cc
 
 (* before we push tasks into [pending], ensure they are removed when we backtrack *)
 let reset_on_backtrack cc : unit =