diff options
| author | Morgan Deters <mdeters@gmail.com> | 2012-06-12 21:29:51 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2012-06-12 21:29:51 +0000 |
| commit | 37a8af9ca9242be9417dd5cea15dd641d18f4b84 (patch) | |
| tree | f1bbff9288fa6034c271e260c74aa40df4104beb | |
| parent | 9348417ac5f12e8269a52a7c9b5a01a4aa558c74 (diff) | |
Fix some compile warnings (but they never showed up on church)
| -rw-r--r-- | src/theory/inst_match.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/inst_match.cpp b/src/theory/inst_match.cpp index e340da75d..32d6c958b 100644 --- a/src/theory/inst_match.cpp +++ b/src/theory/inst_match.cpp @@ -167,7 +167,7 @@ void InstMatch::computeTermVec( const std::vector< Node >& vars, std::vector< No /** add match m for quantifier f starting at index, take into account equalities q, return true if successful */ void InstMatchTrie::addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, int index, ImtIndexOrder* imtio ){ - if( long(index)<f[0].getNumChildren() && ( !imtio || long(index)<imtio->d_order.size() ) ){ + if( long(index)<long(f[0].getNumChildren()) && ( !imtio || long(index)<long(imtio->d_order.size()) ) ){ int i_index = imtio ? imtio->d_order[index] : index; Node n = m.d_map[ qe->getInstantiationConstant( f, i_index ) ]; d_data[n].addInstMatch2( qe, f, m, index+1, imtio ); @@ -176,7 +176,7 @@ void InstMatchTrie::addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, /** exists match */ bool InstMatchTrie::existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, int index, ImtIndexOrder* imtio ){ - if( long(index)==f[0].getNumChildren() || ( imtio && long(index)==imtio->d_order.size() ) ){ + if( long(index)==long(f[0].getNumChildren()) || ( imtio && long(index)==long(imtio->d_order.size()) ) ){ return true; }else{ int i_index = imtio ? imtio->d_order[index] : index; |