Fix issues related to eliminating extended arithmetic operators (#5475)

Fix issues related to eliminating extended arithmetic operators (#5475)

This fixes 2 issues related to eliminating arithmetic operators:
(1) counterexample lemmas in CEGQI were not being preprocessed
(2) ensureLiteral was not doing term formula removal.
This corrects these two issues. Now ensureLiteral does full theory preprocessing on the term we are ensuring literal for, meaning this may trigger lemmas if the term contains extended arithmetic operators like div.

Fixes #5469, fixes #5470, fixes #5471.

This adds --sygus-inst to 2 of these benchmarks which moreover makes them solvable.

This also improves our assertions and trace messages.