From 28af31bf1efff6fc143da3a9db9996162c2befab Mon Sep 17 00:00:00 2001
From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Fri, 19 Oct 2012 00:56:11 +0000
Subject: --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.)
---
 src/theory/quantifiers/model_builder.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src/theory')

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 );
-- 
cgit v1.2.3