From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 2 Jul 2021 13:55:19 +0000 (-0500)
Subject: Fix rewriter for negative constant seq.nth (#6827)
X-Git-Tag: cvc5-1.0.0~1533
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f83a753ad62a005085c47a7c0f4ba2e406d9acd7;p=cvc5.git

Fix rewriter for negative constant seq.nth (#6827)

Fixes #6777.
---

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 28139400b..06464af60 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -273,11 +273,11 @@ void Smt2Printer::toStream(std::ostream& out,
       }
       if (snvec.size() > 1)
       {
-        out << "(seq.++ ";
+        out << "(seq.++";
       }
       for (const Node& snvc : snvec)
       {
-        out << "(seq.unit " << snvc << ")";
+        out << " (seq.unit " << snvc << ")";
       }
       if (snvec.size() > 1)
       {
diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index 423209122..6e67352b3 100644
--- a/src/theory/strings/sequences_rewriter.cpp
+++ b/src/theory/strings/sequences_rewriter.cpp
@@ -1589,14 +1589,17 @@ Node SequencesRewriter::rewriteSeqNth(Node node)
   if (s.isConst() && i.isConst())
   {
     size_t len = Word::getLength(s);
-    size_t pos = i.getConst<Rational>().getNumerator().toUnsignedInt();
-    if (pos < len)
+    if (i.getConst<Rational>().sgn() != -1)
     {
-      std::vector<Node> elements = s.getConst<Sequence>().getVec();
-      const Node& ret = elements[pos];
-      return returnRewrite(node, ret, Rewrite::SEQ_NTH_EVAL);
+      size_t pos = i.getConst<Rational>().getNumerator().toUnsignedInt();
+      if (pos < len)
+      {
+        std::vector<Node> elements = s.getConst<Sequence>().getVec();
+        const Node& ret = elements[pos];
+        return returnRewrite(node, ret, Rewrite::SEQ_NTH_EVAL);
+      }
     }
-    else if (node.getKind() == SEQ_NTH_TOTAL)
+    if (node.getKind() == SEQ_NTH_TOTAL)
     {
       // return arbitrary term
       Node ret = s.getType().getSequenceElementType().mkGroundValue();
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 260b0d9b7..6cf5c76c1 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2150,6 +2150,7 @@ set(regress_1_tests
   regress1/strings/issue6653-4-rre.smt2
   regress1/strings/issue6653-rre.smt2
   regress1/strings/issue6653-rre-small.smt2
+  regress1/strings/issue6777-seq-nth-eval-cm.smt2
   regress1/strings/kaluza-fl.smt2
   regress1/strings/loop002.smt2
   regress1/strings/loop003.smt2
diff --git a/test/regress/regress1/strings/issue6777-seq-nth-eval-cm.smt2 b/test/regress/regress1/strings/issue6777-seq-nth-eval-cm.smt2
new file mode 100644
index 000000000..afa6fa238
--- /dev/null
+++ b/test/regress/regress1/strings/issue6777-seq-nth-eval-cm.smt2
@@ -0,0 +1,12 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(set-option :strings-lazy-pp false)
+(set-option :check-unsat-cores true)
+(declare-fun b () (Seq Int))
+(declare-fun y () Int)
+(declare-fun l () Bool)
+(assert (distinct (seq.nth b y) (seq.nth b 1)))
+(assert (= l (> y 2)))
+(check-sat)