mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-17 11:26:17 +00:00
Code Activity

fix #3385

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-18 10:50:26 -07:00
parent 31164c2eaf
commit fbf5fc9482
1 changed files with 12 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/tactic/arith/eq2bv_tactic.cpp
View file

@ -152,6 +152,7 @@ public:
obj_map<expr, expr*> m_fd; obj_map<expr, expr*> m_fd;
obj_map<expr, unsigned> m_max; obj_map<expr, unsigned> m_max;
expr_mark m_nonfd; expr_mark m_nonfd;
ast_mark m_has_eq;
ptr_vector<expr> m_todo; ptr_vector<expr> m_todo;
eq2bv_tactic(ast_manager & _m): eq2bv_tactic(ast_manager & _m):
@ -175,6 +176,7 @@ public:
m_fd.reset(); m_fd.reset();
m_max.reset(); m_max.reset();
m_nonfd.reset(); m_nonfd.reset();
m_has_eq.reset();
m_bounds.reset(); m_bounds.reset();
ref<bvmc> mc1 = alloc(bvmc, m); ref<bvmc> mc1 = alloc(bvmc, m);
@ -197,7 +199,7 @@ public:
proof_ref new_pr(m); proof_ref new_pr(m);
func_decl_ref var(m); func_decl_ref var(m);
unsigned val; unsigned val;
if (is_bound(g->form(i), var, val)) { if (is_bound(g->form(i), var, val) && !m_has_eq.is_marked(var)) {
g->update(i, m.mk_true(), nullptr, nullptr); g->update(i, m.mk_true(), nullptr, nullptr);
mc1->insert(var, val); mc1->insert(var, val);
continue; continue;
@ -311,7 +313,14 @@ public:
return is_lower(f, var, val) || is_upper(f, var, val); return is_lower(f, var, val) || is_upper(f, var, val);
} }
void mark_has_eq(expr* e) {
if (is_uninterp_const(e)) {
m_has_eq.mark(to_app(e)->get_decl(), true);
}
}
void collect_fd(expr* f) { void collect_fd(expr* f) {
m_trail.push_back(f);
func_decl_ref var(m); func_decl_ref var(m);
unsigned val; unsigned val;
if (is_bound(f, var, val)) return; if (is_bound(f, var, val)) return;
@ -325,6 +334,8 @@ public:
m_nonfd.mark(f, true); m_nonfd.mark(f, true);
expr* e1, *e2; expr* e1, *e2;
if (m.is_eq(f, e1, e2)) { if (m.is_eq(f, e1, e2)) {
mark_has_eq(e1);
mark_has_eq(e2);
if (is_fd(e1, e2) || is_fd(e2, e1)) { if (is_fd(e1, e2) || is_fd(e2, e1)) {
continue; continue;
} }