summaryrefslogtreecommitdiff
path: root/src/theory/shared_terms_database.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/shared_terms_database.cpp')
-rw-r--r--src/theory/shared_terms_database.cpp2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp
index 235d6959c..90037b90b 100644
--- a/src/theory/shared_terms_database.cpp
+++ b/src/theory/shared_terms_database.cpp
@@ -58,7 +58,7 @@ void SharedTermsDatabase::addSharedTerm(TNode atom, TNode term, Theory::Set theo
d_addedSharedTermsSize = d_addedSharedTermsSize + 1;
d_termsToTheories[search_pair] = theories;
if (!d_equalityEngine.hasTerm(term)) {
- d_equalityEngine.addTriggerTerm(term);
+ d_equalityEngine.addTriggerTerm(term, THEORY_UF);
}
} else {
Assert(theories != (*find).second);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback