Baier D.

So the problem is in [line 220](https://github.com/sosy-lab/java-smt/blob/master/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java#L220) in the `SmtInterpolAbstractProver`. I can not tell what the underlying problem is at this moment however. Removing this line avoids the error and...

>> So the problem is in [line 220](https://github.com/sosy-lab/java-smt/blob/master/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java#L220) in the SmtInterpolAbstractProver. I can not tell what the underlying problem is at this moment however. Removing this line avoids the error...

I fixed it using the proper cleanup API of SMTInterpol in 72b06914cf9bd126930d32d37161a8895683abba. I also tested this with CPAchecker and it works fine now. @daniel-raffler if you want to find a...

@leventeBajczi could you spare a look at this PR and maybe give us some feedback on the current proof interface?

> > Good work in cleaning up the classes! > > I added a MathSAT5 native test for the proof generation option and it seems that there is no problem...

Note: this is hard to pin down currently. Also, these model_iterator problems occur regularly (but not at an alarming rate). Would it be helpful to actually catch this exception and...

Thank you both for your input! I guess it's best to wrap the error in an `SolverException` and possibly add our information about the problem to the description. I will...

This is a very similar issue to the tainted environment we encountered when continuing after some interpolation errors in 2022 [here](https://gitlab.com/sosy-lab/software/cpachecker/-/issues/998#note_1017902431)! 2 Things we should do: - Find the initial...

Good work! Maybe you want to open a MR to add this debug delegate? ;D Seems helpful.

When i created the Maven example i also tried to build an example with FAT-Jars and found it to be rather hard with the way we load libs. (In some...