From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 22 Oct 2021 21:01:37 +0000 (-0500)
Subject: Fix symmetry issue in theory engine conflicts (#7469)
X-Git-Tag: cvc5-1.0.0~1000
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bdc1671342704ffa8113cbb6f3b5f07af25d564b;p=cvc5.git

Fix symmetry issue in theory engine conflicts (#7469)

Fixes --check-proofs on proof-new on regress0/strings/issue5384-double-conflict.smt2.
---

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