diff options
Diffstat (limited to 'src/theory/quantifiers/full_model_check.cpp')
| -rw-r--r-- | src/theory/quantifiers/full_model_check.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index 33c853328..8835d00bc 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -405,7 +405,7 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ bool needsDefault = true; for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){ Node n = fm->d_uf_terms[op][i]; - if( !n.getAttribute(NoMatchAttribute()) ){ + if( d_qe->getTermDatabase()->isTermActive( n ) ){ add_conds.push_back( n ); add_values.push_back( n ); Node r = fm->getUsedRepresentative(n); |