diff options
Diffstat (limited to 'src/theory/quantifiers/model_builder.cpp')
-rw-r--r-- | src/theory/quantifiers/model_builder.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index 2f44140c2..d1c04ceab 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -526,7 +526,7 @@ int ModelEngineBuilderDefault::doInstGen( FirstOrderModel* fm, Node f ){ //if applicable, try to add exceptions here if( !tr_terms.empty() ){ //make a trigger for these terms, add instantiations - inst::Trigger* tr = inst::Trigger::mkTrigger( d_qe, f, tr_terms ); + inst::Trigger* tr = inst::Trigger::mkTrigger( d_qe, f, tr_terms, 0, true, inst::Trigger::TR_MAKE_NEW, options::smartTriggers() ); //Notice() << "Trigger = " << (*tr) << std::endl; tr->resetInstantiationRound(); tr->reset( Node::null() ); |