Confluence check: improve performance by interleaving the zero variables

Currently, the extra zero variables are added at the end, so the nodes for these variables are on the top. It is likely more efficient to interleave them with the existing current/old and new variables.

Now that we've changed the CIF controller properties checker to do a separate conversion to BDD/MDD per check, we could likely do this now. It would require functionality in CIF to BDD to request adding a number of extra variables to be added during the conversion. We need only one such set of extra variables for the confluence check.

Addresses #892