Minor bug fix for exhaustive instantiation in model_engine.

diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index c21859e87225ae06c27de6dc2fd379d5775bca09..64ebb6cdaaf90e9a326d62bdf579449f8f2f8c4f 100644 (file)
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -811,9 +811,11 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No
       Trace("fmc-exh-debug") << std::endl;
       int index = riter.increment();
       Trace("fmc-exh-debug") << "Incremented index " << index << std::endl;
-      if (index>=0 && riter.d_index[index]>0 && addedLemmas>0 && riter.d_enum_type[index]==RepSetIterator::ENUM_RANGE) {
-        Trace("fmc-exh-debug") << "Since this is a range enumeration, skip to the next..." << std::endl;
-        riter.increment2( index-1 );
+      if( !riter.isFinished() ){
+        if (index>=0 && riter.d_index[index]>0 && addedLemmas>0 && riter.d_enum_type[index]==RepSetIterator::ENUM_RANGE) {
+          Trace("fmc-exh-debug") << "Since this is a range enumeration, skip to the next..." << std::endl;
+          riter.increment2( index-1 );
+        }
       }
     }
     d_addedLemmas += addedLemmas;