From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Sun, 6 Feb 2022 08:16:48 +0000 (-0800)
Subject: [Seq] Check types for split on indices (#8066)
X-Git-Tag: cvc5-1.0.0~449
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a95f8979d8bd15f11427aaf7f69663959756dd42;p=cvc5.git

[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 98777c4bd..c79664a32 100644
--- 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 13c5e3094..1d231ea88 100644
--- 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
index 000000000..0577479fc
--- /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)