Fix missing/redundant spaces in proofsfix_proof_spaces

Before, in some cases, e.g. when printing sorts and in resolution
proofs, the proofs contained redundant and/or missing spaces. With this
commit, CVC4 now prints out `(trust_f (= (Array Index Element) let10
let12)` instead of `(trust_f (= (Array Index  Element )let10 let12))`.

1 files changed, 7 insertions, 7 deletions

diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h
index 76b5efbe6..603559da1 100644
--- a/src/proof/sat_proof_implementation.h
+++ b/src/proof/sat_proof_implementation.h
@@ -1092,33 +1092,33 @@ TSatProof<Solver>::Statistics::~Statistics() {
 template <class Solver>
 void LFSCSatProof<Solver>::printResolution(ClauseId id, std::ostream& out,
                                            std::ostream& paren) {
-  out << "(satlem_simplify _ _ _ ";
+  out << "(satlem_simplify _ _ _";
   paren << ")";
 
   const ResChain<Solver>& res = this->getResolutionChain(id);
   const typename ResChain<Solver>::ResSteps& steps = res.getSteps();
 
   for (int i = steps.size() - 1; i >= 0; i--) {
-    out << "(";
-    out << (steps[i].sign ? "R" : "Q") << " _ _ ";
+    out << " (";
+    out << (steps[i].sign ? "R" : "Q") << " _ _";
   }
 
   ClauseId start_id = res.getStart();
-  out << this->clauseName(start_id) << " ";
+  out << " " << this->clauseName(start_id);
 
   for (unsigned i = 0; i < steps.size(); i++) {
     prop::SatVariable v =
         prop::MinisatSatSolver::toSatVariable(var(steps[i].lit));
-    out << this->clauseName(steps[i].id) << " "
+    out << " " << this->clauseName(steps[i].id) << " "
         << ProofManager::getVarName(v, this->d_name) << ")";
   }
 
   if (id == this->d_emptyClauseId) {
-    out <<"(\\ empty empty)";
+    out <<" (\\ empty empty)";
     return;
   }
 
-  out << "(\\ " << this->clauseName(id) << "\n";   // bind to lemma name
+  out << " (\\ " << this->clauseName(id) << "\n";   // bind to lemma name
   paren << ")";
 }