Fixed an issue where arrays proofs would sometimes have an extra ")" at the end.

diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp
index ccc072eca48e6d89736f146b39132b42a6834c28..514d8118455b5f96085540ecda019cff16ecfb15 100644 (file)
--- a/src/proof/array_proof.cpp
+++ b/src/proof/array_proof.cpp
@@ -1324,6 +1324,7 @@ void LFSCArrayProof::printTermDeclarations(std::ostream& os, std::ostream& paren
       printSort(array_type.getConstituentType(), os);
 
       os << "))\n";
+      paren << ")";
     } else {
       Assert(term.isVariable());
       if (ProofManager::getSkolemizationManager()->isSkolem(*it)) {
@@ -1333,10 +1334,9 @@ void LFSCArrayProof::printTermDeclarations(std::ostream& os, std::ostream& paren
         os << "(% " << ProofManager::sanitize(term) << " ";
         os << "(term ";
         os << term.getType() << ")\n";
+        paren << ")";
       }
     }
-
-    paren << ")";
   }
 
   Debug("pf::array") << "Declaring terms done!" << std::endl;

diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 42319153fe9e4529541cc23dbe2cc03e8de4c021..e987f1c6fba2577b6963ecfde3ad55ff326d2100 100644 (file)
--- 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,

diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h
index fc2bae19b56fa2d76b00ab2c7f849e1764384093..76b5efbe6723cccb65581e934fd83e16040af9b8 100644 (file)
--- a/src/proof/sat_proof_implementation.h
+++ b/src/proof/sat_proof_implementation.h
@@ -1093,6 +1093,7 @@ template <class Solver>
 void LFSCSatProof<Solver>::printResolution(ClauseId id, std::ostream& out,
                                            std::ostream& paren) {
   out << "(satlem_simplify _ _ _ ";
+  paren << ")";
 
   const ResChain<Solver>& res = this->getResolutionChain(id);
   const typename ResChain<Solver>::ResSteps& steps = res.getSteps();
@@ -1118,7 +1119,7 @@ void LFSCSatProof<Solver>::printResolution(ClauseId id, std::ostream& out,
   }
 
   out << "(\\ " << this->clauseName(id) << "\n";   // bind to lemma name
-  paren << "))";                            // closing parethesis for lemma binding and satlem
+  paren << ")";
 }
 
 /// LFSCSatProof class