From 32eedde897bd2a0c850dfc95b8ef5bf894d47225 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 15 Mar 2026 21:36:22 -0700
Subject: [PATCH] disable rewrite that makes nseq solving harder

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/seq_rewriter.cpp | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index f3aed58ec..43a5c5b5a 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -4371,6 +4371,9 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
             return BR_REWRITE_FULL;
     }
 
+    return BR_FAILED;
+    // disabled
+
     expr_ref hd(m()), tl(m());
     if (get_head_tail(a, hd, tl)) {
         //result = re().mk_in_re(tl, re().mk_derivative(hd, b));