diff options
Diffstat (limited to 'src/proof/proof_manager.cpp')
| -rw-r--r-- | src/proof/proof_manager.cpp | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index 5ce615366..ddd2029fb 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -565,6 +565,7 @@ void LFSCProof::toStream(std::ostream& out) { Debug("pf::pm") << "\t assertion = " << *it3 << std::endl; std::set<Node> atoms; + NodePairSet rewrites; // collects the atoms in the clauses d_cnfProof->collectAtomsAndRewritesForLemmas(used_lemmas, atoms, rewrites); @@ -779,7 +780,9 @@ void LFSCProof::printPreprocessedAssertions(const NodeSet& assertions, //TODO os << "(trust_f "; + if (ProofManager::currentPM()->getTheoryProofEngine()->printsAsBool(*it)) os << "(p_app "; ProofManager::currentPM()->getTheoryProofEngine()->printTheoryTerm((*it).toExpr(), os, globalLetMap); + if (ProofManager::currentPM()->getTheoryProofEngine()->printsAsBool(*it)) os << ")"; os << ") "; os << "(\\ "<< ProofManager::getPreprocessedAssertionName(*it, "") << "\n"; |