From: Guy <katz911@gmail.com>
Date: Wed, 27 Jul 2016 16:46:24 +0000 (-0700)
Subject: If we can't find a weaker implicant, fail gracefully and return the original lemma
X-Git-Tag: cvc5-1.0.0~6040^2~24
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9dd9a6f7cff50d6877a81675073a322730afad91;p=cvc5.git

If we can't find a weaker implicant, fail gracefully and return the original lemma
---

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];