diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-10-19 00:56:11 +0000 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-10-19 00:56:11 +0000 |
| commit | 28af31bf1efff6fc143da3a9db9996162c2befab (patch) | |
| tree | 0d2648eaf6b4793c7faf39a99a9b308910d2c046 /src/theory/quantifiers/model_builder.cpp | |
| parent | 7f10c78f572debd0ddf717bfb9f9453a42c015cb (diff) | |
--fallback-sequential / --no-fallback-sequential option
closes bug 419, fix typo, fix warning
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/theory/quantifiers/model_builder.cpp')
| -rw-r--r-- | src/theory/quantifiers/model_builder.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index e0ab047ab..4c30f6841 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -763,7 +763,7 @@ void ModelEngineBuilderInstGen::getParentQuantifierMatch( InstMatch& mp, Node fp int counter = 0; for( size_t i=0; i<fp[0].getNumChildren(); i++ ){ Node icp = d_qe->getTermDatabase()->getInstantiationConstant( fp, i ); - if( counter<f[0].getNumChildren() ){ + if( (int)counter< (int)f[0].getNumChildren() ){ if( fp[0][i]==f[0][counter] ){ Node ic = d_qe->getTermDatabase()->getInstantiationConstant( f, counter ); Node n = m.getValue( ic ); |