Data-based synthesis could use BDD leak detection
It may be good to:
- Check at the end of synthesis whether no BDD node references are in use. Everything should have been freed.
- For certain loops, such as reachability loops, the number of references should remain the same after each iteration.
This will help detect BDD leaks that we currently have, and prevent (most) new ones from being introduced.