diff --git a/src/util/run.cpp b/src/util/run.cpp
index ee509c19ec1..3fff91591c9 100644
--- a/src/util/run.cpp
+++ b/src/util/run.cpp
@@ -181,6 +181,9 @@ int run(
     }
     else /* fork() returns new pid to the parent process */
     {
+      // must do before resuming signals to avoid race
+      register_child(childpid);
+
       // resume signals
       sigprocmask(SIG_SETMASK, &old_mask, nullptr);
 
@@ -188,10 +191,13 @@ int run(
 
       /* wait for child to exit, and store its status */
       while(waitpid(childpid, &status, 0)==-1)
+      {
         if(errno==EINTR)
           continue; // try again
         else
         {
+          unregister_child();
+
           perror("Waiting for child process failed");
           if(stdin_fd!=STDIN_FILENO)
             close(stdin_fd);
@@ -201,6 +207,9 @@ int run(
             close(stderr_fd);
           return 1;
         }
+      }
+
+      unregister_child();
 
       if(stdin_fd!=STDIN_FILENO)
         close(stdin_fd);
diff --git a/src/util/signal_catcher.cpp b/src/util/signal_catcher.cpp
index 8d25e275e77..80422e55fd1 100644
--- a/src/util/signal_catcher.cpp
+++ b/src/util/signal_catcher.cpp
@@ -9,72 +9,81 @@ Author: Daniel Kroening, kroening@kroening.com
 \*******************************************************************/
 
 #include "signal_catcher.h"
+#include "invariant.h"
 
 #if defined(_WIN32)
-#include <process.h>
 #else
 #include <cstdlib>
-#include <csignal>
 #endif
 
-#include <vector>
-
 // Here we have an instance of an ugly global object.
 // It keeps track of any child processes that we'll kill
-// when we are told to terminate.
+// when we are told to terminate. "No child" is indicated by '0'.
 
 #ifdef _WIN32
 #else
-std::vector<pid_t> pids_of_children;
+pid_t child_pid = 0;
+
+void register_child(pid_t pid)
+{
+  PRECONDITION(child_pid == 0);
+  child_pid = pid;
+}
+
+void unregister_child()
+{
+  PRECONDITION(child_pid != 0);
+  child_pid = 0;
+}
 #endif
 
 void install_signal_catcher()
 {
-  #if defined(_WIN32)
-  #else
+#if defined(_WIN32)
+#else
   // declare act to deal with action on signal set
   // NOLINTNEXTLINE(readability/identifiers)
   static struct sigaction act;
 
-  act.sa_handler=signal_catcher;
-  act.sa_flags=0;
+  act.sa_handler = signal_catcher;
+  act.sa_flags = 0;
   sigfillset(&(act.sa_mask));
 
   // install signal handler
   sigaction(SIGTERM, &act, nullptr);
-  #endif
+#endif
 }
 
 void remove_signal_catcher()
 {
-  #if defined(_WIN32)
-  #else
+#if defined(_WIN32)
+#else
   // declare act to deal with action on signal set
   // NOLINTNEXTLINE(readability/identifiers)
   static struct sigaction act;
 
-  act.sa_handler=SIG_DFL;
-  act.sa_flags=0;
+  act.sa_handler = SIG_DFL;
+  act.sa_flags = 0;
   sigfillset(&(act.sa_mask));
 
   sigaction(SIGTERM, &act, nullptr);
-  #endif
+#endif
 }
 
 void signal_catcher(int sig)
 {
-  #if defined(_WIN32)
-  #else
+#if defined(_WIN32)
+#else
 
-  #if 1
+#if 0
   // kill any children by killing group
   killpg(0, sig);
-  #else
-  // pass on to any children
-  for(const auto &pid : pids_of_children)
-    kill(pid, sig);
-  #endif
+#else
+  // pass on to our child, if any
+  if(child_pid != 0)
+    kill(child_pid, sig);
+#endif
 
   exit(sig); // should contemplate something from sysexits.h
-  #endif
+#endif
 }
diff --git a/src/util/signal_catcher.h b/src/util/signal_catcher.h
index 399e6bb960e..c7c6faaeb19 100644
--- a/src/util/signal_catcher.h
+++ b/src/util/signal_catcher.h
@@ -14,4 +14,10 @@ void install_signal_catcher();
 void remove_signal_catcher();
 void signal_catcher(int sig);
 
+#ifndef _WIN32
+#include <csignal>
+void register_child(pid_t);
+void unregister_child();
+#endif
+
 #endif // CPROVER_UTIL_SIGNAL_CATCHER_H