From a914142c7c6caf89dca96f99c211f449d9725b26 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 31 Mar 2018 05:34:11 -0700 Subject: [PATCH] bit-blaster Signed-off-by: Nikolaj Bjorner --- src/tactic/aig/aig_tactic.cpp | 3 ++- src/tactic/bv/bit_blaster_model_converter.cpp | 10 ++-------- 2 files changed, 4 insertions(+), 9 deletions(-) diff --git a/src/tactic/aig/aig_tactic.cpp b/src/tactic/aig/aig_tactic.cpp index 25c693fde..720c799e0 100644 --- a/src/tactic/aig/aig_tactic.cpp +++ b/src/tactic/aig/aig_tactic.cpp @@ -67,7 +67,6 @@ public: void operator()(goal_ref const & g) { SASSERT(g->is_well_sorted()); - tactic_report report("aig", *g); mk_aig_manager mk(*this, g->m()); if (m_aig_per_assertion) { @@ -92,8 +91,10 @@ public: void operator()(goal_ref const & g, goal_ref_buffer & result) override { fail_if_proof_generation("aig", g); + tactic_report report("aig", *g); operator()(g); g->inc_depth(); + TRACE("aig", g->display(tout);); result.push_back(g.get()); } diff --git a/src/tactic/bv/bit_blaster_model_converter.cpp b/src/tactic/bv/bit_blaster_model_converter.cpp index 406781c1f..4fb66b05d 100644 --- a/src/tactic/bv/bit_blaster_model_converter.cpp +++ b/src/tactic/bv/bit_blaster_model_converter.cpp @@ -123,10 +123,7 @@ struct bit_blaster_model_converter : public model_converter { SASSERT(is_uninterp_const(bit)); func_decl * bit_decl = to_app(bit)->get_decl(); expr * bit_val = old_model->get_const_interp(bit_decl); - if (bit_val == nullptr) { - goto bail; - } - if (m().is_true(bit_val)) + if (bit_val != nullptr && m().is_true(bit_val)) val++; } } @@ -141,10 +138,7 @@ struct bit_blaster_model_converter : public model_converter { func_decl * bit_decl = to_app(bit)->get_decl(); expr * bit_val = old_model->get_const_interp(bit_decl); // remark: if old_model does not assign bit_val, then assume it is false. - if (bit_val == nullptr) { - goto bail; - } - if (!util.is_zero(bit_val)) + if (bit_val != nullptr && !util.is_zero(bit_val)) val++; } }