In the current encoding to single transition system, when translating edge constraint, we do not put any restriction on the big system's state variables that do no correspond to the variables of the target node. This means that when we encounter alien variables during backtranslation of validity witness, we can universally quantify these variables to obtain predicate representation only over its arguments. We can then apply quantifier elimination.
Since QE works on existential quantifiers, we have to first negate the original invariant and then negate again after QE.
In the current encoding to single transition system, when translating edge constraint, we do not put any restriction on the big system's state variables that do no correspond to the variables of the target node. This means that when we encounter alien variables during backtranslation of validity witness, we can universally quantify these variables to obtain predicate representation only over its arguments. We can then apply quantifier elimination. Since QE works on existential quantifiers, we have to first negate the original invariant and then negate again after QE.
Fixes #45.