From 72651e2e98b38a8eec25acffa41f1b5470a76fa8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 14 Mar 2017 19:35:11 -0700 Subject: [PATCH] fixing sources for double frees of clauses. #940 Signed-off-by: Nikolaj Bjorner --- src/sat/sat_asymm_branch.cpp | 2 +- src/sat/sat_simplifier.cpp | 5 ++++- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/src/sat/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp index 8a761ea3a..782713d5c 100644 --- a/src/sat/sat_asymm_branch.cpp +++ b/src/sat/sat_asymm_branch.cpp @@ -188,8 +188,8 @@ namespace sat { case 1: TRACE("asymm_branch", tout << "produced unit clause: " << c[0] << "\n";); s.assign(c[0], justification()); - s.del_clause(c); s.propagate_core(false); + s.del_clause(c); 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: diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index bd975115b..e744bc007 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -279,7 +279,10 @@ namespace sat { unsigned sz = c.size(); if (sz == 0) { s.set_conflict(justification()); - return; + for (; it != end; ++it, ++it2) { + *it2 = *it; + } + break; } if (sz == 1) { s.assign(c[0], justification());