(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 4aac1cac73fc6cc9ffc06eb389e70c1314241d6c..94ca26dd6eabed2ac11b39b741a368e459230036 100644 (file)
--- 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;