diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-10-20 16:03:00 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-20 16:03:00 -0500 |
| commit | f74a8224d363aa8ae4bdc1324ee56306910b5532 (patch) | |
| tree | c91e6784ebaa98cb6ab6b41d60802dddfc3fd21c /src/expr | |
| parent | 656004c54655ab15289d9e7666bda2e1c7bada1c (diff) | |
(proof-new) Fix for CDProof::isSame (#5297)
Did not check for disequalities properly.
Diffstat (limited to 'src/expr')
| -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; |