From 1eb4ddfc5c47c16c66bb3e8eb87351470854ceec Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 25 May 2018 10:38:46 -0700 Subject: Fix --- src/prop/minisat/core/Solver.cc | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 94878f7bc..00ff5315c 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -1789,9 +1789,10 @@ CRef Solver::updateLemmas() { ( TNode cnf_assertion = lemmas_cnf_assertion[i].first; TNode cnf_def = lemmas_cnf_assertion[i].second; + bool isInput = ProofManager::getCnfProof()->isAssertion(cnf_assertion) && ProofManager::getCnfProof()->getProofRule(cnf_assertion) == RULE_GIVEN; Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (2)" << std::endl; - ClauseId id = ProofManager::getSatProof()->registerClause(lemma_ref, THEORY_LEMMA); + ClauseId id = ProofManager::getSatProof()->registerClause(lemma_ref, isInput ? INPUT : THEORY_LEMMA); ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion); ProofManager::getCnfProof()->setClauseDefinition(id, cnf_def); ); @@ -1806,9 +1807,10 @@ CRef Solver::updateLemmas() { ( Node cnf_assertion = lemmas_cnf_assertion[i].first; Node cnf_def = lemmas_cnf_assertion[i].second; + bool isInput = ProofManager::getCnfProof()->isAssertion(cnf_assertion) && ProofManager::getCnfProof()->getProofRule(cnf_assertion) == RULE_GIVEN; Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (3)" << std::endl; - ClauseId id = ProofManager::getSatProof()->registerUnitClause(lemma[0], THEORY_LEMMA); + ClauseId id = ProofManager::getSatProof()->registerUnitClause(lemma[0], isInput ? INPUT : THEORY_LEMMA); ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion); ProofManager::getCnfProof()->setClauseDefinition(id, cnf_def); ); -- cgit v1.2.3