From 97ed1cd07d732612f640f29479b0045c2bc53a1f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 31 Jul 2020 11:46:38 -0700 Subject: [PATCH] don't rewrite empty/non-empty checking predicates Signed-off-by: Nikolaj Bjorner --- src/smt/seq_regex.cpp | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index 53a575269..af5617745 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -411,10 +411,8 @@ namespace smt { << "," << expr_id_str(u) << "," << expr_id_str(n) << ") ";); expr_ref is_nullable = is_nullable_wrapper(r); - if (m.is_true(is_nullable)) { - TRACE("seq_regex", tout << "is nullable\n";); + if (m.is_true(is_nullable)) return; - } literal null_lit = th.mk_literal(is_nullable); expr_ref hd = mk_first(r, n); expr_ref d(m); @@ -441,7 +439,6 @@ namespace smt { lits.push_back(th.mk_literal(next_non_empty)); } - TRACE("seq_regex", tout << lits << "\n";); th.add_axiom(lits); }