mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

track origin slice for concat nodes

Browse source
This commit is contained in:
Jakob Rath 2023-07-19 12:06:02 +02:00
parent af73f26941
commit 85d80a0ae1
1 changed files with 1 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/math/polysat/slicing.cpp
View file

@ -244,6 +244,7 @@ namespace polysat {
args.push_back(n->get_expr());
app* a = m_ast.mk_app(mk_concat_decl(args), args);
enode* concat = find_or_alloc_enode(a, base.size(), base.data(), width(sv), null_var);
info(concat).slice = sv;
base.clear();
m_egraph.merge(sv, concat, encode_dep(dep_t()));
}