From 62b1d83cd665ebbcba04805d0a5e01d44603f3f5 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Sat, 28 Dec 2019 08:19:59 -0600
Subject: [PATCH] debug: add type checking in `CC.merge`

---
 src/cc/Sidekick_cc.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml
index 43cacb61..eb05fb64 100644
--- a/src/cc/Sidekick_cc.ml
+++ b/src/cc/Sidekick_cc.ml
@@ -813,6 +813,7 @@ module Make (A: CC_ARG)
   let merge cc n1 n2 expl =
     Log.debugf 5
       (fun k->k "(@[cc.theory.merge@ :n1 %a@ :n2 %a@ :expl %a@])" N.pp n1 N.pp n2 Expl.pp expl);
+    assert (T.Ty.equal (T.Term.ty n1.n_term) (T.Term.ty n2.n_term));
     merge_classes cc n1 n2 expl
 
   let[@inline] merge_t cc t1 t2 expl =