diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 1d8f9f32710..95f24268577 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -1685,7 +1685,7 @@ seq_util::rex::info seq_util::rex::mk_info_rec(app* e) const { return i1.plus(); case OP_RE_COMPLEMENT: i1 = get_info_rec(e->get_arg(0)); - return i1.compl(); + return i1.complement(); case OP_RE_LOOP: i1 = get_info_rec(e->get_arg(0)); lower_bound = e->get_decl()->get_parameter(0).get_int(); @@ -1754,7 +1754,7 @@ seq_util::rex::info seq_util::rex::info::opt() const { return seq_util::rex::info(classical, classical, interpreted, nonbranching, normalized, monadic, false, l_true, 0, star_height); } -seq_util::rex::info seq_util::rex::info::compl() const { +seq_util::rex::info seq_util::rex::info::complement() const { if (is_known()) { lbool compl_nullable = (nullable == l_true ? l_false : (nullable == l_false ? l_true : l_undef)); unsigned compl_min_length = (compl_nullable == l_false ? 1 : 0); diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 7013a37986f..d94b1ec6f28 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -479,7 +479,7 @@ class seq_util { info star() const; info plus() const; info opt() const; - info compl() const; + info complement() const; info concat(info & rhs, bool lhs_is_concat) const; info disj(info& rhs) const; info conj(info& rhs) const;