diff options
Diffstat (limited to 'src/expr/proof.cpp')
| -rw-r--r-- | src/expr/proof.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
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; |