diff options
Diffstat (limited to 'src/theory/shared_terms_database.cpp')
| -rw-r--r-- | src/theory/shared_terms_database.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp index 90037b90b..0c893482a 100644 --- a/src/theory/shared_terms_database.cpp +++ b/src/theory/shared_terms_database.cpp @@ -297,7 +297,7 @@ bool SharedTermsDatabase::areEqual(TNode a, TNode b) { bool SharedTermsDatabase::areDisequal(TNode a, TNode b) { - return d_equalityEngine.areDisequal(a,b); + return d_equalityEngine.areDisequal(a,b,false); } void SharedTermsDatabase::processSharedLiteral(TNode literal, TNode reason) @@ -305,7 +305,7 @@ void SharedTermsDatabase::processSharedLiteral(TNode literal, TNode reason) bool negated = literal.getKind() == kind::NOT; TNode atom = negated ? literal[0] : literal; if (negated) { - Assert(!d_equalityEngine.areDisequal(atom[0], atom[1])); + Assert(!d_equalityEngine.areDisequal(atom[0], atom[1],false)); d_equalityEngine.assertEquality(atom, false, reason); // !!! need to send this out } |