Bug fixes for bounded integer quantification. Current best strategy is to turn off MBQI. Disable relevant triggers by default.

13 files changed, 267 insertions, 159 deletions

diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index 30ff5242b..ab6b35e01 100644
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -190,7 +190,6 @@ void BoundedIntegers::processLiteral( Node f, Node lit, bool pol,
     }
   }else if( lit.getKind()==LEQ || lit.getKind()==LT || lit.getKind()==GT ) {
     Message() << "BoundedIntegers : Bad kind for literal : " << lit << std::endl;
-    exit(0);
   }
 }
 
@@ -232,7 +231,7 @@ void BoundedIntegers::registerQuantifier( Node f ) {
     if( f[0][i].getType().isInteger() ){
       hasIntType = true;
     }
-    else if( f[0][i].getType().isSort() ){
+    else if( f[0][i].getType().isSort() || f[0][i].getType().getCardinality().isFinite() ){
       finiteTypes++;
     }
   }
@@ -292,6 +291,7 @@ void BoundedIntegers::registerQuantifier( Node f ) {
       }
     }else{
       Trace("bound-int-warn") << "Warning : Bounded Integers : Could not find bounds for " << f << std::endl;
+      //Message() << "Bound integers : Cannot infer bounds of " << f << std::endl;
     }
   }
 }
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 63cac9c15..fa4961352 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -668,13 +668,19 @@ Node FirstOrderModelFmc::getInterval( Node lb, Node ub ){
 }
 
 bool FirstOrderModelFmc::isInRange( Node v, Node i ) {
-  for( unsigned b=0; b<2; b++ ){
-    if( !isStar( i[b] ) ){
-      if( ( b==0 && i[b].getConst<Rational>() > v.getConst<Rational>() ) ||
-          ( b==1 && i[b].getConst<Rational>() <= v.getConst<Rational>() ) ){
-        return false;
+  if( isStar( i ) ){
+    return true;
+  }else if( isInterval( i ) ){
+    for( unsigned b=0; b<2; b++ ){
+      if( !isStar( i[b] ) ){
+        if( ( b==0 && i[b].getConst<Rational>() > v.getConst<Rational>() ) ||
+            ( b==1 && i[b].getConst<Rational>() <= v.getConst<Rational>() ) ){
+          return false;
+        }
       }
     }
+    return true;
+  }else{
+    return v==i;
   }
-  return true;
 }
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index bf10369e6..c22d903f9 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -92,10 +92,10 @@ int EntryTrie::getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node>
     int minIndex = -1;
     if( options::fmfFmcInterval() && inst[index].getType().isInteger() ){
       for( std::map<Node,EntryTrie>::iterator it = d_child.begin(); it != d_child.end(); ++it ){
-        if( !m->isInterval( it->first ) ){
-          std::cout << "Not an interval during getGenIndex " << it->first << std::endl;
-          exit( 11 );
-        }
+        //if( !m->isInterval( it->first ) ){
+        //  std::cout << "Not an interval during getGenIndex " << it->first << std::endl;
+        //  exit( 11 );
+        //}
         //check if it is in the range
         if( m->isInRange(inst[index], it->first )  ){
           int gindex = it->second.getGeneralizationIndex(m, inst, index+1);
@@ -392,13 +392,6 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
       fm->d_models[op]->reset();
 
       Trace("fmc-model-debug") << fm->d_uf_terms[op].size() << " model values for " << op << " ... " << std::endl;
-      for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){
-        Node r = fm->getUsedRepresentative(fm->d_uf_terms[op][i]);
-        Trace("fmc-model-debug") << fm->d_uf_terms[op][i] << " -> " << r << std::endl;
-      }
-      Trace("fmc-model-debug") << std::endl;
-
-
       std::vector< Node > add_conds;
       std::vector< Node > add_values;
       bool needsDefault = true;
@@ -407,8 +400,12 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
         if( !n.getAttribute(NoMatchAttribute()) ){
           add_conds.push_back( n );
           add_values.push_back( n );
+          Node r = fm->getUsedRepresentative(n);
+          Trace("fmc-model-debug") << n << " -> " << r << std::endl;
+          //AlwaysAssert( fm->areEqual( fm->d_uf_terms[op][i], r ) );
         }
       }
+      Trace("fmc-model-debug") << std::endl;
       //possibly get default
       if( needsDefault ){
         Node nmb = d_qe->getTermDatabase()->getModelBasisOpTerm(op);
@@ -487,43 +484,7 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
 
 
       if( options::fmfFmcInterval() ){
-        Trace("fmc-interval-model") << "Changing to interval model, Before : " << std::endl;
-        fm->d_models[op]->debugPrint("fmc-interval-model", op, this);
-        Trace("fmc-interval-model") << std::endl;
-        std::vector< int > indices;
-        for( int i=0; i<(int)fm->d_models[op]->d_cond.size(); i++ ){
-          indices.push_back( i );
-        }
-        std::map< int, std::map< int, Node > > changed_vals;
-        makeIntervalModel( fm, op, indices, 0, changed_vals );
-
-        std::vector< Node > conds;
-        std::vector< Node > values;
-        for( unsigned i=0; i<fm->d_models[op]->d_cond.size(); i++ ){
-          if( changed_vals.find(i)==changed_vals.end() ){
-            conds.push_back( fm->d_models[op]->d_cond[i] );
-          }else{
-            std::vector< Node > children;
-            children.push_back( op );
-            for( unsigned j=0; j<fm->d_models[op]->d_cond[i].getNumChildren(); j++ ){
-              if( changed_vals[i].find(j)==changed_vals[i].end() ){
-                children.push_back( fm->d_models[op]->d_cond[i][j] );
-              }else{
-                children.push_back( changed_vals[i][j] );
-              }
-            }
-            Node nc = NodeManager::currentNM()->mkNode( APPLY_UF, children );
-            conds.push_back( nc );
-            Trace("fmc-interval-model") << "Interval : Entry #" << i << " changed to ";
-            debugPrintCond("fmc-interval-model", nc, true );
-            Trace("fmc-interval-model") << std::endl;
-          }
-          values.push_back( fm->d_models[op]->d_value[i] );
-        }
-        fm->d_models[op]->reset();
-        for( unsigned i=0; i<conds.size(); i++ ){
-          fm->d_models[op]->addEntry(fm, conds[i], values[i] );
-        }
+        convertIntervalModel( fm, op );
       }
 
       Trace("fmc-model-simplify") << "Before simplification : " << std::endl;
@@ -535,6 +496,20 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
 
       fm->d_models[op]->debugPrint("fmc-model", op, this);
       Trace("fmc-model") << std::endl;
+
+      //for debugging
+      /*
+      for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){
+        std::vector< Node > inst;
+        for( unsigned j=0; j<fm->d_uf_terms[op][i].getNumChildren(); j++ ){
+          Node r = fm->getUsedRepresentative( fm->d_uf_terms[op][i][j] );
+          inst.push_back( r );
+        }
+        Node ev = fm->d_models[op]->evaluate( fm, inst );
+        Trace("fmc-model-debug") << ".....Checking eval( " << fm->d_uf_terms[op][i] << " ) = " << ev << std::endl;
+        AlwaysAssert( fm->areEqual( ev, fm->d_uf_terms[op][i] ) );
+      }
+      */
     }
   }
   if( fullModel ){
@@ -588,7 +563,7 @@ void FullModelChecker::debugPrint(const char * tr, Node n, bool dispStar) {
     debugPrint(tr, n[1], dispStar );
   }else{
     TypeNode tn = n.getType();
-    if( d_rep_ids.find(tn)!=d_rep_ids.end() ){
+    if( tn.isSort() && d_rep_ids.find(tn)!=d_rep_ids.end() ){
       if (d_rep_ids[tn].find(n)!=d_rep_ids[tn].end()) {
         Trace(tr) << d_rep_ids[tn][n];
       }else{
@@ -622,79 +597,100 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f,
         initializeType( fmfmc, f[0][i].getType() );
       }
 
-      //model check the quantifier
-      doCheck(fmfmc, f, d_quant_models[f], f[1]);
-      Trace("fmc") << "Definition for quantifier " << f << " is : " << std::endl;
-      d_quant_models[f].debugPrint("fmc", Node::null(), this);
-      Trace("fmc") << std::endl;
-
-      //consider all entries going to non-true
-      for (unsigned i=0; i<d_quant_models[f].d_cond.size(); i++) {
-        if( d_quant_models[f].d_value[i]!=d_true) {
-          Trace("fmc-inst") << "Instantiate based on " << d_quant_models[f].d_cond[i] << "..." << std::endl;
-          bool hasStar = false;
-          std::vector< Node > inst;
-          for (unsigned j=0; j<d_quant_models[f].d_cond[i].getNumChildren(); j++) {
-            if (fmfmc->isStar(d_quant_models[f].d_cond[i][j])) {
-              hasStar = true;
-              inst.push_back(fmfmc->getModelBasisTerm(d_quant_models[f].d_cond[i][j].getType()));
-            }else if( fmfmc->isInterval(d_quant_models[f].d_cond[i][j])){
-              hasStar = true;
-              //if interval, find a sample point
-              if( fmfmc->isStar(d_quant_models[f].d_cond[i][j][0]) ){
-                if( fmfmc->isStar(d_quant_models[f].d_cond[i][j][1]) ){
-                  inst.push_back(fmfmc->getModelBasisTerm(d_quant_models[f].d_cond[i][j][1].getType()));
+      if( !options::fmfModelBasedInst() ){
+        //just exhaustive instantiate
+        Node c = mkCondDefault( fmfmc, f );
+        d_quant_models[f].addEntry( fmfmc, c, d_false );
+        return exhaustiveInstantiate( fmfmc, f, c, -1);
+      }else{
+        //model check the quantifier
+        doCheck(fmfmc, f, d_quant_models[f], f[1]);
+        Trace("fmc") << "Definition for quantifier " << f << " is : " << std::endl;
+        d_quant_models[f].debugPrint("fmc", Node::null(), this);
+        Trace("fmc") << std::endl;
+
+        //consider all entries going to non-true
+        for (unsigned i=0; i<d_quant_models[f].d_cond.size(); i++) {
+          if( d_quant_models[f].d_value[i]!=d_true) {
+            Trace("fmc-inst") << "Instantiate based on " << d_quant_models[f].d_cond[i] << "..." << std::endl;
+            bool hasStar = false;
+            std::vector< Node > inst;
+            for (unsigned j=0; j<d_quant_models[f].d_cond[i].getNumChildren(); j++) {
+              if (fmfmc->isStar(d_quant_models[f].d_cond[i][j])) {
+                hasStar = true;
+                inst.push_back(fmfmc->getModelBasisTerm(d_quant_models[f].d_cond[i][j].getType()));
+              }else if( fmfmc->isInterval(d_quant_models[f].d_cond[i][j])){
+                hasStar = true;
+                //if interval, find a sample point
+                if( fmfmc->isStar(d_quant_models[f].d_cond[i][j][0]) ){
+                  if( fmfmc->isStar(d_quant_models[f].d_cond[i][j][1]) ){
+                    inst.push_back(fmfmc->getModelBasisTerm(d_quant_models[f].d_cond[i][j][1].getType()));
+                  }else{
+                    Node nn = NodeManager::currentNM()->mkNode( MINUS, d_quant_models[f].d_cond[i][j][1],
+                                                                NodeManager::currentNM()->mkConst( Rational(1) ) );
+                    nn = Rewriter::rewrite( nn );
+                    inst.push_back( nn );
+                  }
                 }else{
-                  Node nn = NodeManager::currentNM()->mkNode( MINUS, d_quant_models[f].d_cond[i][j][1],
-                                                              NodeManager::currentNM()->mkConst( Rational(1) ) );
-                  nn = Rewriter::rewrite( nn );
-                  inst.push_back( nn );
+                  inst.push_back(d_quant_models[f].d_cond[i][j][0]);
                 }
               }else{
-                inst.push_back(d_quant_models[f].d_cond[i][j][0]);
+                inst.push_back(d_quant_models[f].d_cond[i][j]);
               }
-            }else{
-              inst.push_back(d_quant_models[f].d_cond[i][j]);
             }
-          }
-          bool addInst = true;
-          if( hasStar ){
-            //try obvious (specified by inst)
-            Node ev = d_quant_models[f].evaluate(fmfmc, inst);
-            if (ev==d_true) {
-              addInst = false;
-            }
-          }else{
-            //for debugging
-            if (Trace.isOn("fmc-test-inst")) {
+            bool addInst = true;
+            if( hasStar ){
+              //try obvious (specified by inst)
               Node ev = d_quant_models[f].evaluate(fmfmc, inst);
-              if( ev==d_true ){
-                std::cout << "WARNING: instantiation was true! " << f << " " << d_quant_models[f].d_cond[i] << std::endl;
-                exit(0);
-              }else{
-                Trace("fmc-test-inst") << "...instantiation evaluated to false." << std::endl;
+              if (ev==d_true) {
+                addInst = false;
+              }
+            }else{
+              //for debugging
+              if (Trace.isOn("fmc-test-inst")) {
+                Node ev = d_quant_models[f].evaluate(fmfmc, inst);
+                if( ev==d_true ){
+                  std::cout << "WARNING: instantiation was true! " << f << " " << d_quant_models[f].d_cond[i] << std::endl;
+                  exit(0);
+                }else{
+                  Trace("fmc-test-inst") << "...instantiation evaluated to false." << std::endl;
+                }
               }
             }
-          }
-          if( addInst ){
-            InstMatch m;
-            for( unsigned j=0; j<inst.size(); j++) {
-              m.set( d_qe, f, j, inst[j] );
-            }
-            d_triedLemmas++;
-            if( d_qe->addInstantiation( f, m ) ){
-              Trace("fmc-debug-inst") << "** Added instantiation." << std::endl;
-              d_addedLemmas++;
+            if( addInst ){
+              if( options::fmfBoundInt() ){
+                std::vector< Node > cond;
+                cond.push_back(d_quant_cond[f]);
+                cond.insert( cond.end(), inst.begin(), inst.end() );
+                //need to do exhaustive instantiate algorithm to set things properly (should only add one instance)
+                Node c = mkCond( cond );
+                int prevInst = d_addedLemmas;
+                exhaustiveInstantiate( fmfmc, f, c, -1 );
+                if( d_addedLemmas==prevInst ){
+                  d_star_insts[f].push_back(i);
+                }
+              }else{
+                //just add the instance
+                InstMatch m;
+                for( unsigned j=0; j<inst.size(); j++) {
+                  m.set( d_qe, f, j, inst[j] );
+                }
+                d_triedLemmas++;
+                if( d_qe->addInstantiation( f, m ) ){
+                  Trace("fmc-debug-inst") << "** Added instantiation." << std::endl;
+                  d_addedLemmas++;
+                }else{
+                  Trace("fmc-debug-inst") << "** Instantiation was duplicate." << std::endl;
+                  //this can happen if evaluation is unknown
+                  //might try it next effort level
+                  d_star_insts[f].push_back(i);
+                }
+              }
             }else{
-              Trace("fmc-debug-inst") << "** Instantiation was duplicate." << std::endl;
-              //this can happen if evaluation is unknown
+              Trace("fmc-debug-inst") << "** Instantiation was already true." << std::endl;
               //might try it next effort level
               d_star_insts[f].push_back(i);
             }
-          }else{
-            Trace("fmc-debug-inst") << "** Instantiation was already true." << std::endl;
-            //might try it next effort level
-            d_star_insts[f].push_back(i);
           }
         }
       }
@@ -726,7 +722,7 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f,
 
 bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index) {
   RepSetIterator riter( d_qe, &(fm->d_rep_set) );
-  Trace("fmc-exh") << "Exhaustive instantiate based on index " << c_index << " : " << c << " ";
+  Trace("fmc-exh") << "----Exhaustive instantiate based on index " << c_index << " : " << c << " ";
   debugPrintCond("fmc-exh", c, true);
   Trace("fmc-exh")<< std::endl;
   Trace("fmc-exh-debug") << "Set interval domains..." << std::endl;
@@ -761,10 +757,12 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No
               riter.d_domain[i].clear();
               riter.d_domain[i].push_back(d_rep_ids[tn][c[i]]);
             }else{
+              Trace("fmc-exh") << "---- Does not have rep : " << c[i] << " for type " << tn << std::endl;
               return false;
             }
           }
         }else{
+          Trace("fmc-exh") << "---- Does not have type : " << tn << std::endl;
           return false;
         }
       }
@@ -774,27 +772,36 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No
     while( !riter.isFinished() ){
       d_triedLemmas++;
       Trace("fmc-exh-debug") << "Inst : ";
+      std::vector< Node > ev_inst;
       std::vector< Node > inst;
       for( int i=0; i<riter.getNumTerms(); i++ ){
-        //m.set( d_quantEngine, f, riter.d_index_order[i], riter.getTerm( i ) );
-        Node r = fm->getUsedRepresentative( riter.getTerm( i ) );
+        Node rr = riter.getTerm( i );
+        Node r = rr;
+        if( r.getType().isSort() ){
+          r = fm->getUsedRepresentative( r );
+        }else{
+          r = fm->getCurrentModelValue( r );
+        }
         debugPrint("fmc-exh-debug", r);
-        Trace("fmc-exh-debug") << " ";
-        inst.push_back(r);
+        Trace("fmc-exh-debug") << " (term : " << rr << ")";
+        ev_inst.push_back( r );
+        inst.push_back( rr );
       }
-      int ev_index = d_quant_models[f].getGeneralizationIndex(fm, inst);
+      int ev_index = d_quant_models[f].getGeneralizationIndex(fm, ev_inst);
       Trace("fmc-exh-debug") << ", index = " << ev_index << " / " << d_quant_models[f].d_value.size();
       Node ev = ev_index==-1 ? Node::null() : d_quant_models[f].d_value[ev_index];
       if (ev!=d_true) {
         InstMatch m;
-        for( int i=0; i<riter.getNumTerms(); i++ ){
-          m.set( d_qe, f, i, riter.getTerm( i ) );
+        for( unsigned i=0; i<inst.size(); i++ ){
+          m.set( d_qe, f, i, inst[i] );
         }
         Trace("fmc-exh-debug") << ", add!";
         //add as instantiation
         if( d_qe->addInstantiation( f, m ) ){
           Trace("fmc-exh-debug")  << " ...success.";
           addedLemmas++;
+        }else{
+          Trace("fmc-exh-debug") << ", failed.";
         }
       }else{
         Trace("fmc-exh-debug") << ", already true";
@@ -808,8 +815,10 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No
       }
     }
     d_addedLemmas += addedLemmas;
+    Trace("fmc-exh") << "----Finished Exhaustive instantiate, lemmas = " << addedLemmas << std::endl;
     return true;
   }else{
+    Trace("fmc-exh") << "----Finished Exhaustive instantiate, failed." << std::endl;
     return false;
   }
 }
@@ -1048,7 +1057,7 @@ void FullModelChecker::doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f,
                                                 std::map< int, Node > & entries, int index,
                                                 std::vector< Node > & cond, std::vector< Node > & val,
                                                 EntryTrie & curr ) {
-  Trace("fmc-uf-process") << "compose " << index << std::endl;
+  Trace("fmc-uf-process") << "compose " << index << " / " << val.size() << std::endl;
   for( unsigned i=1; i<cond.size(); i++) {
     debugPrint("fmc-uf-process", cond[i], true);
     Trace("fmc-uf-process") << " ";
@@ -1060,6 +1069,7 @@ void FullModelChecker::doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f,
     entries[curr.d_data] = c;
   }else{
     Node v = val[index];
+    Trace("fmc-uf-process") << "Process " << v << std::endl;
     bool bind_var = false;
     if( !v.isNull() && v.getKind()==kind::BOUND_VARIABLE ){
       int j = getVariableId(f, v);
@@ -1193,15 +1203,23 @@ bool FullModelChecker::doMeet( FirstOrderModelFmc * fm, std::vector< Node > & co
 }
 
 Node FullModelChecker::doIntervalMeet( FirstOrderModelFmc * fm, Node i1, Node i2, bool mk ) {
+  Trace("fmc-debug2") << "Interval meet : " << i1 << " " << i2 << " " << mk << std::endl;
   if( fm->isStar( i1 ) ){
     return i2;
   }else if( fm->isStar( i2 ) ){
     return i1;
-  }else{
-    if( !fm->isInterval( i1 ) || !fm->isInterval( i2 ) ){
-      std::cout << "Not interval during meet! " << i1 << " " << i2 << std::endl;
-      exit( 0 );
+  }else if( !fm->isInterval( i1 ) && fm->isInterval( i2 ) ){
+    return doIntervalMeet( fm, i2, i1, mk );
+  }else if( !fm->isInterval( i2 ) ){
+    if( fm->isInterval( i1 ) ){
+      if( fm->isInRange( i2, i1 ) ){
+        return i2;
+      }
+    }else if( i1==i2 ){
+      return i1;
     }
+    return Node::null();
+  }else{
     Node b[2];
     for( unsigned j=0; j<2; j++ ){
       Node b1 = i1[j];
@@ -1329,6 +1347,46 @@ bool FullModelChecker::useSimpleModels() {
   return options::fmfFmcSimple();
 }
 
+void FullModelChecker::convertIntervalModel( FirstOrderModelFmc * fm, Node op ){
+  Trace("fmc-interval-model") << "Changing to interval model, Before : " << std::endl;
+  fm->d_models[op]->debugPrint("fmc-interval-model", op, this);
+  Trace("fmc-interval-model") << std::endl;
+  std::vector< int > indices;
+  for( int i=0; i<(int)fm->d_models[op]->d_cond.size(); i++ ){
+    indices.push_back( i );
+  }
+  std::map< int, std::map< int, Node > > changed_vals;
+  makeIntervalModel( fm, op, indices, 0, changed_vals );
+
+  std::vector< Node > conds;
+  std::vector< Node > values;
+  for( unsigned i=0; i<fm->d_models[op]->d_cond.size(); i++ ){
+    if( changed_vals.find(i)==changed_vals.end() ){
+      conds.push_back( fm->d_models[op]->d_cond[i] );
+    }else{
+      std::vector< Node > children;
+      children.push_back( op );
+      for( unsigned j=0; j<fm->d_models[op]->d_cond[i].getNumChildren(); j++ ){
+        if( changed_vals[i].find(j)==changed_vals[i].end() ){
+          children.push_back( fm->d_models[op]->d_cond[i][j] );
+        }else{
+          children.push_back( changed_vals[i][j] );
+        }
+      }
+      Node nc = NodeManager::currentNM()->mkNode( APPLY_UF, children );
+      conds.push_back( nc );
+      Trace("fmc-interval-model") << "Interval : Entry #" << i << " changed to ";
+      debugPrintCond("fmc-interval-model", nc, true );
+      Trace("fmc-interval-model") << std::endl;
+    }
+    values.push_back( fm->d_models[op]->d_value[i] );
+  }
+  fm->d_models[op]->reset();
+  for( unsigned i=0; i<conds.size(); i++ ){
+    fm->d_models[op]->addEntry(fm, conds[i], values[i] );
+  }
+}
+
 void FullModelChecker::makeIntervalModel( FirstOrderModelFmc * fm, Node op, std::vector< int > & indices, int index,
                                           std::map< int, std::map< int, Node > >& changed_vals ) {
   if( index==(int)fm->d_models[op]->d_cond[0].getNumChildren() ){
diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h
index 6bb375c34..abe05d3c7 100644
--- a/src/theory/quantifiers/full_model_check.h
+++ b/src/theory/quantifiers/full_model_check.h
@@ -100,6 +100,7 @@ protected:
                           std::map< int, std::map< int, Node > >& changed_vals );
   void makeIntervalModel( FirstOrderModelFmc * fm, Node op, std::vector< int > & indices, int index,
                           std::map< int, std::map< int, Node > >& changed_vals );
+  void convertIntervalModel( FirstOrderModelFmc * fm, Node op );
 private:
   void doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n );
 
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 628f8b14a..fa7b4e342 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -181,6 +181,16 @@ bool InstantiationEngine::needsCheck( Theory::Effort e ){
   }else{
     d_performCheck = true;
   }
+  static int ierCounter2 = 0;
+  if( e==Theory::EFFORT_LAST_CALL ){
+    ierCounter2++;
+    //with bounded integers, skip every other last call,
+    // since matching loops may occur with infinite quantification
+    if( ierCounter2%2==0 && options::fmfBoundInt() ){
+      d_performCheck = false;
+    }
+  }
+
   return d_performCheck;
 }
 
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index 5edf2de96..ea6f2d775 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -44,7 +44,7 @@ bool QModelBuilder::isQuantifierActive( Node f ) {
 
 
 bool QModelBuilder::optUseModel() {
-  return options::fmfModelBasedInst();
+  return options::fmfModelBasedInst() || options::fmfBoundInt();
 }
 
 void QModelBuilder::debugModel( FirstOrderModel* fm ){
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index b1a0c4ed4..5ff21bcff 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -34,7 +34,7 @@ using namespace CVC4::theory::inst;
 ModelEngine::ModelEngine( context::Context* c, QuantifiersEngine* qe ) :
 QuantifiersModule( qe ){
 
-  if( options::fmfFullModelCheck() ){
+  if( options::fmfFullModelCheck() || options::fmfBoundInt() ){
     d_builder = new fmcheck::FullModelChecker( c, qe );
   }else if( options::fmfNewInstGen() ){
     d_builder = new QModelBuilderInstGen( c, qe );
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index fd114df04..1eb98e7b7 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -58,7 +58,7 @@ option foPropQuant --fo-prop-quant bool :default false
 option smartTriggers /--disable-smart-triggers bool :default true
  disable smart triggers
 # Whether to use relevent triggers
-option relevantTriggers /--disable-relevant-triggers bool :default true
+option relevantTriggers --relevant-triggers bool :default false
  prefer triggers that are more relevant based on SInE style analysis
 option relationalTriggers --relational-triggers bool :default false
  choose relational triggers such as x = f(y), x >= f(y)
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 07b0ebea3..54aa7f726 100755
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -50,7 +50,7 @@ d_lemmas_produced_c(u){
   d_hasAddedLemma = false;
 
   //the model object
-  if( options::fmfFullModelCheck() ){
+  if( options::fmfFullModelCheck() || options::fmfBoundInt() ){
     d_model = new quantifiers::fmcheck::FirstOrderModelFmc( this, c, "FirstOrderModelFmc" );
   }else{
     d_model = new quantifiers::FirstOrderModelIG( c, "FirstOrderModelIG" );
@@ -283,6 +283,10 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std
     d_temp_inst_debug[f]++;
     d_total_inst_count_debug++;
     Trace("inst") << "*** Instantiate " << f << " with " << std::endl;
+    for( int i=0; i<(int)terms.size(); i++ ){
+      Trace("inst") << "   " << terms[i];
+      Trace("inst") << std::endl;
+    }
     //uint64_t maxInstLevel = 0;
     if( options::cbqi() ){
       for( int i=0; i<(int)terms.size(); i++ ){
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index 800e007f7..169688243 100644
--- a/src/theory/rep_set.cpp
+++ b/src/theory/rep_set.cpp
@@ -252,6 +252,7 @@ bool RepSetIterator::resetIndex( int i, bool initial ) {
   if( d_enum_type[ii]==ENUM_RANGE ){
     if( initial || ( d_qe->getBoundedIntegers() && !d_qe->getBoundedIntegers()->isGroundRange( d_owner, d_owner[0][ii] ) ) ){
       Trace("bound-int-rsi") << "Getting range of " << d_owner[0][ii] << std::endl;
+      Node actual_l;
       Node l, u;
       if( d_qe->getBoundedIntegers() && d_qe->getBoundedIntegers()->isBoundVar( d_owner, d_owner[0][ii] ) ){
         d_qe->getBoundedIntegers()->getBoundValues( d_owner, d_owner[0][ii], this, l, u );
@@ -260,6 +261,10 @@ bool RepSetIterator::resetIndex( int i, bool initial ) {
         if( d_bounds[b].find(ii)!=d_bounds[b].end() ){
           Trace("bound-int-rsi") << "May further limit bound(" << b << ") based on " << d_bounds[b][ii] << std::endl;
           if( b==0 && (l.isNull() || d_bounds[b][ii].getConst<Rational>() > l.getConst<Rational>()) ){
+            if( !l.isNull() ){
+              //bound was limited externally, record that the value lower bound is not equal to the term lower bound
+              actual_l = NodeManager::currentNM()->mkNode( MINUS, d_bounds[b][ii], l );
+            }
             l = d_bounds[b][ii];
           }else if( b==1 && (u.isNull() || d_bounds[b][ii].getConst<Rational>() <= u.getConst<Rational>()) ){
             u = NodeManager::currentNM()->mkNode( MINUS, d_bounds[b][ii],
@@ -284,6 +289,10 @@ bool RepSetIterator::resetIndex( int i, bool initial ) {
           d_qe->getBoundedIntegers()->getBounds( d_owner, d_owner[0][ii], this, tl, tu );
         }
         d_lower_bounds[ii] = tl;
+        if( !actual_l.isNull() ){
+          //if bound was limited externally, must consider the offset
+          d_lower_bounds[ii] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( PLUS, tl, actual_l ) );
+        }
         if( ra==NodeManager::currentNM()->mkConst(true) ){
           long rr = range.getConst<Rational>().getNumerator().getLong()+1;
           Trace("bound-int-rsi")  << "Actual bound range is " << rr << std::endl;
@@ -355,7 +364,7 @@ Node RepSetIterator::getTerm( int i ){
     Assert( d_rep_set->d_type_reps.find( tn )!=d_rep_set->d_type_reps.end() );
     return d_rep_set->d_type_reps[tn][d_domain[index][d_index[index]]];
   }else{
-    Trace("rsi-debug") << index << " " << d_lower_bounds[index] << " " << d_index[index] << std::endl;
+    Trace("rsi-debug") << "Get, with offset : " << index << " " << d_lower_bounds[index] << " " << d_index[index] << std::endl;
     Node t = NodeManager::currentNM()->mkNode(PLUS, d_lower_bounds[index],
                                                     NodeManager::currentNM()->mkConst( Rational(d_index[index]) ) );
     t = Rewriter::rewrite( t );
diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp
index c0d114052..284212ba9 100644
--- a/src/theory/uf/theory_uf_model.cpp
+++ b/src/theory/uf/theory_uf_model.cpp
@@ -345,14 +345,14 @@ void UfModelTreeGenerator::setValue( TheoryModel* m, Node n, Node v, bool ground
   d_set_values[ isReq ? 1 : 0 ][ ground ? 1 : 0 ][n] = v;
   if( optUsePartialDefaults() ){
     if( !ground ){
-      int defSize = (int)d_defaults.size();
-      for( int i=0; i<defSize; i++ ){
-        //for soundness, to allow variable order-independent function interpretations,
-        //  we must ensure that the intersection of all default terms
-        //  is also defined.
-        //for example, if we have that f( e, a ) = ..., and f( b, e ) = ...,
-        //  then we must define f( b, a ).
-        if (!options::fmfFullModelCheck()) {
+      if (!options::fmfFullModelCheck()) {
+        int defSize = (int)d_defaults.size();
+        for( int i=0; i<defSize; i++ ){
+          //for soundness, to allow variable order-independent function interpretations,
+          //  we must ensure that the intersection of all default terms
+          //  is also defined.
+          //for example, if we have that f( e, a ) = ..., and f( b, e ) = ...,
+          //  then we must define f( b, a ).
           bool isGround;
           Node ni = getIntersection( m, n, d_defaults[i], isGround );
           if( !ni.isNull() ){
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index 8aa7d625d..4ef11c042 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -542,7 +542,9 @@ void StrongSolverTheoryUF::SortModel::assertDisequal( Node a, Node b, Node reaso
       //if they are not already disequal
       a = d_thss->getTheory()->d_equalityEngine.getRepresentative( a );
       b = d_thss->getTheory()->d_equalityEngine.getRepresentative( b );
-      if( !d_thss->getTheory()->d_equalityEngine.areDisequal( a, b, true ) ){
+      int ai = d_regions_map[a];
+      int bi = d_regions_map[b];
+      if( !d_regions[ai]->isDisequal( a, b, ai==bi ) ){
         Debug("uf-ss") << "Assert disequal " << a << " != " << b << "..." << std::endl;
         //if( reason.getKind()!=NOT || ( reason[0].getKind()!=EQUAL && reason[0].getKind()!=IFF ) ||
         //    a!=reason[0][0] || b!=reason[0][1] ){
@@ -559,8 +561,6 @@ void StrongSolverTheoryUF::SortModel::assertDisequal( Node a, Node b, Node reaso
         //now, add disequalities to regions
         Assert( d_regions_map.find( a )!=d_regions_map.end() );
         Assert( d_regions_map.find( b )!=d_regions_map.end() );
-        int ai = d_regions_map[a];
-        int bi = d_regions_map[b];
         Debug("uf-ss") << "   regions: " << ai << " " << bi << std::endl;
         if( ai==bi ){
           //internal disequality
@@ -663,11 +663,15 @@ void StrongSolverTheoryUF::SortModel::check( Theory::Effort level, OutputChannel
                   return;
                 }
               }else{
-                if( addSplit( d_regions[i], out ) ){
+                int sp = addSplit( d_regions[i], out );
+                if( sp==1 ){
                   addedLemma = true;
 #ifdef ONE_SPLIT_REGION
                   break;
 #endif
+                }else if( sp==-1 ){
+                  check( level, out );
+                  return;
                 }
               }
             }
@@ -771,6 +775,7 @@ bool StrongSolverTheoryUF::SortModel::minimize( OutputChannel* out, TheoryModel*
       }
 #endif
     }else{
+      Trace("uf-ss-debug")  << "Minimize the UF model..." << std::endl;
       //internal minimize, ensure that model forms a clique:
       // if two equivalence classes are neither equal nor disequal, add a split
       int validRegionIndex = -1;
@@ -778,7 +783,7 @@ bool StrongSolverTheoryUF::SortModel::minimize( OutputChannel* out, TheoryModel*
         if( d_regions[i]->d_valid ){
           if( validRegionIndex!=-1 ){
             combineRegions( validRegionIndex, i );
-            if( addSplit( d_regions[validRegionIndex], out ) ){
+            if( addSplit( d_regions[validRegionIndex], out )!=0 ){
               return false;
             }
           }else{
@@ -786,7 +791,7 @@ bool StrongSolverTheoryUF::SortModel::minimize( OutputChannel* out, TheoryModel*
           }
         }
       }
-      if( addSplit( d_regions[validRegionIndex], out ) ){
+      if( addSplit( d_regions[validRegionIndex], out )!=0 ){
         return false;
       }
     }
@@ -1074,7 +1079,7 @@ void StrongSolverTheoryUF::SortModel::allocateCardinality( OutputChannel* out ){
   }
 }
 
-bool StrongSolverTheoryUF::SortModel::addSplit( Region* r, OutputChannel* out ){
+int StrongSolverTheoryUF::SortModel::addSplit( Region* r, OutputChannel* out ){
   Node s;
   if( r->hasSplits() ){
     if( !options::ufssSmartSplits() ){
@@ -1120,11 +1125,26 @@ bool StrongSolverTheoryUF::SortModel::addSplit( Region* r, OutputChannel* out ){
   if (!s.isNull() ){
     //add lemma to output channel
     Assert( s.getKind()==EQUAL );
-    s = Rewriter::rewrite( s );
     Trace("uf-ss-lemma") << "*** Split on " << s << std::endl;
+    Node ss = Rewriter::rewrite( s );
+    if( ss.getKind()!=EQUAL ){
+      Node b_t = NodeManager::currentNM()->mkConst( true );
+      Node b_f = NodeManager::currentNM()->mkConst( false );
+      if( ss==b_f ){
+        Trace("uf-ss-lemma") << "....Assert disequal directly : " << s[0] << " " << s[1] << std::endl;
+        assertDisequal( s[0], s[1], b_t );
+        return -1;
+      }else{
+        Trace("uf-ss-warn") << "Split on unknown literal : " << ss << std::endl;
+      }
+      if( ss==b_t ){
+        Message() << "Bad split " << s << std::endl;
+        exit( 16 );
+      }
+    }
     if( options::sortInference()) {
       for( int i=0; i<2; i++ ){
-        int si = d_thss->getSortInference()->getSortId( s[i] );
+        int si = d_thss->getSortInference()->getSortId( ss[i] );
         Trace("uf-ss-split-si") << si << " ";
       }
       Trace("uf-ss-split-si")  << std::endl;
@@ -1134,13 +1154,13 @@ bool StrongSolverTheoryUF::SortModel::addSplit( Region* r, OutputChannel* out ){
     //Trace("uf-ss-lemma") << s[0].getType() << " " << s[1].getType() << std::endl;
     //Notice() << "*** Split on " << s << std::endl;
     //split on the equality s
-    out->split( s );
+    out->split( ss );
     //tell the sat solver to explore the equals branch first
-    out->requirePhase( s, true );
+    out->requirePhase( ss, true );
     ++( d_thss->d_statistics.d_split_lemmas );
-    return true;
+    return 1;
   }else{
-    return false;
+    return 0;
   }
 }
 
diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h
index 8e568444b..9111ec6a7 100644
--- a/src/theory/uf/theory_uf_strong_solver.h
+++ b/src/theory/uf/theory_uf_strong_solver.h
@@ -200,8 +200,8 @@ public:
   private:
     /** allocate cardinality */
     void allocateCardinality( OutputChannel* out );
-    /** add split */
-    bool addSplit( Region* r, OutputChannel* out );
+    /** add split 0 = no split, -1 = entailed disequality added, 1 = split added */
+    int addSplit( Region* r, OutputChannel* out );
     /** add clique lemma */
     void addCliqueLemma( std::vector< Node >& clique, OutputChannel* out );
     /** add totality axiom */