z3 统计中测量内存使用情况的单位是什么？是MB还是KB？
记忆到底意味着什么？是执行期间的最大内存使用量还是所有分配的总和？
它是执行期间最大堆大小的近似值，并通过 cmd_context.cpp 中的以下函数将其添加到统计对象中：
void cmd_context::display_statistics(...) {
statistics st;
...
unsigned long long mem = memory::get_max_used_memory();
...
st.update("memory", static_cast<double>(mem)/static_cast<double>(1024*1024));
...
}
因此它的单位是MB。但这只是一个近似值，因为计数器不会在每次分配时更新；请参阅 memory_manager.cpp 中的以下注释：
// We only integrate the local thread counters with the global one
// when the local counter > SYNCH_THRESHOLD
#define SYNCH_THRESHOLD 100000
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
