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 28139400b3e2d5c182c747a95f2faadd4a4c106b..06464af609212940b35606d997c851d10c3a267c 100644 (file)
--- 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 4232091220afc4ecf2971129dbeb20341b49ab6d..6e67352b3620728996b29770a5ac897312913a9f 100644 (file)
--- 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 260b0d9b7da499ce42e86a34647ac291f6ee46ba..6cf5c76c19db5ef991bcea4aea38ccd949cb52d0 100644 (file)
--- 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 (file)
index 0000000..afa6fa2
--- /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)