GC cannot collect unused AST nodes/Z3Object instances about scalaz3 HOT 2 OPEN

We tried at some point to use finalize but it turned up to be highly unreliable for our needs. We (tried to) follow instead of C# api which uses a free-buffer that should periodically be checked and cleared. We relied more on a lot of small solvers that we end up freeing manually, so this might explain why the current way has worked out better than relying on finalize for us.

I will have a look at the alternative again.

from scalaz3.

I see. What exactly do you mean, when you say that finalize turned out to be unreliable? In my application, memory consumption rises from symbolic execution to symbolic execution, although it should not. More precisely, native heap size increases continuously.

Maybe this behaviour is also caused by unreliable finalize behaviour, which does not correctly decrement reference counters.

from scalaz3.