mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-06 19:21:22 +00:00
Code Activity

fix #3504

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-25 02:30:51 -07:00
parent 0609408fd7
commit ea396a008a
3 changed files with 15 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -200,13 +200,19 @@ public:
func_decl_ref var(m);
unsigned val;
if (is_bound(g->form(i), var, val) && !m_has_eq.is_marked(var)) {
g->update(i, m.mk_true(), nullptr, nullptr);
if (m.proofs_enabled()) {
new_pr = m.mk_rewrite(g->form(i), m.mk_true());
new_pr = m.mk_modus_ponens(g->pr(i), new_pr);
}
g->update(i, m.mk_true(), new_pr, nullptr);
mc1->insert(var, val);
continue;
}
m_rw(g->form(i), new_curr, new_pr);
if (m.proofs_enabled() && !new_pr) {
new_pr = m.mk_rewrite(g->form(i), new_curr);
if (g->form(i) == new_curr)
continue;
if (m.proofs_enabled()) {
if (!new_pr) new_pr = m.mk_rewrite(g->form(i), new_curr);
new_pr = m.mk_modus_ponens(g->pr(i), new_pr);
}
g->update(i, new_curr, new_pr, g->dep(i));