summaryrefslogtreecommitdiff
path: root/src/theory/uf/inst_strategy.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/uf/inst_strategy.cpp')
-rw-r--r--src/theory/uf/inst_strategy.cpp2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/uf/inst_strategy.cpp b/src/theory/uf/inst_strategy.cpp
index 9d644ae8d..5ce88177a 100644
--- a/src/theory/uf/inst_strategy.cpp
+++ b/src/theory/uf/inst_strategy.cpp
@@ -236,7 +236,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
d_quantEngine->getPhaseReqTerms( f, patTermsF );
//sort into single/multi triggers
std::map< Node, std::vector< Node > > varContains;
- Trigger::getVarContains( f, patTermsF, varContains );
+ d_quantEngine->getTermDatabase()->getVarContains( f, patTermsF, varContains );
for( std::map< Node, std::vector< Node > >::iterator it = varContains.begin(); it != varContains.end(); ++it ){
if( it->second.size()==f[0].getNumChildren() ){
d_patTerms[0][f].push_back( it->first );
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback