summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/term_database.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/term_database.cpp')
-rw-r--r--src/theory/quantifiers/term_database.cpp3
1 files changed, 1 insertions, 2 deletions
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 3153a3c64..417b4ae3a 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -254,8 +254,7 @@ void TermDb::computeModelBasisArgAttribute( Node n ){
//determine if it has model basis attribute
for( int j=0; j<(int)n.getNumChildren(); j++ ){
if( n[j].getAttribute(ModelBasisAttribute()) ){
- val = 1;
- break;
+ val++;
}
}
ModelBasisArgAttribute mbaa;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback