From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Fri, 25 Jul 2014 22:50:21 +0000 (+0200)
Subject: Minor bug fix for exhaustive instantiation in model_engine.
X-Git-Tag: cvc5-1.0.0~6684
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c4d8629dc65d283a2fe03f6ad46ff3a65b9b62e4;p=cvc5.git

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 c21859e87..64ebb6cda 100644
--- 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;