diff options
Diffstat (limited to 'src/theory/quantifiers/trigger.cpp')
-rw-r--r-- | src/theory/quantifiers/trigger.cpp | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index c4bc248d3..cff28f243 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -38,7 +38,8 @@ d_quantEngine( qe ), d_f( f ){ for( int i=0; i<(int)d_nodes.size(); i++ ){ Trace("trigger") << " " << d_nodes[i] << std::endl; } - Trace("trigger") << ", smart triggers = " << smartTriggers << std::endl; + Trace("trigger-debug") << ", smart triggers = " << smartTriggers; + Trace("trigger") << std::endl; if( smartTriggers ){ if( d_nodes.size()==1 ){ if( isSimpleTrigger( d_nodes[0] ) ){ @@ -49,6 +50,8 @@ d_quantEngine( qe ), d_f( f ){ } }else{ d_mg = new InstMatchGeneratorMulti( f, d_nodes, qe, matchOption ); + //d_mg = InstMatchGenerator::mkInstMatchGenerator( d_nodes, qe ); + //d_mg->setActiveAdd(); } }else{ d_mg = InstMatchGenerator::mkInstMatchGenerator( d_nodes, qe ); |