Improve auxiliary variable elimination in Normalizer

[blishko]

Currently, some auxiliary variables are not eliminated, because the code for detecting substitutions does not distinguish between the variables we want to keep and variables we want to eliminate.
Thus, from an equality s = aux + 1 (where s is a state variable) it may pick s as the variable to eliminate.

It would be better if the code preferred TBE (to be eliminated) variables over the other ones.

Example to test: 2021/LIA-Lin/chc-LIA-Lin_569.smt2