From 6184c5fdbcad3ad666f8220cdebcae4601b03bd1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 11 Jun 2013 15:29:22 -0400 Subject: [PATCH 1/3] reorder attibutes to match initialization order Signed-off-by: Nikolaj Bjorner --- src/muz_qe/dl_instruction.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/muz_qe/dl_instruction.cpp b/src/muz_qe/dl_instruction.cpp index 6b16968c2..637d9a17f 100644 --- a/src/muz_qe/dl_instruction.cpp +++ b/src/muz_qe/dl_instruction.cpp @@ -528,9 +528,9 @@ namespace datalog { class instr_filter_interpreted_and_project : public instruction { reg_idx m_src; - reg_idx m_res; app_ref m_cond; unsigned_vector m_cols; + reg_idx m_res; public: instr_filter_interpreted_and_project(reg_idx src, app_ref & condition, unsigned col_cnt, const unsigned * removed_cols, reg_idx result) From 2c8b314a15ba1bfc79e508b0266df1405782656b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 13 Jun 2013 13:34:20 -0700 Subject: [PATCH 2/3] Fix issue https://z3.codeplex.com/workitem/48 Signed-off-by: Leonardo de Moura --- src/sat/sat_simplifier.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 623c73758..47c4b6150 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -625,7 +625,8 @@ namespace sat { case 1: TRACE("elim_lit", tout << "clause became unit: " << c[0] << "\n";); propagate_unit(c[0]); - remove_clause(c); + // propagate_unit will delete c. + // remove_clause(c); return; case 2: TRACE("elim_lit", tout << "clause became binary: " << c[0] << " " << c[1] << "\n";); @@ -816,7 +817,8 @@ namespace sat { } if (sz == 1) { propagate_unit(c[0]); - remove_clause(c); + // propagate_unit will delete c. + // remove_clause(c); continue; } if (sz == 2) { From 40b1137b30da4914c233001a704928662567f60d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 13 Jun 2013 13:45:14 -0700 Subject: [PATCH 3/3] Fix issue https://z3.codeplex.com/workitem/47 Signed-off-by: Leonardo de Moura --- src/sat/sat_asymm_branch.cpp | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/sat/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp index 81d631e4e..b8ac520b2 100644 --- a/src/sat/sat_asymm_branch.cpp +++ b/src/sat/sat_asymm_branch.cpp @@ -72,11 +72,14 @@ namespace sat { int limit = -static_cast(m_asymm_branch_limit); std::stable_sort(s.m_clauses.begin(), s.m_clauses.end(), clause_size_lt()); m_counter -= s.m_clauses.size(); + SASSERT(s.m_qhead == s.m_trail.size()); clause_vector::iterator it = s.m_clauses.begin(); clause_vector::iterator it2 = it; clause_vector::iterator end = s.m_clauses.end(); try { for (; it != end; ++it) { + if (s.inconsistent()) + break; SASSERT(s.m_qhead == s.m_trail.size()); if (m_counter < limit || s.inconsistent()) { *it2 = *it; @@ -111,6 +114,7 @@ namespace sat { bool asymm_branch::process(clause & c) { TRACE("asymm_branch_detail", tout << "processing: " << c << "\n";); SASSERT(s.scope_lvl() == 0); + SASSERT(s.m_qhead == s.m_trail.size()); #ifdef Z3DEBUG unsigned trail_sz = s.m_trail.size(); #endif @@ -143,6 +147,7 @@ namespace sat { SASSERT(!s.inconsistent()); SASSERT(s.scope_lvl() == 0); SASSERT(trail_sz == s.m_trail.size()); + SASSERT(s.m_qhead == s.m_trail.size()); if (i == sz - 1) { // clause size can't be reduced. s.attach_clause(c); @@ -181,15 +186,18 @@ namespace sat { s.assign(c[0], justification()); s.del_clause(c); s.propagate_core(false); + SASSERT(s.inconsistent() || s.m_qhead == s.m_trail.size()); return false; // check_missed_propagation() may fail, since m_clauses is not in a consistent state. case 2: SASSERT(s.value(c[0]) == l_undef && s.value(c[1]) == l_undef); s.mk_bin_clause(c[0], c[1], false); s.del_clause(c); + SASSERT(s.m_qhead == s.m_trail.size()); return false; default: c.shrink(new_sz); s.attach_clause(c); + SASSERT(s.m_qhead == s.m_trail.size()); return true; } }