From 90312eb079b1f70ea4d8d229f66273a66a1b7ab1 Mon Sep 17 00:00:00 2001
From: Guy <katz911@gmail.com>
Date: Tue, 26 Jul 2016 16:37:57 -0700
Subject: [PATCH] Bug fix: If a lemma (a disjunction) has a "false" literal in
 it, it can be ignored, but a "true" literal really should stay

---
 src/proof/proof_manager.cpp | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index e5e00f117..65dbb644d 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -336,11 +336,8 @@ std::set<Node> ProofManager::satClauseToNodeSet(prop::SatClause* clause) {
     prop::SatLiteral lit = (*clause)[i];
     Node node = getCnfProof()->getAtom(lit.getSatVariable());
     Expr atom = node.toExpr();
-    if (atom.isConst()) {
-      Assert (atom == utils::mkTrue());
-      continue;
-    }
-    result.insert(lit.isNegated() ? node.notNode() : node);
+    if (atom != utils::mkTrue())
+      result.insert(lit.isNegated() ? node.notNode() : node);
   }
 
   return result;
-- 
2.30.2