From 8d3dfd36b22670c1fc35c0f5295387988eba04bd Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 12 Jun 2019 02:37:24 -0700
Subject: [PATCH] initialize/finalize cooperate at top-level

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/util/cooperate.h | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

diff --git a/src/util/cooperate.h b/src/util/cooperate.h
index 7d58d947d..a8cb7e8e8 100644
--- a/src/util/cooperate.h
+++ b/src/util/cooperate.h
@@ -34,11 +34,17 @@ inline void cooperate(char const * task) {
 void initialize_cooperate();
 void finalize_cooperate();
 
+#else
+inline void cooperate(char const *) {}
+inline void initialize_cooperate() {}
+inline void finalize_cooperate() {}
+
+#endif
+
+
 /*
   ADD_INITIALIZER('initialize_cooperate();')
   ADD_FINALIZER('finalize_cooperate();')
 */
 
-#else
-inline void cooperate(char const *) {}
-#endif
+