From 1cec37904f1d770d7756d5661ff9b86fbca6d7ac Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 3 Feb 2020 09:31:36 -0600
Subject: [PATCH] Fix corner case of empty domains in bounded fmf (#3690)

---
 src/theory/rep_set.cpp                   | 20 ++++++++++++++++++--
 test/regress/CMakeLists.txt              |  1 +
 test/regress/regress1/fmf/issue3689.smt2 | 10 ++++++++++
 3 files changed, 29 insertions(+), 2 deletions(-)
 create mode 100644 test/regress/regress1/fmf/issue3689.smt2

diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index 55cef5ea7..243846b33 100644
--- 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 012fde3b8..3bcdec380 100644
--- 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
index 000000000..83b64ba29
--- /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)
-- 
2.30.2