From 6e558806017750c77b5ba589755b754489c8c4da Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 18 May 2020 19:38:21 -0700 Subject: [PATCH] constant folding Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index add6b6afd..29840c850 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -1984,7 +1984,11 @@ bool seq_rewriter::get_head_tail(expr* s, expr_ref& head, expr_ref& tail) { } expr_ref seq_rewriter::kleene_and(expr* cond, expr* r) { + if (m().is_true(cond)) + return expr_ref(r, m()); expr* re_empty = m_util.re.mk_empty(m().get_sort(r)); + if (m().is_false(cond)) + return expr_ref(re_empty, m()); return expr_ref(m().mk_ite(cond, r, re_empty), m()); }