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
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 picksas 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