diff --git a/src/mini-cc/Sidekick_mini_cc.ml b/src/mini-cc/Sidekick_mini_cc.ml
index a3e604f9..4e431765 100644
--- a/src/mini-cc/Sidekick_mini_cc.ml
+++ b/src/mini-cc/Sidekick_mini_cc.ml
@@ -15,6 +15,8 @@ module type S = sig
 
   val create : term_state -> t
 
+  val clear : t -> unit
+
   val add_lit : t -> term -> bool -> unit
 
   val check_sat : t -> bool
@@ -144,6 +146,16 @@ module Make(A: ARG) = struct
     T_tbl.add self.tbl false_ self.false_;
     self
 
+  let clear (self:t) : unit =
+    self.ok <- true;
+    T_tbl.clear self.tbl;
+    Sig_tbl.clear self.sig_tbl;
+    self.pending <- [];
+    self.combine <- [];
+    T_tbl.add self.tbl self.true_.n_t self.true_;
+    T_tbl.add self.tbl self.false_.n_t self.false_;
+    ()
+
   let sub_ t k : unit =
     match A.cc_view t with
     | Bool _ | Opaque _ -> ()
diff --git a/src/mini-cc/Sidekick_mini_cc.mli b/src/mini-cc/Sidekick_mini_cc.mli
index f7a66730..10990313 100644
--- a/src/mini-cc/Sidekick_mini_cc.mli
+++ b/src/mini-cc/Sidekick_mini_cc.mli
@@ -22,6 +22,9 @@ module type S = sig
 
   val create : term_state -> t
 
+  val clear : t -> unit
+  (** Fully reset the congruence closure's state *)
+
   val add_lit : t -> term -> bool -> unit
   (** [add_lit cc p sign] asserts that [p=sign] *)
 
diff --git a/src/mini-cc/tests/tests.ml b/src/mini-cc/tests/tests.ml
index 1b6d72fa..751e944b 100644
--- a/src/mini-cc/tests/tests.ml
+++ b/src/mini-cc/tests/tests.ml
@@ -70,6 +70,18 @@ let () = mk_test "test_f_f_f_a" @@ fun () ->
   A.(check bool) "is-unsat" (CC.check_sat cc) false;
   ()
 
+let () = mk_test "test_repeated_f_f_f_a" @@ fun () ->
+  let module S = Setup() in
+  let cc = CC.create S.tst in
+  for _i = 0 to 10 do
+    CC.add_lit cc S.(neq a (f (f (f (f (f (f a))))))) true;
+    A.(check bool) "is-sat" (CC.check_sat cc) true;
+    CC.add_lit cc S.(eq a (f a)) true;
+    A.(check bool) "is-unsat" (CC.check_sat cc) false;
+    CC.clear cc;
+  done;
+  ()
+
 let () = mk_test "test_trans" @@ fun () ->
   let module S = Setup() in
   let cc = CC.create S.tst in
@@ -89,6 +101,18 @@ let () = mk_test "test_true" @@ fun () ->
   A.(check bool) "is-unsat" (CC.check_sat cc) false;
   ()
 
+let () = mk_test "test_repeated_true" @@ fun () ->
+  let module S = Setup() in
+  let cc = CC.create S.tst in
+  for _i = 0 to 10 do
+    CC.add_lit cc S.true_ true;
+    A.(check bool) "is-sat" (CC.check_sat cc) true;
+    CC.add_lit cc S.false_ true;
+    A.(check bool) "is-unsat" (CC.check_sat cc) false;
+    CC.clear cc;
+  done;
+  ()
+
 let () = mk_test "test_false" @@ fun () ->
   let module S = Setup() in
   let cc = CC.create S.tst in