From bdc1671342704ffa8113cbb6f3b5f07af25d564b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 22 Oct 2021 16:01:37 -0500 Subject: [PATCH] Fix symmetry issue in theory engine conflicts (#7469) Fixes --check-proofs on proof-new on regress0/strings/issue5384-double-conflict.smt2. --- src/theory/theory_engine.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 -- 2.30.2