summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/term_database.cpp
diff options
context:
space:
mode:
authorKshitij Bansal <kshitij@cs.nyu.edu>2013-05-09 17:47:53 -0400
committerKshitij Bansal <kshitij@cs.nyu.edu>2013-05-09 17:47:53 -0400
commit83ecbc2357ffbb7d0772804c360302ca1daa2400 (patch)
tree4b6ec5beb85ce3be22604e7d65aa42dc10d8585b /src/theory/quantifiers/term_database.cpp
parentb53423bcec060d5a49ee2df4d1da55ed289de1d2 (diff)
parent588468e4800d790aecd35725c123d21f3e7a86ae (diff)
Merge branch 'master' of ssh://github.com/CVC4/CVC4
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