Andrew Reynolds 05a9433b25 Fix issue with substitution context in strings extended function inference (#12292) ...

Fixes https://github.com/cvc5/cvc5-projects/issues/776.

This updates the explanation mechanism for context dependent
simplification, to ensure substitutions whose LHS are concatention terms
are avoided.

Would otherwise lead to cyclic proofs, which cause the conversion proof
generator to fail.

The regression added required 2 RARE rewrites which were missing.

2025-12-09 20:15:32 +00:00

..

eo/cpc

Fix issue with substitution context in strings extended function inference (#12292)

2025-12-09 20:15:32 +00:00

lfsc/signatures

Fix LFSC regressions with log2 (#12231)

2025-11-12 15:54:46 +00:00