projects / cvc5.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 4929b5d)
Fix symmetry issue in theory engine conflicts (#7469)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 22 Oct 2021 21:01:37 +0000 (16:01 -0500)
committerGitHub <noreply@github.com>
Fri, 22 Oct 2021 21:01:37 +0000 (21:01 +0000)
Fixes --check-proofs on proof-new on regress0/strings/issue5384-double-conflict.smt2.

src/theory/theory_engine.cpp patch | blob | history

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 1e7116ac4b6fb1758d3e96533ed7239ae13f2845..0f3260920bc7e07b9c233e577032fda1422f473f 100644 (file)
--- 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