Do not mark string extended functions as eliminated after reduction lemmas (#4306)

The current policy marked extended functions in strings as "reduced" (eliminated) when we generated their reduction lemma. The upside is that the solver can effectively ignore them. The downside is that we cannot do context-dependent simplification on them, and hence we miss out conflicts during the remainder of the check-sat call.

This changes the policy so they are not marked as reduced. Instead, reduction lemmas are cached in the standard way while allowing context-dependent simplification.

0 files changed, 0 insertions, 0 deletions