Fix rep set increment for empty domains (#3682)

diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index d293890bf52d580357eceb2033fef4708778817f..55cef5ea715aaa3c7adfc5156d6de97746af1045 100644 (file)
--- a/src/theory/rep_set.cpp
+++ b/src/theory/rep_set.cpp
@@ -371,8 +371,8 @@ int RepSetIterator::incrementAtIndex(int i)
 }
 
 int RepSetIterator::do_reset_increment( int i, bool initial ) {
-  bool emptyDomain = false;
   for( unsigned ii=(i+1); ii<d_index.size(); ii++ ){
+    bool emptyDomain = false;
     int ri_res = resetIndex( ii, initial );
     if( ri_res==-1 ){
       //failed
@@ -383,16 +383,13 @@ int RepSetIterator::do_reset_increment( int i, bool initial ) {
       emptyDomain = true;
     }
     //force next iteration if currently an empty domain
-    if( emptyDomain ){
-      d_index[ii] = domainSize(ii)-1;
+    if (emptyDomain)
+    {
+      Trace("rsi-debug") << "This is an empty domain, increment." << std::endl;
+      return increment();
     }
   }
-  if( emptyDomain ){
-    Trace("rsi-debug") << "This is an empty domain, increment." << std::endl;
-    return increment();
-  }else{
-    return i;
-  }
+  return i;
 }
 
 int RepSetIterator::increment(){

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 179c5fe4c43164b5d40caae7f2c938b96405c8f5..d5414364af6c7993192b82babe0b06ede2d77868 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1229,6 +1229,7 @@ set(regress_1_tests
   regress1/fmf/german73.smt2
   regress1/fmf/issue2034-preinit.smt2
   regress1/fmf/issue3587.smt2
+  regress1/fmf/issue3615.smt2
   regress1/fmf/issue3626.smt2
   regress1/fmf/issue916-fmf-or.smt2
   regress1/fmf/jasmin-cdt-crash.smt2

diff --git a/test/regress/regress1/fmf/issue3615.smt2 b/test/regress/regress1/fmf/issue3615.smt2
new file mode 100644 (file)
index 0000000..48ad7c7
--- /dev/null
+++ b/test/regress/regress1/fmf/issue3615.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --fmf-bound
+; EXPECT: sat
+(set-logic UFLIA)
+(declare-fun f (Int) Bool)
+(assert (forall ((x Int) (y Int)) (or (>= x 0) (<= x 0) (< y 0) (> y x) (f x))))
+(check-sat)