diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2020-05-15 10:44:13 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2020-05-15 10:44:13 -0500 |
| commit | d9a85838aa3814d068d28578c9ad120ba6279592 (patch) | |
| tree | 02ff2d4ed978e2bd31a2094eaf71e3ebdb2bf897 | |
| parent | faa7b83c6665eb7e7110eaf807453315b34c4768 (diff) | |
Fix
| -rw-r--r-- | src/theory/uf/equality_engine.cpp | 4 |
1 files 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 |