diff options
author | Guy <katz911@gmail.com> | 2016-07-19 19:33:15 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-07-19 19:33:15 -0700 |
commit | 6fa28b63b3345d64de3a1ac55b2e41600c678424 (patch) | |
tree | b2269d5754594620c1aacd4c245bb36eb8f65e8c /src/proof | |
parent | 3e3563a1f312b024653503837a56aef10a41eb9f (diff) |
Bug fix
Diffstat (limited to 'src/proof')
-rw-r--r-- | src/proof/proof_manager.cpp | 7 |
1 files changed, 6 insertions, 1 deletions
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()); |