diff --git a/src/ast/rewriter/seq_range_collapse.cpp b/src/ast/rewriter/seq_range_collapse.cpp index 0c739e0c07..988603af9e 100644 --- a/src/ast/rewriter/seq_range_collapse.cpp +++ b/src/ast/rewriter/seq_range_collapse.cpp @@ -130,8 +130,8 @@ namespace seq { // range bounds. This matches the shape used elsewhere in // seq_rewriter and avoids creating duplicate AST nodes with // different ids for semantically identical ranges. - expr_ref slo(u.str.mk_unit(u.str.mk_char(lo)), m); - expr_ref shi(u.str.mk_unit(u.str.mk_char(hi)), m); + expr_ref slo(u.str.mk_string(zstring(lo)), m); + expr_ref shi(u.str.mk_string(zstring(hi)), m); return expr_ref(u.re.mk_range(slo, shi), m); } diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 29949a151b..3cb049b457 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -422,7 +422,7 @@ func_decl* seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p case OP_STRING_LE: case OP_STRING_IS_DIGIT: case OP_STRING_TO_CODE: - case OP_STRING_FROM_CODE: + case OP_STRING_FROM_CODE: match(*m_sigs[k], arity, domain, range, rng); return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k));