diff options
Diffstat (limited to 'src/proof/drat/drat_proof.cpp')
-rw-r--r-- | src/proof/drat/drat_proof.cpp | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/proof/drat/drat_proof.cpp b/src/proof/drat/drat_proof.cpp index c2f2fa49e..5b9487a00 100644 --- a/src/proof/drat/drat_proof.cpp +++ b/src/proof/drat/drat_proof.cpp @@ -259,12 +259,12 @@ void DratProof::outputAsLfsc(std::ostream& os, uint8_t indentation) const { case ADDITION: { - os << "DRATProofa"; + os << "DRATProofa "; break; } case DELETION: { - os << "DRATProofd"; + os << "DRATProofd "; break; } default: { Unreachable("Unrecognized DRAT instruction kind"); @@ -273,7 +273,7 @@ void DratProof::outputAsLfsc(std::ostream& os, uint8_t indentation) const for (const SatLiteral& l : i.d_clause) { os << "(clc (" << (l.isNegated() ? "neg " : "pos ") - << ProofManager::getVarName(l.getSatVariable()) << ") "; + << ProofManager::getVarName(l.getSatVariable(), "bb") << ") "; } os << "cln"; std::fill_n(std::ostream_iterator<char>(os), i.d_clause.size(), ')'); |