mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-13 09:26:15 +00:00
Code Activity

don't reset core after it has been populated for the cut #3451 and presumably other bugs

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-23 13:19:28 -07:00 • committed by Lev Nachmanson
parent 38eca3b66a
commit e16c62d6e2
2 changed files with 5 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/smt_context_pp.cpp
View file

@ -454,6 +454,7 @@ namespace smt {
display_lemma_as_smt_problem(out, num_antecedents, antecedents, consequent, logic); display_lemma_as_smt_problem(out, num_antecedents, antecedents, consequent, logic);
TRACE("non_linear", display_lemma_as_smt_problem(tout, num_antecedents, antecedents, consequent, logic);); TRACE("non_linear", display_lemma_as_smt_problem(tout, num_antecedents, antecedents, consequent, logic););
out.close(); out.close();
SASSERT(m_lemma_id != 78);
return m_lemma_id; return m_lemma_id;
} }
@ -497,6 +498,7 @@ namespace smt {
); );
display_lemma_as_smt_problem(out, num_antecedents, antecedents, num_eq_antecedents, eq_antecedents, consequent, logic); display_lemma_as_smt_problem(out, num_antecedents, antecedents, num_eq_antecedents, eq_antecedents, consequent, logic);
out.close(); out.close();
SASSERT(m_lemma_id != 78);
return m_lemma_id; return m_lemma_id;
} }

6
src/smt/theory_lra.cpp
View file

@ -2044,6 +2044,9 @@ public:
TRACE("arith", tout << "cut\n";); TRACE("arith", tout << "cut\n";);
++m_stats.m_gomory_cuts; ++m_stats.m_gomory_cuts;
// m_explanation implies term <= k // m_explanation implies term <= k
m_eqs.reset();
m_core.reset();
m_params.reset();
for (auto const& ev : m_explanation) { for (auto const& ev : m_explanation) {
if (!ev.first.is_zero()) { if (!ev.first.is_zero()) {
set_evidence(ev.second); set_evidence(ev.second);
@ -2058,9 +2061,6 @@ public:
} }
IF_VERBOSE(4, verbose_stream() << "cut " << b << "\n"); IF_VERBOSE(4, verbose_stream() << "cut " << b << "\n");
TRACE("arith", dump_cut_lemma(tout, m_lia->get_term(), m_lia->get_offset(), m_explanation, m_lia->is_upper());); TRACE("arith", dump_cut_lemma(tout, m_lia->get_term(), m_lia->get_offset(), m_explanation, m_lia->is_upper()););
m_eqs.reset();
m_core.reset();
m_params.reset();
literal lit(ctx().get_bool_var(b), false); literal lit(ctx().get_bool_var(b), false);
TRACE("arith", TRACE("arith",
ctx().display_lemma_as_smt_problem(tout << "new cut:\n", m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), lit); ctx().display_lemma_as_smt_problem(tout << "new cut:\n", m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), lit);