From 0168ec9f128246d1a6a0a34f7ee59aec109b7782 Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Fri, 27 Apr 2012 19:26:01 +0000 Subject: Fixed warning in decision_engine.h, minor tweak to caregraph function in arrays, fixed bug with equalities between constants in shared terms database --- src/theory/shared_terms_database.cpp | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'src/theory/shared_terms_database.cpp') diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp index 24cbc165c..577e1b957 100644 --- a/src/theory/shared_terms_database.cpp +++ b/src/theory/shared_terms_database.cpp @@ -204,11 +204,9 @@ void SharedTermsDatabase::mergeSharedTerms(TNode a, TNode b) // Normalize the equality Node equality = left.eqNode(right); Node normalized = Rewriter::rewriteEquality(currentTheory, equality); - if (normalized.getKind() != kind::CONST_BOOLEAN) { + if (normalized.getKind() != kind::CONST_BOOLEAN || !normalized.getConst()) { // Notify client d_sharedNotify.notify(normalized, equality, currentTheory); - } else { - Assert(equality.getConst()); } } @@ -253,6 +251,7 @@ void SharedTermsDatabase::processSharedLiteral(TNode literal, TNode reason) if (negated) { Assert(!d_equalityEngine.areDisequal(atom[0], atom[1])); d_equalityEngine.addDisequality(atom[0], atom[1], reason); + // !!! need to send this out } else { Assert(!d_equalityEngine.areEqual(atom[0], atom[1])); -- cgit v1.2.3