diff options
Diffstat (limited to 'src/proof')
-rw-r--r-- | src/proof/proof_manager.cpp | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index a0b25fab1..a86991963 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -313,6 +313,7 @@ void ProofManager::getLemmasInUnsatCore(theory::TheoryId theory, std::vector<Nod d_satProof->collectClausesUsed(used_inputs, used_lemmas); IdToSatClause::const_iterator it; + std::set<Node> seen; for (it = used_lemmas.begin(); it != used_lemmas.end(); ++it) { std::set<Node> lemma = satClauseToNodeSet(it->second); @@ -325,8 +326,9 @@ void ProofManager::getLemmasInUnsatCore(theory::TheoryId theory, std::vector<Nod continue; recipe = getCnfProof()->getProofRecipe(lemma); - if (recipe.simpleLemma() && recipe.getTheory() == theory) { + if (recipe.simpleLemma() && recipe.getTheory() == theory && seen.find(recipe.getOriginalLemma()) == seen.end()) { lemmas.push_back(recipe.getOriginalLemma()); + seen.insert(recipe.getOriginalLemma()); } } } |