summaryrefslogtreecommitdiff
path: root/src/theory/bv/theory_bv.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/bv/theory_bv.cpp')
-rw-r--r--src/theory/bv/theory_bv.cpp5
1 files changed, 0 insertions, 5 deletions
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 857d4d6fb..79a20c9c9 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -209,11 +209,6 @@ TrustNode TheoryBV::explain(TNode node) { return d_internal->explain(node); }
void TheoryBV::notifySharedTerm(TNode t)
{
d_internal->notifySharedTerm(t);
- // temporary, will be built into Theory::addSharedTerm
- if (d_equalityEngine != nullptr)
- {
- d_equalityEngine->addTriggerTerm(t, THEORY_BV);
- }
}
void TheoryBV::ppStaticLearn(TNode in, NodeBuilder<>& learned)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback