diff --git a/src/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml
index ce6275fa..8a58c75e 100644
--- a/src/cc/Sidekick_cc.ml
+++ b/src/cc/Sidekick_cc.ml
@@ -443,25 +443,25 @@ module Make (A: CC_ARG)
         | Some (App_fun (f1, a1)), Some (App_fun (f2, a2)) ->
           assert (Fun.equal f1 f2);
           assert (List.length a1 = List.length a2);
-          List.fold_left2 (explain_equal cc ~th) acc a1 a2
+          List.fold_left2 (explain_equal_rec_ cc ~th) acc a1 a2
         | Some (App_ho (f1, a1)), Some (App_ho (f2, a2)) ->
-          let acc = explain_equal cc ~th acc f1 f2 in
-          explain_equal cc ~th acc a1 a2
+          let acc = explain_equal_rec_ cc ~th acc f1 f2 in
+          explain_equal_rec_ cc ~th acc a1 a2
         | Some (If (a1,b1,c1)), Some (If (a2,b2,c2)) ->
-          let acc = explain_equal cc ~th acc a1 a2 in
-          let acc = explain_equal cc ~th acc b1 b2 in
-          explain_equal cc ~th acc c1 c2
+          let acc = explain_equal_rec_ cc ~th acc a1 a2 in
+          let acc = explain_equal_rec_ cc ~th acc b1 b2 in
+          explain_equal_rec_ cc ~th acc c1 c2
         | _ ->
           assert false
       end
     | E_lit lit -> lit :: acc
     | E_theory e' ->
       th := true; explain_decompose_expl cc ~th acc e'
-    | E_merge (a,b) -> explain_equal cc ~th acc a b
+    | E_merge (a,b) -> explain_equal_rec_ cc ~th acc a b
     | E_merge_t (a,b) ->
       (* find nodes for [a] and [b] on the fly *)
       begin match T_tbl.find cc.tbl a, T_tbl.find cc.tbl b with
-        | a, b -> explain_equal cc ~th acc a b
+        | a, b -> explain_equal_rec_ cc ~th acc a b
         | exception Not_found ->
           Error.errorf "expl: cannot find node(s) for %a, %a" Term.pp a Term.pp b
       end
@@ -469,7 +469,7 @@ module Make (A: CC_ARG)
       let acc = explain_decompose_expl cc ~th acc a in
       explain_decompose_expl cc ~th acc b
 
-  and explain_equal (cc:t) ~th (acc:lit list) (a:node) (b:node) : _ list =
+  and explain_equal_rec_ (cc:t) ~th (acc:lit list) (a:node) (b:node) : _ list =
     Log.debugf 5
       (fun k->k "(@[cc.explain_loop.at@ %a@ =?= %a@])" N.pp a N.pp b);
     assert (N.equal (find_ a) (find_ b));
@@ -654,8 +654,8 @@ module Make (A: CC_ARG)
            C3: r1 C1 C2
         *)
         let lits = explain_decompose_expl cc ~th [] e_ab in
-        let lits = explain_equal cc ~th lits a ra in
-        let lits = explain_equal cc ~th lits b rb in
+        let lits = explain_equal_rec_ cc ~th lits a ra in
+        let lits = explain_equal_rec_ cc ~th lits b rb in
         let emit_proof p =
           let p_lits = Iter.of_list lits |> Iter.map Lit.neg in
           P.lemma_cc p_lits p in
@@ -754,7 +754,7 @@ module Make (A: CC_ARG)
     let half_expl = lazy (
       let th = ref false in
       let lits = explain_decompose_expl cc ~th [] e_12 in
-      th, explain_equal cc ~th lits r2 t2
+      th, explain_equal_rec_ cc ~th lits r2 t2
     ) in
     (* TODO: flag per class, `or`-ed on merge, to indicate if the class
        contains at least one lit *)
@@ -773,7 +773,7 @@ module Make (A: CC_ARG)
            let reason =
              let e = lazy (
                let lazy (th, acc) = half_expl in
-               let lits = explain_equal cc ~th acc u1 t1 in
+               let lits = explain_equal_rec_ cc ~th acc u1 t1 in
                let emit_proof p =
                  (* make a tautology, not a true guard *)
                  let p_lits = Iter.cons lit (Iter.of_list lits |> Iter.map Lit.neg) in
@@ -863,7 +863,7 @@ module Make (A: CC_ARG)
 
   let explain_eq cc n1 n2 : lit list =
     let th = ref true in
-    explain_equal cc ~th [] n1 n2
+    explain_equal_rec_ cc ~th [] n1 n2
 
   let on_pre_merge cc f = cc.on_pre_merge <- f :: cc.on_pre_merge
   let on_post_merge cc f = cc.on_post_merge <- f :: cc.on_post_merge