diff options
author | Guy <katz911@gmail.com> | 2016-08-03 15:51:22 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-08-03 15:51:22 -0700 |
commit | c82514b57252444df982b35af4809e0fd4635e37 (patch) | |
tree | 12ad1fe87c8d7723762a120645006bed29ce8c51 /src/proof/proof_manager.cpp | |
parent | 53020abb9381f4e29d628c054c990ddb43bba4b2 (diff) |
Fixed an issue where arrays proofs would sometimes have an extra ")" at the end.
Diffstat (limited to 'src/proof/proof_manager.cpp')
-rw-r--r-- | src/proof/proof_manager.cpp | 13 |
1 files changed, 5 insertions, 8 deletions
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index 42319153f..e987f1c6f 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -596,6 +596,7 @@ void LFSCProof::toStream(std::ostream& out) { smt::SmtScope scope(d_smtEngine); std::ostringstream paren; out << "(check\n"; + paren << ")"; out << " ;; Declarations\n"; // declare the theory atoms @@ -618,6 +619,7 @@ void LFSCProof::toStream(std::ostream& out) { Debug("pf::pm") << std::endl << "LFSCProof::toStream: print assertions DONE" << std::endl; out << "(: (holds cln)\n\n"; + paren << ")"; // Have the theory proofs print deferred declarations, e.g. for skolem variables. out << " ;; Printing deferred declarations \n\n"; @@ -659,20 +661,15 @@ void LFSCProof::toStream(std::ostream& out) { Debug("pf::pm") << "Proof manager: printing theory lemmas DONE!" << std::endl; if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER && ProofManager::getBitVectorProof()) { - // print actual resolution proof - // d_satProof->printResolutions(out, paren); ProofManager::getBitVectorProof()->getSatProof()->printResolutionEmptyClause(out, paren); - paren <<")))\n;;"; - out << paren.str(); - out << "\n"; } else { // print actual resolution proof d_satProof->printResolutions(out, paren); d_satProof->printResolutionEmptyClause(out, paren); - paren <<")))\n;;"; - out << paren.str(); - out << "\n"; } + + out << paren.str(); + out << "\n;;\n"; } void LFSCProof::printPreprocessedAssertions(const NodeSet& assertions, |