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

parameter eval order

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-10-07 10:21:09 -07:00 • committed by Nikolaj Bjorner
parent 52e55854a4
commit 5ae7bb078a
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1910,7 +1910,8 @@ br_status seq_rewriter::mk_seq_mapi(expr* f, expr* i, expr* seqA, expr_ref& resu
}
if (str().is_concat(seqA, s1, s2)) {
expr_ref j(m_autil.mk_add(i, str().mk_length(s1)), m());
result = str().mk_concat(str().mk_mapi(f, i, s1), str().mk_mapi(f, j, s2));
auto a = str().mk_mapi(f, i, s1);
result = str().mk_concat(a, str().mk_mapi(f, j, s2));
return BR_REWRITE2;
}
return BR_FAILED;