diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2013-05-09 17:47:53 -0400 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2013-05-09 17:47:53 -0400 |
commit | 83ecbc2357ffbb7d0772804c360302ca1daa2400 (patch) | |
tree | 4b6ec5beb85ce3be22604e7d65aa42dc10d8585b /src/theory/quantifiers/term_database.cpp | |
parent | b53423bcec060d5a49ee2df4d1da55ed289de1d2 (diff) | |
parent | 588468e4800d790aecd35725c123d21f3e7a86ae (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.cpp | 3 |
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; |