Fixes for witness terms appearing in CEGQI instantiations (#8350)

Fixes for witness terms appearing in CEGQI instantiations (#8350)

Fixes #8344.

We now have cases where witness terms e.g. `(witness x : String. len(x) = N)` appear in model values.  These terms require special care in CEGQI.

There are 2 fixes in this PR:
(1) we update our policy on what a legal term is,
(2) we erase annotations from witness terms appearing in instantiations, which is required for ensuring that proofs are consistent.  Otherwise, the skolemization lemma for a witness term does not introduce the same skolem.