diff options
Diffstat (limited to 'src/theory/arrays/theory_arrays.cpp')
| -rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 34c4fd156..b4a234748 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -883,9 +883,11 @@ Node TheoryArrays::explain(TNode literal, eq::EqProof* proof) { // SHARING ///////////////////////////////////////////////////////////////////////////// - -void TheoryArrays::addSharedTerm(TNode t) { - Debug("arrays::sharing") << spaces(getSatContext()->getLevel()) << "TheoryArrays::addSharedTerm(" << t << ")" << std::endl; +void TheoryArrays::notifySharedTerm(TNode t) +{ + Debug("arrays::sharing") << spaces(getSatContext()->getLevel()) + << "TheoryArrays::notifySharedTerm(" << t << ")" + << std::endl; d_equalityEngine->addTriggerTerm(t, THEORY_ARRAYS); if (t.getType().isArray()) { d_sharedArrays.insert(t); |