about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
-rw-r--r--tools/klee/main.cpp4
1 files changed, 2 insertions, 2 deletions
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index 2b7310ec..c3188259 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -353,9 +353,9 @@ std::ostream *KleeHandler::openOutputFile(const std::string &filename) {
   std::string path = getOutputFilename(filename);
   f = new std::ofstream(path.c_str(), io_mode);
   if (!f) {
-    klee_warning("out of memory");
+    klee_error("error opening file \"%s\" (out of memory)", filename.c_str());
   } else if (!f->good()) {
-    klee_warning("error opening: %s", filename.c_str());
+    klee_error("error opening file \"%s\".  KLEE may have run out of file descriptors: try to increase the maximum number of open file descriptors by using ulimit.", filename.c_str());
     delete f;
     f = NULL;
   }