From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 20 Oct 2020 21:03:00 +0000 (-0500)
Subject: (proof-new) Fix for CDProof::isSame (#5297)
X-Git-Tag: cvc5-1.0.0~2682
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f74a8224d363aa8ae4bdc1324ee56306910b5532;p=cvc5.git

(proof-new) Fix for CDProof::isSame (#5297)

Did not check for disequalities properly.
---

diff --git a/src/expr/proof.cpp b/src/expr/proof.cpp
index 4aac1cac7..94ca26dd6 100644
--- a/src/expr/proof.cpp
+++ b/src/expr/proof.cpp
@@ -408,7 +408,8 @@ bool CDProof::isSame(TNode f, TNode g)
     // symmetric equality
     return true;
   }
-  if (fk == NOT && gk == NOT && f[0][0] == g[0][1] && f[0][1] == g[0][0])
+  if (fk == NOT && gk == NOT && f[0].getKind() == EQUAL
+      && g[0].getKind() == EQUAL && f[0][0] == g[0][1] && f[0][1] == g[0][0])
   {
     // symmetric disequality
     return true;