Z3 Java API: when to dispose expressions / Z3 objects?

Question

In my Java code, I'm invoking Z3 in a loop to check a formula (which depends on the loop index and is different for every iteration) until the formula becomes satisfiable, as sketched in the following pseudo code fragment:

int n = 0;
do {
    n += 1;

    Context ctx = new Context();
    Solver solver = ctx.mkSolver();

    // Construct large formula b(n) (depending on n)
    // with a lot of Boolean subexpressions
    BoolExpr b = ... 
    solver.add(b);

    Status result = solver.check();

    solver.dispose();
    ctx.dispose();

    if (result == Status.SATISFIABLE) {
         break;
    }

} while (true);

However, I'm quickly running into memory issues (i.e., a Z3Exception with message "out of memory" is thrown), and I feel that I'm probably not correctly disposing the created Z3Objects.

Since I did not find information of this (i just found Z3 Java API documentation or tutorial and Performance issues about Z3 for Java), my questions are:

1. When calling solver.dispose(), are all contained BoolExpr disposed as well or do I need to remember them somewhere and call .dispose() on any of them?
2. Would it be more performant to move the creation and disposal of the context and solver out of the loop and instead use solver.push() and solver.pop() inside the loop?
3. What other Z3Objects should I dispose "manually" in the given case?

Answer 1

When a Z3Exception with the "out of memory" message is thrown, it means that the native libz3.dll ran out of memory. Disposing both solver and context in every loop iteration is really the best that can be done (a few things still stay in memory, e.g., symbols). Note however that the Solver and Context objects look like tiny objects to the garbage collector (they are just a pointer and Java can't see what's behind the pointer). So, the first thing to try is to add a call to System.gc() in the hope that all Z3 objects will actually get collected at that point. Also, I seem to recall that the Java virtual machine has a default memory limit that is smaller than one would expect, but they can be set by the -Xms and -Xmx options.