From f74a8224d363aa8ae4bdc1324ee56306910b5532 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 20 Oct 2020 16:03:00 -0500
Subject: [PATCH] (proof-new) Fix for CDProof::isSame (#5297)

Did not check for disequalities properly.
---
 src/expr/proof.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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;
-- 
2.30.2