diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-12-02 06:14:12 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-12-02 06:14:12 -0600 |
| commit | 3179bfe0fff1372b4080196dd28f0079d859830f (patch) | |
| tree | de0e9a9af3eac2fe0c5252aace5e500439e5699d /src/theory/quantifiers/model_builder.cpp | |
| parent | 1edc0786ca4cc2dd60dc66a3ff0ac701b50f4103 (diff) | |
Minor improvements to inst match generator (#1415)
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(); } } } |