simplify string patterns into prefix/suffix constraints

Signed-off-by: Nikolaj Bjorner <[email protected]>

src/ast/rewriter/seq_rewriter.cpp

@@ -4541,6 +4541,15 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
        result = m_br.mk_eq_rw(a, b_s);
        return BR_REWRITE_FULL;
     }
+    expr* c = nullptr, *d = nullptr, *e = nullptr;
+    if (re().is_concat(b, c, d) && re().is_to_re(c, e) && re().is_full_seq(d)) {
+        result = str().mk_prefix(e, a);
+        return BR_REWRITE1;
+    }
+    if (re().is_concat(b, c, d) && re().is_to_re(d, e) && re().is_full_seq(c)) {
+        result = str().mk_suffix(e, a);
+        return BR_REWRITE1;
+    }
     expr* b1 = nullptr;
     expr* eps = nullptr;
     if (re().is_opt(b, b1) ||