From 2c8b314a15ba1bfc79e508b0266df1405782656b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 13 Jun 2013 13:34:20 -0700 Subject: [PATCH] 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) {