From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 30 Jan 2020 22:30:47 +0000 (-0600)
Subject: Fix rep set increment for empty domains (#3682)
X-Git-Tag: cvc5-1.0.0~3704
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a456ef81b15e2f8612cd41a31ad811af35f47846;p=cvc5.git

Fix rep set increment for empty domains (#3682)
---

diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index d293890bf..55cef5ea7 100644
--- 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 179c5fe4c..d5414364a 100644
--- 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
index 000000000..48ad7c7df
--- /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)