diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-11 15:15:53 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-11 15:15:53 -0500 |
| commit | 2b7a0168bddfd2b840171aa8b9681f16d606c0b8 (patch) | |
| tree | 0ff97f5c812231101990599649062e6e59ede926 /test/regress/regress0/wiki.04.cvc | |
| parent | bff3b0cbcc38cae5548bc4b36af5bb1c0f66c149 (diff) | |
(proof-new) Handle mismatched assumptions in proof equality engine during mkScope (#5012)
This modifies the fix for Boolean equalities with constants so that is addressed lazily during ProofNodeManager mkScope instead of when asserting assumptions to the proof equality engine. This ensures that the default method for asserting facts to the equality engine for external assertions does not have any special cases.
A previously abandoned solution to this issue had made this a part of CDProof. Instead, this PR modifies the mkScope method only. The fix makes mkScope robust to any assumption mismatches in mkScope that can be fixed by rewriting, not just Boolean equality with constants. It is intended to be used infrequently as a last resort when mkScope has mismatched assumptions. The handling of mismatches due to symmetry remains in this method.
Diffstat (limited to 'test/regress/regress0/wiki.04.cvc')
0 files changed, 0 insertions, 0 deletions