Currently, debug output is very limited. It only prints a few lines at the end of the check, with the conclusion. There is more debug output, but this needs to be enabled in the code. I propose to change some of that to normal debug output, to show what checks (mutual exclusiveness, update equivalence, etc) is being checked, etc. We should then print normal BDD debug output, like we do with other BDD-based checks, and during data-based synthesis, rather than the internal representation of `BDD.toString`. This may be tricky if the predicate has zero variables, as `BddUtils.bddToStr` can't handle those, currently. Addresses #892