minor

1 files changed, 6 insertions, 1 deletions

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index d095d6801..e2a057e49 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -84,8 +84,13 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
                                       nm->mkNode(GEQ, lt0, t12),
                                       nm->mkNode(MINUS, lt0, t12),
                                       d_zero));
+    Node b14 = nm->mkNode(STRING_LENGTH, skt)
+                   .eqNode(nm->mkNode(ITE,
+                                      nm->mkNode(GEQ, lt0, t12),
+                                      m,
+                                      nm->mkNode(MINUS, lt0, n)));
 
-    Node b1 = nm->mkNode(AND, b11, b12, b13);
+    Node b1 = nm->mkNode(AND, b11, b12, b13, b14);
     Node b2 = skt.eqNode(d_empty_str);
     Node lemma = nm->mkNode(ITE, cond, b1, b2);