From d0610224d0eeab12fd4f779e01b5fdd36c57b304 Mon Sep 17 00:00:00 2001
From: Andres Notzli <andres.noetzli@gmail.com>
Date: Mon, 8 Aug 2016 20:33:24 -0700
Subject: Fix missing/redundant spaces in proofs

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))`.
---
 src/proof/arith_proof.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'src/proof/arith_proof.cpp')

diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp
index 100f60600..4e813d646 100644
--- a/src/proof/arith_proof.cpp
+++ b/src/proof/arith_proof.cpp
@@ -804,9 +804,9 @@ void LFSCArithProof::printOwnedSort(Type type, std::ostream& os) {
 
   if (type.isInteger() && d_realMode) {
     // If in "real mode", don't use type Int for, e.g., equality.
-    os << "Real ";
+    os << "Real";
   } else {
-    os << type << " ";
+    os << type;
   }
 }
 
-- 
cgit v1.2.3