1 files changed, 15 insertions, 11 deletions
diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp
index ac1d1d01..ddcc57a1 100644
--- a/lib/Expr/ExprPPrinter.cpp
+++ b/lib/Expr/ExprPPrinter.cpp
@@ -13,12 +13,10 @@
 #include "klee/Constraints.h"
 
 #include "llvm/Support/CommandLine.h"
+#include "llvm/Support/raw_ostream.h"
 
 #include <map>
 #include <vector>
-#include <iostream>
-#include <sstream>
-#include <iomanip>
 
 using namespace klee;
 
@@ -47,10 +45,11 @@ private:
   std::map<const UpdateNode*, unsigned> updateBindings;
   std::set< ref<Expr> > couldPrint, shouldPrint;
   std::set<const UpdateNode*> couldPrintUpdates, shouldPrintUpdates;
-  std::ostream &os;
+  llvm::raw_ostream &os;
   unsigned counter;
   unsigned updateCounter;
   bool hasScan;
+  bool forceNoLineBreaks;
   std::string newline;
 
   /// shouldPrintWidth - Predicate for whether this expression should
@@ -299,7 +298,7 @@ private:
   }
 
 public:
-  PPrinter(std::ostream &_os) : os(_os), newline("\n") {
+  PPrinter(llvm::raw_ostream &_os) : os(_os), newline("\n") {
     reset();
   }
 
@@ -307,10 +306,15 @@ public:
     newline = _newline;
   }
 
+  void setForceNoLineBreaks(bool _forceNoLineBreaks) {
+    forceNoLineBreaks = _forceNoLineBreaks;
+  }
+
   void reset() {
     counter = 0;
     updateCounter = 0;
     hasScan = false;
+    forceNoLineBreaks = false;
     bindings.clear();
     updateBindings.clear();
     couldPrint.clear();
@@ -412,7 +416,7 @@ public:
   /* Public utility functions */
 
   void printSeparator(PrintContext &PC, bool simple, unsigned indent) {
-    if (simple) {
+    if (simple || forceNoLineBreaks) {
       PC << ' ';
     } else {
       PC.breakLine(indent);
@@ -420,11 +424,11 @@ public:
   }
 };
 
-ExprPPrinter *klee::ExprPPrinter::create(std::ostream &os) {
+ExprPPrinter *klee::ExprPPrinter::create(llvm::raw_ostream &os) {
   return new PPrinter(os);
 }
 
-void ExprPPrinter::printOne(std::ostream &os,
+void ExprPPrinter::printOne(llvm::raw_ostream &os,
                             const char *message, 
                             const ref<Expr> &e) {
   PPrinter p(os);
@@ -438,7 +442,7 @@ void ExprPPrinter::printOne(std::ostream &os,
   PC.breakLine();
 }
 
-void ExprPPrinter::printSingleExpr(std::ostream &os, const ref<Expr> &e) {
+void ExprPPrinter::printSingleExpr(llvm::raw_ostream &os, const ref<Expr> &e) {
   PPrinter p(os);
   p.scan(e);
 
@@ -448,13 +452,13 @@ void ExprPPrinter::printSingleExpr(std::ostream &os, const ref<Expr> &e) {
   p.print(e, PC);
 }
 
-void ExprPPrinter::printConstraints(std::ostream &os,
+void ExprPPrinter::printConstraints(llvm::raw_ostream &os,
                                     const ConstraintManager &constraints) {
   printQuery(os, constraints, ConstantExpr::alloc(false, Expr::Bool));
 }
 
 
-void ExprPPrinter::printQuery(std::ostream &os,
+void ExprPPrinter::printQuery(llvm::raw_ostream &os,
                               const ConstraintManager &constraints,
                               const ref<Expr> &q,
                               const ref<Expr> *evalExprsBegin,