From 6df711254b39190fdb726058626b32026b338d67 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 10 Sep 2022 16:03:52 -0700 Subject: [PATCH] fix type error when mapping over the empty sequence --- src/ast/rewriter/seq_rewriter.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 4f70b7933..eed36af81 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -2068,7 +2068,7 @@ br_status seq_rewriter::mk_seq_replace_all(expr* a, expr* b, expr* c, expr_ref& */ br_status seq_rewriter::mk_seq_map(expr* f, expr* seqA, expr_ref& result) { if (str().is_empty(seqA)) { - result = str().mk_empty(get_array_range(f->get_sort())); + result = str().mk_empty(str().mk_seq(get_array_range(f->get_sort()))); return BR_DONE; } expr* a, *s1, *s2; @@ -2087,7 +2087,7 @@ br_status seq_rewriter::mk_seq_map(expr* f, expr* seqA, expr_ref& result) { br_status seq_rewriter::mk_seq_mapi(expr* f, expr* i, expr* seqA, expr_ref& result) { if (str().is_empty(seqA)) { - result = str().mk_empty(get_array_range(f->get_sort())); + result = str().mk_empty(str().mk_seq(get_array_range(f->get_sort()))); return BR_DONE; } expr* a, *s1, *s2;