From c82514b57252444df982b35af4809e0fd4635e37 Mon Sep 17 00:00:00 2001
From: Guy <katz911@gmail.com>
Date: Wed, 3 Aug 2016 15:51:22 -0700
Subject: [PATCH] Fixed an issue where arrays proofs would sometimes have an
 extra ")" at the end.

---
 src/proof/array_proof.cpp            |  4 ++--
 src/proof/proof_manager.cpp          | 13 +++++--------
 src/proof/sat_proof_implementation.h |  3 ++-
 3 files changed, 9 insertions(+), 11 deletions(-)

diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp
index ccc072eca..514d81184 100644
--- 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 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,
diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h
index fc2bae19b..76b5efbe6 100644
--- 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
-- 
2.30.2