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 152a3e1802612e1302fe6ad06d5819dad2368e36..b0d53806480845d9d6c512f12f4da35728d686ff 100644 (file)
--- 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 20784051650b666cab5621731ceae7333cbfa656..d112bdf1d79edb5dec76e6f884ec0c845a625ba1 100644 (file)
--- 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 (file)
index 0000000..88a89b7
--- /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)