diff options
Diffstat (limited to 'src/theory/quantifiers/full_model_check.cpp')
| -rw-r--r-- | src/theory/quantifiers/full_model_check.cpp | 12 |
1 files changed, 2 insertions, 10 deletions
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index c7d7b7415..d542e878c 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -672,12 +672,8 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, } }else{ //just add the instance - InstMatch m; - for( unsigned j=0; j<inst.size(); j++) { - m.set( d_qe, f, j, inst[j] ); - } d_triedLemmas++; - if( d_qe->addInstantiation( f, m ) ){ + if( d_qe->addInstantiation( f, inst ) ){ Trace("fmc-debug-inst") << "** Added instantiation." << std::endl; d_addedLemmas++; }else{ @@ -792,13 +788,9 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No Trace("fmc-exh-debug") << ", index = " << ev_index << " / " << d_quant_models[f].d_value.size(); Node ev = ev_index==-1 ? Node::null() : d_quant_models[f].d_value[ev_index]; if (ev!=d_true) { - InstMatch m; - for( unsigned i=0; i<inst.size(); i++ ){ - m.set( d_qe, f, i, inst[i] ); - } Trace("fmc-exh-debug") << ", add!"; //add as instantiation - if( d_qe->addInstantiation( f, m ) ){ + if( d_qe->addInstantiation( f, inst ) ){ Trace("fmc-exh-debug") << " ...success."; addedLemmas++; }else{ |