mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-31 19:29:13 +00:00
Code Activity

Bugfix for AIG tactic.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-05-14 13:44:39 +01:00
parent ce749240d7
commit 2d1a0b010d
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/tactic/aig/aig_tactic.cpp
View file

@ -78,13 +78,13 @@ public:
mk_aig_manager mk(*this, g->m()); mk_aig_manager mk(*this, g->m());
if (m_aig_per_assertion) { if (m_aig_per_assertion) {
unsigned size = g->size(); for (unsigned i = 0; i < g->size(); i++) {
for (unsigned i = 0; i < size; i++) {
aig_ref r = m_aig_manager->mk_aig(g->form(i)); aig_ref r = m_aig_manager->mk_aig(g->form(i));
m_aig_manager->max_sharing(r); m_aig_manager->max_sharing(r);
expr_ref new_f(g->m()); expr_ref new_f(g->m());
m_aig_manager->to_formula(r, new_f); m_aig_manager->to_formula(r, new_f);
g->update(i, new_f, 0, g->dep(i)); expr_dependency * ed = g->dep(i);
g->update(i, new_f, 0, ed);
} }
} }
else { else {