diff options
Diffstat (limited to 'src/theory/quantifiers/qinterval_builder.cpp')
| -rwxr-xr-x | src/theory/quantifiers/qinterval_builder.cpp | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/src/theory/quantifiers/qinterval_builder.cpp b/src/theory/quantifiers/qinterval_builder.cpp index ce85cecc0..ece519d1c 100755 --- a/src/theory/quantifiers/qinterval_builder.cpp +++ b/src/theory/quantifiers/qinterval_builder.cpp @@ -1036,14 +1036,12 @@ bool QIntervalBuilder::doExhaustiveInstantiation( FirstOrderModel * fm, Node q, if( fmqint->d_var_order[q]->getInstantiation( fmqint, l, u, inst ) ){
Trace("qint-inst") << "** Instantiate with ";
//just add the instance
- InstMatch m;
for( unsigned j=0; j<inst.size(); j++) {
- m.set( d_qe, q, j, inst[j] );
Trace("qint-inst") << inst[j] << " ";
}
Trace("qint-inst") << std::endl;
d_triedLemmas++;
- if( d_qe->addInstantiation( q, m ) ){
+ if( d_qe->addInstantiation( q, inst ) ){
Trace("qint-inst") << " ...added instantiation." << std::endl;
d_addedLemmas++;
}else{
|