mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

fix #6477

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-12-04 13:02:45 -08:00
parent ead2a46a88
commit 87095950cb
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1988,6 +1988,10 @@ bool bv_rewriter::distribute_concat(decl_kind k, unsigned n, expr* const* args,
expr* e = to_app(arg)->get_arg(0); expr* e = to_app(arg)->get_arg(0);
unsigned sz1 = get_bv_size(e); unsigned sz1 = get_bv_size(e);
unsigned sz2 = get_bv_size(arg); unsigned sz2 = get_bv_size(arg);
if (sz1 == sz2) {
result = m.mk_app(get_fid(), k, n, args);
return true;
}
expr_ref_vector args1(m), args2(m); expr_ref_vector args1(m), args2(m);
for (unsigned j = 0; j < n; ++j) { for (unsigned j = 0; j < n; ++j) {
args1.push_back(m_mk_extract(sz2 - 1, sz2 - sz1, args[j])); args1.push_back(m_mk_extract(sz2 - 1, sz2 - sz1, args[j]));