In the inner loop of IMC
Theta uses the same solver both for checking reachability and for checking fixedpoint.
Because of this, everything is popped from the solver in preparation for the next check.
This is unfortunate because the solver cannot take any advantage of the incremental nature of the checks.

I believe it would be more efficient to have two dedicated solvers.
An interpolating solver that checks reachability and a non-interpolating solver that checks fixedpoint.
The only obstacle there is that the interpolant computed by the first solver must be added to the second solver.
I don't know how difficult this is to do in Theta.
Usually, it is possible to have a single context (like a term manager) and multiple solver instances operated over the same context.