From ed258ca01902fb9ca48e9464cf32fbd56c1a7a76 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 18 Aug 2020 22:04:09 -0700 Subject: [PATCH] approximate min-length for complements Signed-off-by: Nikolaj Bjorner --- src/ast/seq_decl_plugin.cpp | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 249923c4a..695a534d3 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -1668,8 +1668,7 @@ seq_util::re::info seq_util::re::mk_info_rec(app* e) const { case OP_RE_PLUS: return get_info_rec(e->get_arg(0)); case OP_RE_COMPLEMENT: - i1 = get_info_rec(e->get_arg(0)); - return info(i1.min_length > 0 ? 0 : UINT_MAX); + return info(0); case OP_RE_LOOP: i1 = get_info_rec(e->get_arg(0)); return info(u.max_mul(i1.min_length, e->get_decl()->get_parameter(0).get_int())); @@ -1687,4 +1686,4 @@ seq_util::re::info seq_util::re::mk_info_rec(app* e) const { return info(std::min(i1.min_length, i2.min_length)); } return invalid_info; -} \ No newline at end of file +}