Suggestion to improve implementation of IMC

[blishko]

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.

[AdamZsofi]

@KlevisImeri will work on this. :)

[leventeBajczi]

@KlevisImeri will you have time in the near future to continue working on this?

[KlevisImeri]

@leventeBajczi After the week of repeats (19 December 2025) I will be free and I can work for this. If it is needed a bit earlier I can try to squize some time. I looked at the code, apparently what is left is:

• Merging the new commits from master to the pull request branch
• As I remember this enhancement didn't have a very big effect but when I looked at the result we where failing at some easy verification task we where not failing before. So I concluded there are some bugs that have to be fixed.