Optimizations for QCF to check relevant domain of variable argument positions eagerly, global ordering mechanism for quantified formulas within check. Refactoring of term database.

1 files changed, 1 insertions, 1 deletions

diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp
index 9181677ee..b353fce2f 100644
--- a/src/theory/quantifiers/relevant_domain.cpp
+++ b/src/theory/quantifiers/relevant_domain.cpp
@@ -95,7 +95,7 @@ void RelevantDomain::compute(){
         it2->second->reset();
       }
     }
-    for( int i=0; i<d_model->getNumAssertedQuantifiers(); i++ ){
+    for( unsigned i=0; i<d_model->getNumAssertedQuantifiers(); i++ ){
       Node q = d_model->getAssertedQuantifier( i );
       Node icf = d_qe->getTermDatabase()->getInstConstantBody( q );
       Trace("rel-dom-debug") << "compute relevant domain for " << icf << std::endl;