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

debug: add type checking in CC.merge

Browse source
This commit is contained in:
Simon Cruanes 2019-12-28 08:19:59 -06:00
parent 91e9b6cc2c
commit 62b1d83cd6
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/cc/Sidekick_cc.ml
View file

@ -813,6 +813,7 @@ module Make (A: CC_ARG)
let merge cc n1 n2 expl = let merge cc n1 n2 expl =
Log.debugf 5 Log.debugf 5
(fun k->k "(@[cc.theory.merge@ :n1 %a@ :n2 %a@ :expl %a@])" N.pp n1 N.pp n2 Expl.pp expl); (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 merge_classes cc n1 n2 expl
let[@inline] merge_t cc t1 t2 expl = let[@inline] merge_t cc t1 t2 expl =