[Seq] Check types for split on indices (#8066)

We applied `STRINGS_ARRAY_EQ_SPLIT` to pairs of `seq.nth` terms of
different types. This lead to assertion (in debug) and performance
problems (in production). The commit adds a type check.

diff --git a/src/theory/strings/array_core_solver.cpp b/src/theory/strings/array_core_solver.cpp
index 98777c4bd5ff0001fd1376b3331fc4c71d5e430d..c79664a3247c2085eb9e4e2994af5b5f3cd47afc 100644 (file)
--- a/src/theory/strings/array_core_solver.cpp
+++ b/src/theory/strings/array_core_solver.cpp
@@ -85,10 +85,16 @@ void ArrayCoreSolver::checkNth(const std::vector<Node>& nthTerms)
   {
     for (size_t j = i + 1; j < nthTerms.size(); j++)
     {
-      Node x = nthTerms[i][0];
-      Node y = nthTerms[j][0];
-      Node n = nthTerms[i][1];
-      Node m = nthTerms[j][1];
+      TNode x = nthTerms[i][0];
+      TNode y = nthTerms[j][0];
+
+      if (x.getType() != y.getType())
+      {
+        continue;
+      }
+
+      TNode n = nthTerms[i][1];
+      TNode m = nthTerms[j][1];
       if (d_state.areEqual(n, m) && !d_state.areEqual(x, y)
           && !d_state.areDisequal(x, y))
       {

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 13c5e3094aff5a839c6981e380f9b93b0d614e02..1d231ea884ce2960b2973725e275bb39065166ee 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1117,6 +1117,7 @@ set(regress_0_tests
   regress0/seq/issue5665-invalid-model.smt2
   regress0/seq/issue6337-seq.smt2
   regress0/seq/len_simplify.smt2
+  regress0/seq/mixed-types-seq-nth.smt2
   regress0/seq/nth-oob.smt2
   regress0/seq/nth-unit.smt2
   regress0/seq/nth-update.smt2

diff --git a/test/regress/regress0/seq/mixed-types-seq-nth.smt2 b/test/regress/regress0/seq/mixed-types-seq-nth.smt2
new file mode 100644 (file)
index 0000000..0577479
--- /dev/null
+++ b/test/regress/regress0/seq/mixed-types-seq-nth.smt2
@@ -0,0 +1,16 @@
+; COMMAND-LINE: --seq-array=lazy -q
+
+(set-logic QF_UFSLIA)
+(declare-sort E 0)
+(declare-const s1 (Seq Int))
+(declare-const s2 (Seq Int))
+(declare-const s3 (Seq E))
+(declare-const s4 (Seq E))
+
+(declare-const i Int)
+
+(assert (distinct (seq.nth s1 i) (seq.nth s2 i)))
+(assert (distinct (seq.nth s3 i) (seq.nth s4 i)))
+
+(set-info :status sat)
+(check-sat)