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

fix unsound slice criteria (#6625)

Browse source 
* rename for readability

* bug fix #6617. Don't slice op args that are values
This commit is contained in:
Hari Govind V K 2023-03-06 22:28:22 -05:00 • committed by GitHub
parent 42076a3c13
commit f7c9c9ef72
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 6 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/muz/transforms/dl_mk_slice.cpp
View file

@ -467,15 +467,15 @@ namespace datalog {
void mk_slice::solve_vars(rule& r, uint_set& used_vars, uint_set& parameter_vars) {
expr_ref_vector conjs = get_tail_conjs(r);
for (expr * e : conjs) {
expr_ref r(m);
expr_ref rhs(m);
unsigned v = 0;
if (is_eq(e, v, r) && is_output(v) && m_var_is_sliceable[v]) {
if (is_eq(e, v, rhs) && is_output(v) && m_var_is_sliceable[v]) {
TRACE("dl", tout << "is_eq: " << mk_pp(e, m) << " " << (m_solved_vars[v].get()?"solved":"new") << "\n";);
add_var(v);
if (!m_solved_vars[v].get()) {
TRACE("dl", tout << v << " is solved\n";);
add_free_vars(parameter_vars, r);
m_solved_vars[v] = r;
add_free_vars(parameter_vars, rhs);
m_solved_vars[v] = rhs;
}
else {
TRACE("dl", tout << v << " is used\n";);
@ -666,10 +666,8 @@ namespace datalog {
}
else {
SASSERT(m.is_value(arg));
if (!is_output) {
TRACE("dl", tout << "input " << i << " in " << p->get_decl()->get_name() << "\n";);
bv.unset(i);
}
TRACE("dl", tout << i << " in " << p->get_decl()->get_name() << " is a value, unable to slice\n";);
bv.unset(i);
}
}
}