mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 03:33:35 +00:00
Code Activity

fix type error when mapping over the empty sequence

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-09-10 16:03:52 -07:00
parent 8311525472
commit 6df711254b
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/ast/rewriter/seq_rewriter.cpp
View file

@ -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;