mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix #5256

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-05-17 17:41:34 -07:00
parent 4f9ad28a05
commit 30974968af
1 changed files with 33 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

52
src/smt/tactic/ctx_solver_simplify_tactic.cpp
View file

@ -213,37 +213,51 @@ protected:
sz = a->get_num_args(); sz = a->get_num_args();
n2 = nullptr; n2 = nullptr;
bool found = false;
//
// This is a single traversal version of the context
// simplifier. It simplifies only the first occurrence of
// a sub-term with respect to the context.
//
for (unsigned i = 0; i < sz; ++i) { for (unsigned i = 0; i < sz; ++i) {
expr* arg = a->get_arg(i); expr* arg = a->get_arg(i);
if (cache.find(arg, path_r)) { if (cache.find(arg, path_r) &&
// path_r.m_parent == self_pos && path_r.m_idx == i) {
// This is a single traversal version of the context args.push_back(path_r.m_expr);
// simplifier. It simplifies only the first occurrence of found = true;
// a sub-term with respect to the context. continue;
// }
args.push_back(arg);
if (path_r.m_parent == self_pos && path_r.m_idx == i) { }
args.push_back(path_r.m_expr);
//
// the context is not equivalent to top-level
// if it is already simplified.
// Bug exposes such a scenario #5256
//
if (!found) {
args.reset();
for (unsigned i = 0; i < sz; ++i) {
expr* arg = a->get_arg(i);
if (!n2 && !m.is_value(arg)) {
n2 = mk_fresh(id, arg->get_sort());
trail.push_back(n2);
todo.push_back(expr_pos(self_pos, ++child_id, i, arg));
names.push_back(n2);
args.push_back(n2);
} }
else { else {
args.push_back(arg); args.push_back(arg);
} }
} }
else if (!n2 && !m.is_value(arg)) {
n2 = mk_fresh(id, arg->get_sort());
trail.push_back(n2);
todo.push_back(expr_pos(self_pos, ++child_id, i, arg));
names.push_back(n2);
args.push_back(n2);
}
else {
args.push_back(arg);
}
} }
m_mk_app(a->get_decl(), args.size(), args.data(), res); m_mk_app(a->get_decl(), args.size(), args.data(), res);
trail.push_back(res); trail.push_back(res);
// child needs to be visited. // child needs to be visited.
if (n2) { if (n2) {
SASSERT(!found);
m_solver.push(); m_solver.push();
tmp = m.mk_eq(res, n); tmp = m.mk_eq(res, n);
m_solver.assert_expr(tmp); m_solver.assert_expr(tmp);