Simplify strings term registration (#6174)

Simplify strings term registration (#6174)

String terms may enter into the equality engine without appearing in assertions, due to eager context-dependent simplification internal to the equality engine (--strings-eager-eval). In rare cases, we did not catch when a new string constant appeared in the equality engine, meaning it would not be marked as relevant leading to bogus models in incremental mode.

This makes it so that proxy variables are stored in a user-context dependent manner, which impacts when terms marked as having a proxy variable are registered.

The PR also simplifies our policies for when string terms are registered slightly.

Fixes #6072.