跟踪z3内存泄漏

Question

我们遇到了一些与似乎是内存泄漏相关的问题。我们正在使用具有重新计数垃圾收集的上下文。下面是对这种情况的简短描述：我们创建了很多重新计数的上下文（400-500），其中我们很少有求解器（< 5），检查几个公式，然后删除所有内容。我们试图在删除上下文之前删除所有内容。我们目睹的是内存占用不断增加（高达几Gb），即使我们一次只使用5或6个新鲜和小的上下文。

1）当上下文被删除时，Z3是否释放了上下文中所有对象的内存？ （即使那些refcount> 0的是）如果不是，原因可能是我们忘记了删除几个对象。

2）您是否有任何工具/提示可帮助我们追踪内存中的内容。也许是在open_log生成的文件之上的东西？或者在gcc下重播日志时看哪里？

谢谢！

Answer 1

1）当上下文被删除时，Z3将释放部分内存，但我们无法保证当引用计数器未正确使用时，所有内存都将被删除。

2）我通常使用Valgrind来跟踪内存泄漏。我认为这太棒了。我们可以创建在一个文件z3.log执行的日志，然后执行

 valgrind z3 z3.log 

顺便说一句，在调试模式下编译也可能会有帮助。在调试模式下，Z3还会报告上下文被删除时仍然存在的AST列表。