Add constants from equality engine evaluation to model (#5391)

Fixes #5330. The issue mentions to related model checking failures:

When the theory of strings computes a model, there is a step that
chooses a constant that is different from other constants of the same
length in other equivalence classes. In the example, the issue was
that the constant "A" was introduced by doing evaluation in the
equality engine of the theory of strings. The constant was then not
added to the term set and was skipped while asserting the equality
engine to the theory model. As a result, an equivalence class was
assigned "A" even though it already existed, which made the model
invalid. The fix ensures that all constants in the equality engine are
added to the theory model. It should be ok to handle the issue during
model construction because other theories shouldn't have to care about
the constants that we computed internally within the theory of
strings.
When an equivalence class has a normal form that consists of a single
seq.unit, then we need to make sure that the value for the argument
is consistent with the rest of the model and we have to make sure that
we choose different values for different equivalence classes. The
commit adds code for retrieving the value of the argument to
seq.unit from the model and adds the resulting constant to the
theory model to block it for other equivalence classes. Previously,
this was not done and we ended up with two different equivalence
classes being assigned the same constant.

0 files changed, 0 insertions, 0 deletions