From 6fa28b63b3345d64de3a1ac55b2e41600c678424 Mon Sep 17 00:00:00 2001
From: Guy <katz911@gmail.com>
Date: Tue, 19 Jul 2016 19:33:15 -0700
Subject: [PATCH] Bug fix

---
 src/proof/proof_manager.cpp | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 09fc5dc8b..cb6eee330 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -321,7 +321,12 @@ void ProofManager::getLemmasInUnsatCore(theory::TheoryId theory, std::vector<Nod
       lemma.insert(lit.isNegated() ? node.notNode() : node);
     }
 
-    LemmaProofRecipe recipe = getCnfProof()->getProofRecipe(lemma);
+    // TODO: we should be able to drop the "haveProofRecipe" check.
+    // 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 (recipe.simpleLemma() && recipe.getTheory() == theory) {
       lemmas.push_back(recipe.getOriginalLemma());
-- 
2.30.2