Fix corner case of empty domains in bounded fmf (#3690)

diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index 55cef5ea715aaa3c7adfc5156d6de97746af1045..243846b339695100f30faae7d46a980e577daab5 100644 (file)
--- a/src/theory/rep_set.cpp
+++ b/src/theory/rep_set.cpp
@@ -350,6 +350,7 @@ int RepSetIterator::incrementAtIndex(int i)
 #ifdef DISABLE_EVAL_SKIP_MULTIPLE
   i = (int)d_index.size()-1;
 #endif
+  Trace("rsi-debug") << "RepSetIterator::incrementAtIndex: " << i << std::endl;
   //increment d_index
   if( i>=0){
     Trace("rsi-debug") << "domain size of " << i << " is " << domainSize(i) << std::endl;
@@ -361,6 +362,7 @@ int RepSetIterator::incrementAtIndex(int i)
     }
   }
   if( i==-1 ){
+    Trace("rsi-debug") << "increment failed" << std::endl;
     d_index.clear();
     return -1;
   }else{
@@ -371,6 +373,8 @@ int RepSetIterator::incrementAtIndex(int i)
 }
 
 int RepSetIterator::do_reset_increment( int i, bool initial ) {
+  Trace("rsi-debug") << "RepSetIterator::do_reset_increment: " << i
+                     << ", initial=" << initial << std::endl;
   for( unsigned ii=(i+1); ii<d_index.size(); ii++ ){
     bool emptyDomain = false;
     int ri_res = resetIndex( ii, initial );
@@ -385,10 +389,22 @@ int RepSetIterator::do_reset_increment( int i, bool initial ) {
     //force next iteration if currently an empty domain
     if (emptyDomain)
     {
-      Trace("rsi-debug") << "This is an empty domain, increment." << std::endl;
-      return increment();
+      Trace("rsi-debug") << "This is an empty domain (index " << ii << ")."
+                         << std::endl;
+      if (ii > 0)
+      {
+        // increment at the previous index
+        return incrementAtIndex(ii - 1);
+      }
+      else
+      {
+        // this is the first index, we are done
+        d_index.clear();
+        return -1;
+      }
     }
   }
+  Trace("rsi-debug") << "Finished, return " << i << std::endl;
   return i;
 }
 

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 012fde3b88f7630eab1e2bb1ea4b74d3f3972fe7..3bcdec380498ef72583b88d91b4f3b0060d761ce 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1232,6 +1232,7 @@ set(regress_1_tests
   regress1/fmf/issue3587.smt2
   regress1/fmf/issue3615.smt2
   regress1/fmf/issue3626.smt2
+  regress1/fmf/issue3689.smt2
   regress1/fmf/issue916-fmf-or.smt2
   regress1/fmf/jasmin-cdt-crash.smt2
   regress1/fmf/ko-bound-set.cvc

diff --git a/test/regress/regress1/fmf/issue3689.smt2 b/test/regress/regress1/fmf/issue3689.smt2
new file mode 100644 (file)
index 0000000..83b64ba
--- /dev/null
+++ b/test/regress/regress1/fmf/issue3689.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --fmf-bound
+; EXPECT: sat
+(set-logic ALL)
+(declare-sort S 0)
+(declare-fun c () S)
+(declare-fun b () S)
+(declare-fun d (S Int) Bool)
+(assert (distinct b c))
+(assert (forall ((e S) (f Int)) (=> (and (> f 1) (< f 0)) (d e f))))
+(check-sat)