3 files changed, 7 insertions, 19 deletions
diff --git a/include/klee/Internal/Module/KInstruction.h b/include/klee/Internal/Module/KInstruction.h
index 98e4e3d0..a81e8d8f 100644
--- a/include/klee/Internal/Module/KInstruction.h
+++ b/include/klee/Internal/Module/KInstruction.h
@@ -44,7 +44,6 @@ namespace klee {
 
   public:
     virtual ~KInstruction();
-    void printFileLine(llvm::raw_ostream &) const;
     std::string printFileLine() const;
 
   };
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 308b4456..03ac1331 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -1153,9 +1153,7 @@ void Executor::printDebugInstructions(ExecutionState &state) {
 
   if (!DebugPrintInstructions.isSet(STDERR_COMPACT) &&
       !DebugPrintInstructions.isSet(FILE_COMPACT)) {
-    (*stream) << "     ";
-    state.pc->printFileLine(*stream);
-    (*stream) << ":";
+    (*stream) << "     " << state.pc->printFileLine() << ":";
   }
 
   (*stream) << state.pc->info->assemblyLine;
@@ -3080,10 +3078,9 @@ void Executor::callExternalFunction(ExecutionState &state,
     for (unsigned i=0; i<arguments.size(); i++) {
       os << arguments[i];
       if (i != arguments.size()-1)
-	os << ", ";
+        os << ", ";
     }
-    os << ") at ";
-    state.pc->printFileLine(os);
+    os << ") at " << state.pc->printFileLine();
     
     if (AllExternalWarnings)
       klee_warning("%s", os.str().c_str());
diff --git a/lib/Module/KInstruction.cpp b/lib/Module/KInstruction.cpp
index d1e6c470..c7c841a4 100644
--- a/lib/Module/KInstruction.cpp
+++ b/lib/Module/KInstruction.cpp
@@ -8,7 +8,6 @@
 //===----------------------------------------------------------------------===//
 
 #include "klee/Internal/Module/KInstruction.h"
-#include "llvm/Support/raw_ostream.h"
 #include <string>
 
 using namespace llvm;
@@ -20,15 +19,8 @@ KInstruction::~KInstruction() {
   delete[] operands;
 }
 
-void KInstruction::printFileLine(llvm::raw_ostream &debugFile) const {
-  if (info->file != "")
-    debugFile << info->file << ":" << info->line;
-  else debugFile << "[no debug info]";
-}
-
-std::string KInstruction::printFileLine() const {
-  std::string str;
-  llvm::raw_string_ostream oss(str);
-  printFileLine(oss);
-  return oss.str();
+std::string KInstruction::getSourceLocation() const {
+  if (!info->file.empty())
+    return info->file + ":" + std::to_string(info->line);
+  else return "[no debug info]";
 }