diff options
Diffstat (limited to 'src/theory/quantifiers/term_database.cpp')
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 493b9e931..d637fa25f 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -144,7 +144,6 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ computeModelBasisArgAttribute( n ); if( !n.getAttribute(NoMatchAttribute()) ){ if( !d_func_map_trie[ it->first ].addTerm( d_quantEngine, n ) ){ - //only set no match if not a model basis argument term NoMatchAttribute nma; n.setAttribute(nma,true); congruentCount++; @@ -171,7 +170,6 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ if( !en.getAttribute(NoMatchAttribute()) ){ Node op = en.getOperator(); if( !d_pred_map_trie[i][op].addTerm( d_quantEngine, en ) ){ - //only set no match if not a model basis argument term NoMatchAttribute nma; en.setAttribute(nma,true); congruentCount++; |