From b980a15177515456a7f51eadaca9bf2659f1e295 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 4 Dec 2013 13:02:49 -0800 Subject: [PATCH 1/2] fix leak by commenting out probe experiment Signed-off-by: Nikolaj Bjorner --- src/opt/fu_malik.cpp | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/src/opt/fu_malik.cpp b/src/opt/fu_malik.cpp index 99ecdf2a5..cf0fefe52 100644 --- a/src/opt/fu_malik.cpp +++ b/src/opt/fu_malik.cpp @@ -205,12 +205,13 @@ namespace opt { if (!found) { continue; } - expr_ref block_var(m); + expr_ref block_var(m), tmp(m); block_var = m.mk_fresh_const("block_var", m.mk_bool_sort()); m_aux[i] = m.mk_fresh_const("aux", m.mk_bool_sort()); m_soft[i] = m.mk_or(m_soft[i].get(), block_var); block_vars.push_back(block_var); - s().assert_expr(m.mk_or(m_soft[i].get(), m_aux[i].get())); + tmp = m.mk_or(m_soft[i].get(), m_aux[i].get()); + s().assert_expr(tmp); } SASSERT (!block_vars.empty()); assert_at_most_one(block_vars); @@ -252,7 +253,9 @@ namespace opt { for (unsigned i = 0; i < num_assertions; ++i) { g.assert_expr(current_solver.get_assertion(i)); } - probe *p = mk_is_qfbv_probe(); +#if 0 + // TBD: this leaks references somehow + probe_ref p = mk_is_qfbv_probe(); bool all_bv = (*p)(g).is_true(); if (all_bv) { smt::context & ctx = opt_s.get_context(); @@ -266,6 +269,7 @@ namespace opt { m_use_new_bv_solver = true; IF_VERBOSE(1, verbose_stream() << "Force to use the new BV solver." << std::endl;); } +#endif } // TBD: bug when cancel flag is set, fu_malik returns is_sat == l_true instead of l_undef @@ -274,9 +278,11 @@ namespace opt { lbool is_sat = s().check_sat(0,0); if (!m_soft.empty() && is_sat == l_true) { solver::scoped_push _sp(s()); + expr_ref tmp(m); for (unsigned i = 0; i < m_soft.size(); ++i) { m_aux.push_back(m.mk_fresh_const("p", m.mk_bool_sort())); - s().assert_expr(m.mk_or(m_soft[i].get(), m_aux[i].get())); + tmp = m.mk_or(m_soft[i].get(), m_aux[i].get()); + s().assert_expr(tmp); } lbool is_sat = l_true; From ead414c4ee8e72c1d9fad7bcdae7aa4a357cf51c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 4 Dec 2013 13:11:58 -0800 Subject: [PATCH 2/2] add back skipped consequences, exposed by fu-malik assertion violation Signed-off-by: Nikolaj Bjorner --- src/smt/theory_pb.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index d8d90b19a..e5686e2e2 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -1251,6 +1251,7 @@ namespace smt { justification* cjs = cls.get_justification(); if (cjs) { IF_VERBOSE(0, verbose_stream() << "skipping justification for clause over: " << conseq << "\n";); + m_ineq_literals.push_back(conseq); break; } unsigned num_lits = cls.get_num_literals(); @@ -1282,6 +1283,7 @@ namespace smt { // only process pb justifications. if (j.get_from_theory() != get_id()) { IF_VERBOSE(0, verbose_stream() << "skipping justification for " << conseq << "\n";); + m_ineq_literals.push_back(conseq); break; } pb_justification& pbj = dynamic_cast(j);