diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-07-26 00:50:21 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-07-26 00:50:31 +0200 |
commit | c4d8629dc65d283a2fe03f6ad46ff3a65b9b62e4 (patch) | |
tree | e653fd3aaa3816c02347565ef394b9dfdce0b090 /src/theory/quantifiers/full_model_check.cpp | |
parent | fc76056f4ac7f049fc62d3c1de91e44fb58ab2e1 (diff) |
Minor bug fix for exhaustive instantiation in model_engine.
Diffstat (limited to 'src/theory/quantifiers/full_model_check.cpp')
-rw-r--r-- | src/theory/quantifiers/full_model_check.cpp | 8 |
1 files 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; |