From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 8 Jun 2021 06:11:28 +0000 (-0500)
Subject: Fix str.update reduction (#6696)
X-Git-Tag: cvc5-1.0.0~1633
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2cddf7e216d3d2015a42246ef7a76b75ccaf6462;p=cvc5.git

Fix str.update reduction (#6696)

Fixes the 2nd benchmark from #6653.
---

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 152a3e180..b0d538064 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -163,8 +163,9 @@ Node StringsPreprocess::reduce(Node t,
     Node a2 = s.eqNode(nm->mkNode(STRING_CONCAT, sk1, sk3, sk2));
     // length of first skolem is second argument
     Node a3 = nm->mkNode(STRING_LENGTH, sk1).eqNode(n);
+    Node a4 = nm->mkNode(STRING_LENGTH, rs).eqNode(nm->mkNode(STRING_LENGTH, sk3));
 
-    Node b1 = nm->mkNode(AND, a1, a2, a3);
+    Node b1 = nm->mkNode(AND, {a1, a2, a3, a4});
     Node b2 = skt.eqNode(s);
     Node lemma = nm->mkNode(ITE, cond, b1, b2);
 
@@ -172,7 +173,8 @@ Node StringsPreprocess::reduce(Node t,
     // IF    n >=0 AND n < len( s )
     // THEN: skt = sk1 ++ substr(r,0,len(s)-n) ++ sk2 AND
     //       s = sk1 ++ sk3 ++ sk2 AND
-    //       len( sk1 ) = n
+    //       len( sk1 ) = n AND
+    //       len( substr(r,0,len(s)-n) ) = len( sk3 )
     // ELSE: skt = s
     // We use an optimization where r is used instead of substr(r,0,len(s)-n)
     // if r is a constant of length one.
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 207840516..d112bdf1d 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2125,6 +2125,7 @@ set(regress_1_tests
   regress1/strings/issue6337-replace-re.smt2
   regress1/strings/issue6567-empty-re-range.smt2
   regress1/strings/issue6604-2.smt2
+  regress1/strings/issue6653-2-update-c-len.smt2
   regress1/strings/kaluza-fl.smt2
   regress1/strings/loop002.smt2
   regress1/strings/loop003.smt2
diff --git a/test/regress/regress1/strings/issue6653-2-update-c-len.smt2 b/test/regress/regress1/strings/issue6653-2-update-c-len.smt2
new file mode 100644
index 000000000..88a89b725
--- /dev/null
+++ b/test/regress/regress1/strings/issue6653-2-update-c-len.smt2
@@ -0,0 +1,7 @@
+(set-logic ALL)
+(set-info :status sat)
+(set-option :strings-lazy-pp false)
+(set-option :check-unsat-cores true)
+(declare-fun s () String)
+(assert (not (= "A" (str.substr (str.update "AAAAAA" 1 s) 5 1))))
+(check-sat)