8 files changed, 50 insertions, 2 deletions
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index b0f6e63bf..5ecc33778 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -716,7 +716,22 @@ bool BoundedIntegers::getRsiSubsitution( Node q, Node v, std::vector< Node >& va
     Trace("bound-int-rsi") << "Look up the value for " << d_set[q][i] << " " << i << std::endl;
     int vo = rsi->getVariableOrder(i);
     Assert(q[0][vo] == d_set[q][i]);
-    Node t = rsi->getCurrentTerm(vo, true);
+    TypeNode tn = d_set[q][i].getType();
+    // If the type of tn is not closed enumerable, we must map the value back
+    // to a term that appears in the same equivalence class as the constant.
+    // Notice that this is to ensure that unhandled values (e.g. uninterpreted
+    // constants, datatype values) do not enter instantiations/lemmas, which
+    // can lead to refutation unsoundness. However, it is important that we
+    // conversely do *not* map terms to values in other cases. In particular,
+    // replacing a constant c with a term t can lead to solution unsoundness
+    // if we are instantiating a quantified formula that corresponds to a
+    // reduction for t, since then the reduction is using circular reasoning:
+    // the current value of t is being used to reason about the range of
+    // its axiomatization. This is limited to reductions in the theory of
+    // strings, which use quantification on integers only. Note this
+    // impacts only quantified formulas with 2+ dimensions and dependencies
+    // between dimensions, e.g. str.indexof_re reduction.
+    Node t = rsi->getCurrentTerm(vo, !tn.isClosedEnumerable());
     Trace("bound-int-rsi") << "term : " << t << std::endl;
     vars.push_back( d_set[q][i] );
     subs.push_back( t );
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index d0eee1886..f6af5b680 100644
--- a/src/theory/rep_set.cpp
+++ b/src/theory/rep_set.cpp
@@ -429,14 +429,17 @@ Node RepSetIterator::getCurrentTerm(unsigned i, bool valTerm) const
                      << d_domain_elements[i].size() << std::endl;
   Assert(0 <= curr && curr < d_domain_elements[i].size());
   Node t = d_domain_elements[i][curr];
+  Trace("rsi-debug") << "rsi : term = " << t << std::endl;
   if (valTerm)
   {
     Node tt = d_rs->getTermForRepresentative(t);
     if (!tt.isNull())
     {
+  Trace("rsi-debug") << "rsi : return rep term = " << tt << std::endl;
       return tt;
     }
   }
+  Trace("rsi-debug") << "rsi : return" << std::endl;
   return t;
 }
 
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index b0d538064..dbb6d4cf3 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -323,7 +323,7 @@ Node StringsPreprocess::reduce(Node t,
     //         n <= i < ite(skk = -1, len(s), skk) ^ 0 < l <= len(s) - i =>
     //           ~in_re(substr(s, i, l), r)) ^
     //       (skk != -1 =>
-    //          exists l. 0 <= l < len(s) - skk ^ in_re(substr(s, skk, l), r))
+    //          exists l. 0 <= l <= len(s) - skk ^ in_re(substr(s, skk, l), r))
     //
     // Note that this reduction relies on eager reduction lemmas being sent to
     // properly limit the range of skk.
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index a5a687f9f..4ee8e513e 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2126,7 +2126,11 @@ set(regress_1_tests
   regress1/strings/issue6337-replace-re.smt2
   regress1/strings/issue6567-empty-re-range.smt2
   regress1/strings/issue6604-2.smt2
+  regress1/strings/issue6635-rre.smt2
   regress1/strings/issue6653-2-update-c-len.smt2
+  regress1/strings/issue6653-4-rre.smt2
+  regress1/strings/issue6653-rre.smt2
+  regress1/strings/issue6653-rre-small.smt2
   regress1/strings/kaluza-fl.smt2
   regress1/strings/loop002.smt2
   regress1/strings/loop003.smt2
diff --git a/test/regress/regress1/strings/issue6635-rre.smt2 b/test/regress/regress1/strings/issue6635-rre.smt2
new file mode 100644
index 000000000..cbca77783
--- /dev/null
+++ b/test/regress/regress1/strings/issue6635-rre.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --strings-exp --re-elim --re-elim-agg
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun a () String)
+(assert (str.in_re (str.replace_re a (re.++ (str.to_re "A") (re.union (str.to_re "") (str.to_re (str.from_code (str.len a))))) "AB") (re.+ (str.to_re "A"))))
+(check-sat)
diff --git a/test/regress/regress1/strings/issue6653-4-rre.smt2 b/test/regress/regress1/strings/issue6653-4-rre.smt2
new file mode 100644
index 000000000..8de99a334
--- /dev/null
+++ b/test/regress/regress1/strings/issue6653-4-rre.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --strings-exp --re-elim --re-elim-agg
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun x () String)
+(assert (str.in_re (str.replace_re x (str.to_re "A") x) (re.++ (re.comp (str.to_re "A")) (str.to_re "A") re.allchar)))
+(check-sat)
diff --git a/test/regress/regress1/strings/issue6653-rre-small.smt2 b/test/regress/regress1/strings/issue6653-rre-small.smt2
new file mode 100644
index 000000000..c4b6a497b
--- /dev/null
+++ b/test/regress/regress1/strings/issue6653-rre-small.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --strings-exp --strings-fmf --re-elim --re-elim-agg
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun a () String)
+(assert (str.in_re a (re.+ (str.to_re (str.replace_re a (str.to_re a) "A")))))
+(check-sat)
diff --git a/test/regress/regress1/strings/issue6653-rre.smt2 b/test/regress/regress1/strings/issue6653-rre.smt2
new file mode 100644
index 000000000..66b7dd64e
--- /dev/null
+++ b/test/regress/regress1/strings/issue6653-rre.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --strings-exp --re-elim --re-elim-agg
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun a () String)
+(declare-fun b () String)
+(assert (str.in_re (str.replace_re b (str.to_re (str.replace_all a (str.++ b "a") b)) (str.++ b "a")) (re.+ (str.to_re "b"))))
+(assert (str.in_re a (re.* (re.range "a" "b"))))
+(check-sat)