From c44344c041ef50991d0e212ec23faf8febc8c805 Mon Sep 17 00:00:00 2001
From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Thu, 18 Sep 2014 16:39:33 -0400
Subject: [PATCH] cvc4terminate infinite loop fix

---
 src/main/util.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/main/util.cpp b/src/main/util.cpp
index 5819028da..3b7c6b95a 100644
--- 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"
-- 
2.30.2