diff --git a/src/util/trace.cpp b/src/util/trace.cpp
index 9571e99e6..68437ab92 100644
--- a/src/util/trace.cpp
+++ b/src/util/trace.cpp
@@ -21,7 +21,6 @@ Revision History:
 
 #ifdef _TRACE
 std::ofstream tout(".z3-trace"); 
-#endif
 
 static bool g_enable_all_trace_tags = false;
 static str_hashtable* g_enabled_trace_tags = nullptr;
@@ -56,13 +55,11 @@ bool is_trace_enabled(const char * tag) {
 }
 
 void close_trace() {
-#ifdef _TRACE
     tout.close();
-#endif
 }
 
 void open_trace() {
-#ifdef _TRACE
     tout.open(".z3-trace");
-#endif
 }
+
+#endif
diff --git a/src/util/trace.h b/src/util/trace.h
index 789beafc1..be652a620 100644
--- a/src/util/trace.h
+++ b/src/util/trace.h
@@ -33,9 +33,6 @@ Revision History:
 #ifdef _TRACE
 extern std::ofstream tout; 
 #define TRACE_CODE(CODE) { CODE } ((void) 0 )
-#else
-#define TRACE_CODE(CODE) ((void) 0)
-#endif
 
 void enable_trace(const char * tag);
 void enable_all_trace(bool flag);
@@ -48,6 +45,18 @@ void finalize_trace();
   ADD_FINALIZER('finalize_trace();')
 */
 
+#else
+#define TRACE_CODE(CODE) ((void) 0)
+
+static inline void enable_trace(const char * tag) {}
+static inline void enable_all_trace(bool flag) {}
+static inline void disable_trace(const char * tag) {}
+static inline bool is_trace_enabled(const char * tag) {}
+static inline void close_trace() {}
+static inline void open_trace() {}
+static inline void finalize_trace() {}
+#endif
+
 #define TRACE(TAG, CODE) TRACE_CODE(if (is_trace_enabled(TAG)) { tout << "-------- [" << TAG << "] " << __FUNCTION__ << " " << __FILE__ << ":" << __LINE__ << " ---------\n"; CODE tout << "------------------------------------------------\n"; tout.flush(); })
 
 #define STRACE(TAG, CODE) TRACE_CODE(if (is_trace_enabled(TAG)) { CODE tout.flush(); })
@@ -55,4 +64,3 @@ void finalize_trace();
 #define CTRACE(TAG, COND, CODE) TRACE_CODE(if (is_trace_enabled(TAG) && (COND)) { tout << "-------- [" << TAG << "] " << __FUNCTION__ << " " << __FILE__ << ":" << __LINE__ << " ---------\n"; CODE tout << "------------------------------------------------\n"; tout.flush(); })
 
 #endif /* TRACE_H_ */
-