From 7f8a7c3d83011dd1d0571b2c4d954b3434f60901 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 14 Oct 2017 11:59:09 -0700
Subject: [PATCH] fix the fixme of #1307

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/test/main.cpp | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/src/test/main.cpp b/src/test/main.cpp
index cdc06404c..98be722e3 100644
--- a/src/test/main.cpp
+++ b/src/test/main.cpp
@@ -10,9 +10,7 @@
 #include "util/memory_manager.h"
 #include "util/gparams.h"
 
-static void tst_exit_all_tests() {
-    exit(0);
-}
+
 //
 // Unit tests fail by asserting.
 // If they return, we assume the unit test succeeds
@@ -210,7 +208,7 @@ int main(int argc, char ** argv) {
     TST(prime_generator);
     TST(permutation);
     TST(nlsat);
-    TST(exit_all_tests);
+    if (test_all) return 0;
     TST(ext_numeral);
     TST(interval);
     TST(f2n);