From 2d1a0b010ddcfc965f6cd8064b2a48ba2fefdc04 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 14 May 2015 13:44:39 +0100 Subject: [PATCH] Bugfix for AIG tactic. --- src/tactic/aig/aig_tactic.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/tactic/aig/aig_tactic.cpp b/src/tactic/aig/aig_tactic.cpp index dc577eb73..f1f1c7330 100644 --- a/src/tactic/aig/aig_tactic.cpp +++ b/src/tactic/aig/aig_tactic.cpp @@ -78,13 +78,13 @@ public: mk_aig_manager mk(*this, g->m()); if (m_aig_per_assertion) { - unsigned size = g->size(); - for (unsigned i = 0; i < size; i++) { + for (unsigned i = 0; i < g->size(); i++) { aig_ref r = m_aig_manager->mk_aig(g->form(i)); m_aig_manager->max_sharing(r); expr_ref new_f(g->m()); 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 {