From bf23f7c82661c8ca9d2f59eaac2edfd770f3a833 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 9 Dec 2019 21:49:29 -0600 Subject: [PATCH] fix(cc): remove too powerful assertion in CC --- src/cc/Sidekick_cc.ml | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/src/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml index 87f20ea6..d5946010 100644 --- a/src/cc/Sidekick_cc.ml +++ b/src/cc/Sidekick_cc.ml @@ -171,9 +171,7 @@ module Make (A: CC_ARG) let mk_reduction : t = E_reduction let[@inline] mk_congruence n1 n2 : t = E_congruence (n1,n2) - let[@inline] mk_merge a b : t = - assert (same_class a b); - if N.equal a b then mk_reduction else E_merge (a,b) + let[@inline] mk_merge a b : t = if N.equal a b then mk_reduction else E_merge (a,b) let[@inline] mk_merge_t a b : t = if Term.equal a b then mk_reduction else E_merge_t (a,b) let[@inline] mk_lit l : t = E_lit l