The param MEMORY_HIGH_WATERMARK is disabled on Linux with the comment:
// The non-windows memory manager does not have access to memory sizes.

After inspecting src/util/memory_manager.cpp, I believe this comment may no longer apply.

Is there still a reason not to enable this feature for non-Windows builds?

Suggested patch:
diff --git a/src/front_end_params/front_end_params.cpp b/src/front_end_params/front_end_params.cpp
index 2dc037e..7a43b83 100644
--- a/src/front_end_params/front_end_params.cpp
+++ b/src/front_end_params/front_end_params.cpp
@@ -49,13 +49,10 @@ void front_end_params::register_params(ini_params & p) {
     p.register_bool_param("ASYNC_COMMANDS", m_async_commands, "enable/disable support for asynchronous commands in the Simplify front-end.");
     p.register_bool_param("DISPLAY_CONFIG", m_display_config, "display configuration used by Z3");
-#ifdef _WINDOWS
-    // The non-windows memory manager does not have access to memory sizes.
     p.register_unsigned_param("MEMORY_HIGH_WATERMARK", m_memory_high_watermark, 
                               "set high watermark for memory consumption (in megabytes)");
     p.register_unsigned_param("MEMORY_MAX_SIZE", m_memory_max_size,
                               "set hard upper limit for memory consumption (in megabytes)");
     // external users should not have access to it.
Closed Mar 25, 2013 at 5:33 PM by leodemoura
Thanks for reporting this issue. It affects the master (official release) branch, but it is not an issue in the unstable (work-in-progress) branch.


leodemoura wrote Mar 25, 2013 at 5:32 PM

This issue has been fixed in the unstable (work-in-progress) branch.
The modifications in the unstable branch will be available in the next release.
In the meantime, you can build this branch, or use one of the available nightly builds.
The nightly builds are not official releases, and are built using the unstable branch.
For more information about nightly builds: