Confluence check: improve performance by creating zero/old relations only for relevant variables

Currently, we create 'x0 = x' zero/old relations for all variables. It should be enough to add them only for the variables in the supports of the BDD edges being considered (the event pair). That way, we create less such relations. Since it blows up exponentially the more variables we have, this should greatly improve the performance of the check.

Addresses #892