From ce4ba524301ee3a8a297b2c3050e7d2c5ee58d08 Mon Sep 17 00:00:00 2001
From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Thu, 14 Jun 2012 17:06:14 +0000
Subject: restore destruction of stuff in driver

---
 src/main/driver.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src/main')

diff --git a/src/main/driver.cpp b/src/main/driver.cpp
index 36840f28e..00072d6d9 100644
--- a/src/main/driver.cpp
+++ b/src/main/driver.cpp
@@ -326,7 +326,7 @@ int runCvc4(int argc, char* argv[], Options& options) {
     pStatistics->flushInformation(*options.err);
   }
 
-  exit(returnValue);
+  return returnValue;
 }
 
 /** Executes a command. Deletes the command after execution. */
-- 
cgit v1.2.3