diff options
Diffstat (limited to 'src/proof/cnf_proof.cpp')
-rw-r--r-- | src/proof/cnf_proof.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp index 69b613f28..d1a228ecb 100644 --- a/src/proof/cnf_proof.cpp +++ b/src/proof/cnf_proof.cpp @@ -350,8 +350,9 @@ void LFSCCnfProof::printAtomMapping(const std::set<Node>& atoms, prop::SatVariable var = getLiteral(atom).getSatVariable(); //FIXME hideous LFSCTheoryProofEngine* pe = (LFSCTheoryProofEngine*)ProofManager::currentPM()->getTheoryProofEngine(); - // pe->printLetTerm(atom.toExpr(), os); + if (pe->printsAsBool(atom.toExpr())) os << "(p_app "; pe->printBoundTerm(atom.toExpr(), os, letMap); + if (pe->printsAsBool(atom.toExpr())) os << ")"; os << " (\\ " << ProofManager::getVarName(var, d_name); os << " (\\ " << ProofManager::getAtomName(var, d_name) << "\n"; |