diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index c28a14c3b..641dba59c 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -9838,7 +9838,7 @@ def Full(s): re.all >>> e1 = Full(ReSort(StringSort())) >>> print(e1) - re.allchar + re.all """ if isinstance(s, ReSortRef): return ReRef(Z3_mk_re_full(s.ctx_ref(), s.ast), s.ctx) diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index daf39b79e..2790c5c48 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -545,7 +545,7 @@ void seq_decl_plugin::init() { m_sigs[OP_RE_COMPLEMENT] = alloc(psig, m, "re.complement", 1, 1, &reA, reA); m_sigs[OP_RE_EMPTY_SET] = alloc(psig, m, "re.empty", 1, 0, 0, reA); m_sigs[OP_RE_FULL_SEQ_SET] = alloc(psig, m, "re.all", 1, 0, 0, reA); - m_sigs[OP_RE_FULL_CHAR_SET] = alloc(psig, m, "re.all1", 1, 0, 0, reA); + m_sigs[OP_RE_FULL_CHAR_SET] = alloc(psig, m, "re.allchar", 1, 0, 0, reA); m_sigs[OP_RE_OF_PRED] = alloc(psig, m, "re.of.pred", 1, 1, &predA, reA); m_sigs[OP_SEQ_TO_RE] = alloc(psig, m, "seq.to.re", 1, 1, &seqA, reA); m_sigs[OP_SEQ_IN_RE] = alloc(psig, m, "seq.in.re", 1, 2, seqAreA, boolT);