CODEWITHSUNDEEP
z3
Etienne Kneuss
Etienne Kneuss

Reputation: 108

Tracking z3 memory leaks

We are experiencing with a couple of issues related to what appears to be a memory leak. We are using contexts with ref-counting garbage collection. Here is a short description of the situation:

Through ScalaZ3 on latest unstable, we create a lot of re-counting contexts(400-500), on which we few solvers (<5), check a couple of formulas, and then delete everything. We try to del-ref everything prior to deleting the context itself. What we witness is that the memory footprint keeps increasing (up to several Gb), even though we only use 5 or 6 fresh and small contexts at a time.

1) Do Z3 free the memory of all objects within a context, when this context gets deleted? (Even those with refcount > 0 that is) If not, the reason is probably that we forgot to del-ref several objects.

2) Do you have any tool/tip that would help us track down what remains in memory. Maybe something on top of a open_log generated file? Or where to look when replaying the log under gcc?

Thanks!

Upvotes: 3

Views: 494

Answers (1)

Leonardo de Moura
Leonardo de Moura

Reputation: 21475

1) Z3 will free some of the memory when the context is deleted, but we do not have any guarantee that all memory will be deleted when the reference counters are not properly used.

2) I usually use Valgrind to track memory leaks. I think it is amazing. We can create the log of the execution in a file z3.log, and then execute

       valgrind z3 z3.log

BTW, compiling in debug mode may also help. In debug mode, Z3 will also report the list of ASTs that are still alive when the context is deleted.

Upvotes: 3

Related Questions