From d26ef08c699ad91bdf98c6be084170bd50cdb2a9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 18 May 2020 19:41:37 -0700 Subject: [PATCH] na Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index be7101cff..89844c426 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -2001,15 +2001,13 @@ expr_ref seq_rewriter::is_nullable(expr* r) { SASSERT(m_util.is_re(r)); expr* r1 = nullptr, *r2 = nullptr; unsigned lo = 0, hi = 0; - if (m_util.re.is_concat(r, r1, r2)) { + if (m_util.re.is_concat(r, r1, r2) || + m_util.re.is_intersection(r, r1, r2)) { return expr_ref(mk_and(m(), is_nullable(r1), is_nullable(r2)), m()); } if (m_util.re.is_union(r, r1, r2)) { return expr_ref(mk_or(m(), is_nullable(r1), is_nullable(r2)), m()); } - if (m_util.re.is_intersection(r, r1, r2)) { - return expr_ref(mk_and(m(), is_nullable(r1), is_nullable(r2)), m()); - } if (m_util.re.is_star(r) || m_util.re.is_opt(r) || m_util.re.is_full_seq(r)) {