From c4d8629dc65d283a2fe03f6ad46ff3a65b9b62e4 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Sat, 26 Jul 2014 00:50:21 +0200 Subject: [PATCH] Minor bug fix for exhaustive instantiation in model_engine. --- src/theory/quantifiers/full_model_check.cpp | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) 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; -- 2.30.2