CPAChecker regressions when Princess is used

[daniel-raffler]

Hello,
as reported here a recent update from JavaSMT 5.0.1 to version 5.0.1-723-g57d7e4ab4 in CPAChecker has introduced a few new exceptions when Princess is used. The issue can be triggered by running:

bin/cpachecker --heap 13000M --stack 50M --no-output-files --option cpa.predicate.memoryAllocationsAlwaysSucceed=true --predicateAnalysis --option cpa.predicate.encodeFloatAs=INTEGER --option cpa.predicate.encodeBitvectorAs=INTEGER --option solver.solver=princess --timelimit 60s --stats --spec test/programs/benchmarks/properties/unreach-call.prp --32 test/programs/benchmarks/array-fpi/s1iff.c

and the full error message is as follows:

Error: Refinement failed: Interpolation failed in solver PRINCESS with message 'Internal exception: java.lang.ClassCastException: class ap.proof.ModelSearchProver$UnsatResult$ cannot be cast to class ap.proof.ModelSearchProver$ModelResult (ap.proof.ModelSearchProver$UnsatResult$ and ap.proof.ModelSearchProver$ModelResult are in unnamed module of loader 'app')'. (RefinementFailedException.forInterpolationFailureInSolver, SEVERE)

This appears to be a bug in Princess and we should report it to the developers. The Princess version before the update was Princess 2024-01-12 and the new version uses Princess 2025-06-25. When the partial model is used the crash disappears, so the problem may be linked to our work-around