cvc4terminate infinite loop fix

diff --git a/src/main/util.cpp b/src/main/util.cpp
index 5819028daa2172ddd78542d04e29812f46a55034..3b7c6b95a93dcc74a193a90d6a5a268af7c6dac1 100644 (file)
--- a/src/main/util.cpp
+++ b/src/main/util.cpp
@@ -199,6 +199,7 @@ void cvc4unexpected() {
 }
 
 void cvc4terminate() {
+  set_terminate(default_terminator);
 #ifdef CVC4_DEBUG
   fprintf(stderr, "\n"
           "CVC4 was terminated by the C++ runtime.\n"