summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/ambqi_builder.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/ambqi_builder.cpp')
-rwxr-xr-x[-rw-r--r--]src/theory/quantifiers/ambqi_builder.cpp2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp
index 5192da7de..97116dee4 100644..100755
--- a/src/theory/quantifiers/ambqi_builder.cpp
+++ b/src/theory/quantifiers/ambqi_builder.cpp
@@ -787,7 +787,7 @@ void AbsMbqiBuilder::processBuildModel(TheoryModel* m, bool fullModel) {
Trace("ambqi-model-debug") << "Initial terms: " << std::endl;
for( size_t i=0; i<fm->d_uf_terms[f].size(); i++ ){
Node n = fm->d_uf_terms[f][i];
- if( !n.getAttribute(NoMatchAttribute()) ){
+ if( d_qe->getTermDatabase()->isTermActive( n ) ){
Trace("ambqi-model-debug") << " " << n << " -> " << fm->getRepresentativeId( n ) << std::endl;
fapps.push_back( n );
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback