Fix 1243

Open Halbaroth opened this issue 10 months ago • 0 comments

The fix consists in using declared_ids to guarantee that we never define symbols that have not been declared at the current assertion level in models. A proper fix requires a lot of work as we need to rework the push/pop mechanism of CDCL.

This PR is rebased https://github.com/OCamlPro/alt-ergo/pull/1280 to ensure we won't mix identifiers from different assertion levels as it could happen with string-based identifiers.

Jan 30 '25 17:01 Halbaroth