From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Fri, 11 Feb 2022 00:21:06 +0000 (-0800)
Subject: Fix type check of `seq.nth` (#8093)
X-Git-Tag: cvc5-1.0.0~427
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=50d93bfc5bcd160059522e22310934ea4ecb2c57;p=cvc5.git

Fix type check of `seq.nth` (#8093)

The code for type checking `seq.nth` was trying to retrieve the sequence
element type before ensuring that the type of the first argument was a
sequence, which lead to assertion failures. This commit reorders the
checks to avoid this issue.
---

diff --git a/src/theory/strings/theory_strings_type_rules.cpp b/src/theory/strings/theory_strings_type_rules.cpp
index 183344aa2..c92502c40 100644
--- a/src/theory/strings/theory_strings_type_rules.cpp
+++ b/src/theory/strings/theory_strings_type_rules.cpp
@@ -312,13 +312,14 @@ TypeNode SeqNthTypeRule::computeType(NodeManager* nodeManager,
                                      bool check)
 {
   TypeNode t = n[0].getType(check);
+  if (check && !t.isSequence())
+  {
+    throw TypeCheckingExceptionPrivate(n, "expecting a sequence in nth");
+  }
+
   TypeNode t1 = t.getSequenceElementType();
   if (check)
   {
-    if (!t.isSequence())
-    {
-      throw TypeCheckingExceptionPrivate(n, "expecting a sequence in nth");
-    }
     TypeNode t2 = n[1].getType(check);
     if (!t2.isInteger())
     {
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index bc3880b18..c812d364e 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1145,6 +1145,7 @@ set(regress_0_tests
   regress0/seq/seq-ex5.smt2
   regress0/seq/seq-expand-defs.smt2
   regress0/seq/seq-nemp.smt2
+  regress0/seq/seq-nth-type-check.smt2
   regress0/seq/seq-nth-uf-z.smt2
   regress0/seq/seq-nth-uf.smt2
   regress0/seq/seq-nth-undef-unsat.smt2
diff --git a/test/regress/regress0/seq/seq-nth-type-check.smt2 b/test/regress/regress0/seq/seq-nth-type-check.smt2
new file mode 100644
index 000000000..3e9c38e7b
--- /dev/null
+++ b/test/regress/regress0/seq/seq-nth-type-check.smt2
@@ -0,0 +1,8 @@
+; DISABLE-TESTER: dump
+; EXPECT: expecting a sequence
+; SCRUBBER: grep -o "expecting a sequence"
+; EXIT: 1
+(set-logic QF_SLIA)
+(declare-const i Int)
+(assert (= i (seq.nth 0 i)))
+(check-sat)