diff options
Diffstat (limited to 'src/prop/cnf_stream.cpp')
| -rw-r--r-- | src/prop/cnf_stream.cpp | 9 |
1 files changed, 1 insertions, 8 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index eda736b8a..f2401041e 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -678,8 +678,7 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool removable, bool negated, ProofRule proof_id, - TNode from, - LemmaProofRecipe* proofRecipe) { + TNode from) { Debug("cnf") << "convertAndAssert(" << node << ", removable = " << (removable ? "true" : "false") << ", negated = " << (negated ? "true" : "false") << ")" << endl; @@ -689,12 +688,6 @@ void TseitinCnfStream::convertAndAssert(TNode node, Node assertion = negated ? node.notNode() : (Node)node; Node from_assertion = negated? from.notNode() : (Node) from; - if (proofRecipe) { - Debug("pf::sat") << "TseitinCnfStream::convertAndAssert: setting proof recipe" << std::endl; - proofRecipe->dump("pf::sat"); - d_cnfProof->setProofRecipe(proofRecipe); - } - if (proof_id != RULE_INVALID) { d_cnfProof->pushCurrentAssertion(from.isNull() ? assertion : from_assertion); d_cnfProof->registerAssertion(from.isNull() ? assertion : from_assertion, proof_id); |