diff --git a/src/util/run.cpp b/src/util/run.cpp
index ee509c19ec1..6f1bb6d7127 100644
--- a/src/util/run.cpp
+++ b/src/util/run.cpp
@@ -15,22 +15,25 @@ Date: August 2012
 #else
 
 #include <cstring>
-#include <unistd.h>
 #include <cerrno>
 #include <cstdio>
 #include <cstdlib>
 
-#include <sys/wait.h>
-#include <sys/types.h>
-#include <sys/stat.h>
 #include <fcntl.h>
 #include <signal.h>
+#include <sys/stat.h>
+#include <sys/types.h>
+#include <sys/wait.h>
+#include <unistd.h>
 
 #endif
 
-#include <util/invariant.h>
-#include <util/unicode.h>
-#include <util/signal_catcher.h>
+#include <fstream>
+
+#include "invariant.h"
+#include "signal_catcher.h"
+#include "tempfile.h"
+#include "unicode.h"
 
 int run(const std::string &what, const std::vector<std::string> &argv)
 {
@@ -228,3 +231,22 @@ int run(
   }
   #endif
 }
+
+int run(
+  const std::string &what,
+  const std::vector<std::string> &argv,
+  const std::string &std_input,
+  std::ostream &std_output,
+  const std::string &std_error)
+{
+  temporary_filet tmpi("tmp.stdout", "");
+
+  int result = run(what, argv, std_input, tmpi(), std_error);
+
+  std::ifstream instream(tmpi());
+
+  if(instream)
+    std_output << instream.rdbuf(); // copy
+
+  return result;
+}
diff --git a/src/util/run.h b/src/util/run.h
index e9b02b8eeb0..60a0c0ee47f 100644
--- a/src/util/run.h
+++ b/src/util/run.h
@@ -12,6 +12,7 @@ Date: August 2012
 #ifndef CPROVER_UTIL_RUN_H
 #define CPROVER_UTIL_RUN_H
 
+#include <iosfwd>
 #include <string>
 #include <vector>
 
@@ -24,4 +25,12 @@ int run(
   const std::string &std_output,
   const std::string &std_error);
 
+/// A variant that streams the stdout of the child into an ostream
+int run(
+  const std::string &what,
+  const std::vector<std::string> &argv,
+  const std::string &std_input,
+  std::ostream &std_output,
+  const std::string &std_error);
+
 #endif // CPROVER_UTIL_RUN_H