mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +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:30:58 -07:00 • committed by Nikolaj Bjorner
parent 6bca12d399
commit 23ce6917c5
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -2071,8 +2071,8 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
SASSERT(bs.size() > 1);
s1 = s1.extract(s2.length(), s1.length() - s2.length());
as[0] = str().mk_string(s1);
result = str().mk_prefix(str().mk_concat(as.size(), as.data(), sort_a),
str().mk_concat(bs.size()-1, bs.data()+1, sort_a));
auto a = str().mk_concat(as.size(), as.data(), sort_a);
result = str().mk_prefix(a, str().mk_concat(bs.size()-1, bs.data()+1, sort_a));
TRACE(seq, tout << s1 << " " << s2 << " " << result << "\n";);
return BR_REWRITE_FULL;
}