[issue984] Exit more gracefully when running out of memory.

We no longer try to clean up the program state when running out of memory.

src/search/planner.cc

@@ -46,6 +46,5 @@ int main(int argc, const char **argv) {
     ExitCode exitcode = search_algorithm->found_solution()
         ? ExitCode::SUCCESS
         : ExitCode::SEARCH_UNSOLVED_INCOMPLETE;
-    utils::report_exit_code_reentrant(exitcode);
-    return static_cast<int>(exitcode);
+    exit_with(exitcode);
 }

src/search/utils/system.cc

@@ -49,11 +49,9 @@ void exit_with(ExitCode exitcode) {
     exit(static_cast<int>(exitcode));
 }
 
-void exit_after_receiving_signal(ExitCode exitcode) {
-    /*
-      In signal handlers, we have to use the "safe function" _Exit() rather
-      than the unsafe function exit().
-    */
+void exit_with_reentrant(ExitCode exitcode) {
+    /* In signal handlers or when we run out of memory, we have to use the
+       "safe function" _Exit() rather than the unsafe function exit(). */
     report_exit_code_reentrant(exitcode);
     _Exit(static_cast<int>(exitcode));
 }

src/search/utils/system.h

@@ -54,7 +54,7 @@ enum class ExitCode {
 };
 
 NO_RETURN extern void exit_with(ExitCode returncode);
-NO_RETURN extern void exit_after_receiving_signal(ExitCode returncode);
+NO_RETURN extern void exit_with_reentrant(ExitCode returncode);
 
 int get_peak_memory_in_kb();
 const char *get_exit_code_message_reentrant(ExitCode exitcode);

src/search/utils/system_unix.cc

@@ -164,7 +164,7 @@ static void out_of_memory_handler() {
       memory for the stack of the signal handler and raising a signal here.
     */
     write_reentrant_str(STDOUT_FILENO, "Failed to allocate memory.\n");
-    exit_with(ExitCode::SEARCH_OUT_OF_MEMORY);
+    exit_with_reentrant(ExitCode::SEARCH_OUT_OF_MEMORY);
 }
 
 static void signal_handler(int signal_number) {
@@ -173,7 +173,7 @@ static void signal_handler(int signal_number) {
     write_reentrant_int(STDOUT_FILENO, signal_number);
     write_reentrant_str(STDOUT_FILENO, " -- exiting\n");
     if (signal_number == SIGXCPU) {
-        exit_after_receiving_signal(ExitCode::SEARCH_OUT_OF_TIME);
+        exit_with_reentrant(ExitCode::SEARCH_OUT_OF_TIME);
     }
     raise(signal_number);
 }

src/search/utils/system_windows.cc

@@ -15,7 +15,7 @@ using namespace std;
 namespace utils {
 void out_of_memory_handler() {
     cout << "Failed to allocate memory." << endl;
-    exit_with(ExitCode::SEARCH_OUT_OF_MEMORY);
+    exit_with_reentrant(ExitCode::SEARCH_OUT_OF_MEMORY);
 }
 
 void signal_handler(int signal_number) {