diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-02-05 01:35:21 -0600 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-02-05 01:35:21 -0600 |
| commit | 58d58ad5da9bbfbe1df338083fbb2a2e7c8d19e9 (patch) | |
| tree | 2701a84716ed406b1251afadeec67b4f5c100d81 /src/theory/quantifiers/model_builder.cpp | |
| parent | 17cf7ddc9613785a7bfb7d7957f1432a51dd137c (diff) | |
More improvements for E-matching
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() ); |