From 88ef8c7cda767a1373b7b9a73cd617173cce1cbe Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Fri, 20 Mar 2026 14:07:12 +0100 Subject: [PATCH] Another regex witness bug --- src/ast/rewriter/seq_rewriter.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index a1e1596a5..e0b86d50c 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -6106,7 +6106,9 @@ lbool seq_rewriter::some_string_in_re(expr_mark& visited, expr* r, unsigned_vect if (!re().is_empty(el)) { if (has_bounds) exclude.push_back({ low, high }); - todo.push_back({ expr_ref(el, m()), str.size(), std::move(exclude), false }); + todo.push_back({ expr_ref(el, m()), str.size(), exclude, false }); + if (has_bounds) + exclude.pop_back(); } if (has_bounds) { // I want this case to be processed first => push it last