diff --git a/src/util/memory_manager.cpp b/src/util/memory_manager.cpp
index 5f56ded98..354a11aeb 100644
--- a/src/util/memory_manager.cpp
+++ b/src/util/memory_manager.cpp
@@ -173,6 +173,7 @@ void memory::display_i_max_usage(std::ostream & os) {
               << "\n";
 }
 
+#if _DEBUG
 void memory::deallocate(char const * file, int line, void * p) {
     deallocate(p);
     TRACE_CODE(if (!g_finalizing) TRACE("memory", tout << "dealloc " << std::hex << p << std::dec << " " << file << ":" << line << "\n";););
@@ -183,6 +184,7 @@ void * memory::allocate(char const* file, int line, char const* obj, size_t s) {
     TRACE("memory", tout << "alloc " << std::hex << r << std::dec << " " << file << ":" << line << " " << obj << " " << s << "\n";);
     return r;
 }
+#endif
 
 #if defined(_WINDOWS) || defined(_USE_THREAD_LOCAL)
 // ==================================
diff --git a/src/util/memory_manager.h b/src/util/memory_manager.h
index 2cabc70b7..f1ce37ca6 100644
--- a/src/util/memory_manager.h
+++ b/src/util/memory_manager.h
@@ -23,6 +23,24 @@ Revision History:
 #include<ostream>
 #include"z3_exception.h"
 
+#ifndef __has_builtin
+# define __has_builtin(x) 0
+#endif
+
+#ifdef __GNUC__
+# if (__GNUC__ * 100 + __GNUC_MINOR__) >= 409 || __has_builtin(returns_nonnull)
+#  define GCC_RET_NON_NULL __attribute__((returns_nonnull))
+# else
+#  define GCC_RET_NON_NULL
+# endif
+# define ALLOC_ATTR __attribute__((malloc)) GCC_RET_NON_NULL
+#elif defined(_WINDOWS)
+# define ALLOC_ATTR __declspec(restrict)
+#else
+# define ALLOC_ATTR
+#endif
+
+
 class out_of_memory_error : public z3_error {
 public:
     out_of_memory_error();
@@ -39,9 +57,11 @@ public:
     static void display_max_usage(std::ostream& os);
     static void display_i_max_usage(std::ostream& os);
     static void deallocate(void* p);
-    static void* allocate(size_t s);
+    static void* allocate(size_t s) ALLOC_ATTR;
+#if _DEBUG
     static void deallocate(char const* file, int line, void* p);
-    static void* allocate(char const* file, int line, char const* obj, size_t s);
+    static void* allocate(char const* file, int line, char const* obj, size_t s) ALLOC_ATTR;
+#endif
     static unsigned long long get_allocation_size();
     static unsigned long long get_max_used_memory();
     // temporary hack to avoid out-of-memory crash in z3.exe
@@ -74,6 +94,9 @@ void dealloc(T * ptr) {
 
 #endif
 
+template<typename T>
+T * alloc_vect(unsigned sz) ALLOC_ATTR;
+
 template<typename T>
 T * alloc_vect(unsigned sz) {
     T * r = static_cast<T*>(memory::allocate(sizeof(T) * sz));