From 063f6fe15f7a0269359a59e6129b796a1e6950ae Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 4 Nov 2013 12:26:20 -0800
Subject: [PATCH] fix assertion violations (reported by Christoph
 Wintersteiger) at sage\app8\bench_2174.smt2, sage\app9\bench_1450.smt2,
 sage\app9\bench_1546.smt2

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/sat/sat_simplifier.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index 37d41a5fd..f20ffa7c7 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -407,7 +407,7 @@ namespace sat {
                 remove_clause(c2);
                 m_num_subsumed++;
             }
-            else {
+            else if (!c2.was_removed()) {
                 // subsumption resolution
                 TRACE("subsumption_resolution", tout << c1 << " sub-ref(" << *l_it << ") " << c2 << "\n";);
                 elim_lit(c2, *l_it);