From fb0eb029a85f3c94f9949d14a079885d4a54234a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 21 Jan 2025 09:13:38 -0800 Subject: [PATCH] use lifted bool --- src/ast/rewriter/seq_rewriter.cpp | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 4c4cc900f..e284c012c 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -4559,11 +4559,17 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) { expr_ref new_r = mk_derivative(m_util.mk_char(ch), r); r = new_r; } - if (re().get_info(r).nullable) + + switch (re().get_info(r).nullable) { + case l_true: result = m().mk_true(); - else + return BR_DONE; + case l_false: result = m().mk_false(); - return BR_DONE; + return BR_DONE; + default: + break; + } } expr_ref b_s(m());