From d9a85838aa3814d068d28578c9ad120ba6279592 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 15 May 2020 10:44:13 -0500 Subject: Fix --- src/theory/uf/equality_engine.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 67213fb9b..504f43d72 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -456,7 +456,7 @@ void EqualityEngine::assertEqualityInternal(TNode t1, TNode t2, TNode reason, un enqueue(MergeCandidate(t1Id, t2Id, pid, reason)); } -void EqualityEngine::assertPredicate(TNode t, bool polarity, TNode reason, unsigned pid) { +bool EqualityEngine::assertPredicate(TNode t, bool polarity, TNode reason, unsigned pid) { Debug("equality") << d_name << "::eq::addPredicate(" << t << "," << (polarity ? "true" : "false") << ")" << std::endl; Assert(t.getKind() != kind::EQUAL) << "Use assertEquality instead"; TNode b = polarity ? d_true : d_false; @@ -469,7 +469,7 @@ void EqualityEngine::assertPredicate(TNode t, bool polarity, TNode reason, unsig return true; } -void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason, unsigned pid) { +bool EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason, unsigned pid) { Debug("equality") << d_name << "::eq::addEquality(" << eq << "," << (polarity ? "true" : "false") << ")" << std::endl; if (polarity) { // If two terms are already equal, don't assert anything -- cgit v1.2.3