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 dba04ce51..fbd122bd6 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -717,7 +717,7 @@ int QModelBuilderDefault::doInstGen( FirstOrderModel* fm, Node f ){ tr->reset( Node::null() ); //d_qe->d_optInstMakeRepresentative = false; //d_qe->d_optMatchIgnoreModelBasis = true; - addedLemmas += tr->addInstantiations( d_quant_basis_match[f] ); + addedLemmas += tr->addInstantiations(); } } } |