diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-10-22 16:01:37 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-10-22 21:01:37 +0000 |
| commit | bdc1671342704ffa8113cbb6f3b5f07af25d564b (patch) | |
| tree | 2a54840225625ddb69c90dc8204f3a06f341d525 | |
| parent | 4929b5dcfaba1e051309a0debfeaf9f8bf8e2d8b (diff) | |
Fix symmetry issue in theory engine conflicts (#7469)
Fixes --check-proofs on proof-new on regress0/strings/issue5384-double-conflict.smt2.
| -rw-r--r-- | src/theory/theory_engine.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 1e7116ac4..0f3260920 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1476,7 +1476,7 @@ void TheoryEngine::conflict(TrustNode tconflict, TheoryId theoryId) } else { - if (fullConflict != conflict) + if (!CDProof::isSame(fullConflict, conflict)) { // ------------------------- explained ---------- from theory // fullConflict => conflict ~conflict |