From 9dd9a6f7cff50d6877a81675073a322730afad91 Mon Sep 17 00:00:00 2001
From: Guy <katz911@gmail.com>
Date: Wed, 27 Jul 2016 09:46:24 -0700
Subject: [PATCH] If we can't find a weaker implicant, fail gracefully and
 return the original lemma

---
 src/proof/proof_manager.cpp | 16 ++++++++++------
 1 file changed, 10 insertions(+), 6 deletions(-)

diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 65dbb644d..0e683b084 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -321,9 +321,10 @@ void ProofManager::getLemmasInUnsatCore(theory::TheoryId theory, std::vector<Nod
     // however, there are some rewrite issues with the arith solver, resulting
     // in non-registered recipes. For now we assume no one is requesting arith lemmas.
     LemmaProofRecipe recipe;
-    if (getCnfProof()->haveProofRecipe(lemma))
-      recipe = getCnfProof()->getProofRecipe(lemma);
+    if (!getCnfProof()->haveProofRecipe(lemma))
+      continue;
 
+    recipe = getCnfProof()->getProofRecipe(lemma);
     if (recipe.simpleLemma() && recipe.getTheory() == theory) {
       lemmas.push_back(recipe.getOriginalLemma());
     }
@@ -368,9 +369,10 @@ Node ProofManager::getWeakestImplicantInUnsatCore(Node lemma) {
     // however, there are some rewrite issues with the arith solver, resulting
     // in non-registered recipes. For now we assume no one is requesting arith lemmas.
     LemmaProofRecipe recipe;
-    if (getCnfProof()->haveProofRecipe(currentLemma))
-      recipe = getCnfProof()->getProofRecipe(currentLemma);
+    if (!getCnfProof()->haveProofRecipe(currentLemma))
+      continue;
 
+    recipe = getCnfProof()->getProofRecipe(currentLemma);
     if (recipe.getOriginalLemma() == lemma) {
       for (lemmaIt = currentLemma.begin(); lemmaIt != currentLemma.end(); ++lemmaIt) {
         builder << *lemmaIt;
@@ -381,12 +383,14 @@ Node ProofManager::getWeakestImplicantInUnsatCore(Node lemma) {
           if (lemma[i] == *lemmaIt)
             found = true;
         }
-        AlwaysAssert(found);
+
+        if (!found)
+          return lemma;
       }
     }
   }
 
-  Assert(builder.getNumChildren() != 0);
+  AlwaysAssert(builder.getNumChildren() != 0);
 
   if (builder.getNumChildren() == 1)
     return builder[0];
-- 
2.30.2