simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 11:15:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

fix(cc): remove too powerful assertion in CC

Browse source
This commit is contained in:
Simon Cruanes 2019-12-09 21:49:29 -06:00
parent c54ee2310e
commit bf23f7c826
1 changed files with 1 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/cc/Sidekick_cc.ml
View file

@ -171,9 +171,7 @@ module Make (A: CC_ARG)
let mk_reduction : t = E_reduction let mk_reduction : t = E_reduction
let[@inline] mk_congruence n1 n2 : t = E_congruence (n1,n2) let[@inline] mk_congruence n1 n2 : t = E_congruence (n1,n2)
let[@inline] mk_merge a b : t = let[@inline] mk_merge a b : t = if N.equal a b then mk_reduction else E_merge (a,b)
assert (same_class a b);
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_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 let[@inline] mk_lit l : t = E_lit l