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 183344aa289ea9e46d25756e098f14dbccce42a3..c92502c4052b20ab4809d5f019acab23323b995b 100644 (file)
--- 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 bc3880b189060a1430bd1f64db3bcf2404166aff..c812d364e5f0a0b7751d6e3541f3ca38cddd529b 100644 (file)
--- 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 (file)
index 0000000..3e9c38e
--- /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)