Use the partial model for formula evaluation in Princess

[daniel-raffler]

Hello,
We stopped using the partial model in Princess here as there were several solver issues when using it with rational formulas. Most of these issues have now been resolved by the Princess developers and we should look into whether it's possible to return to using the partial model in JavaSMT.

[daniel-raffler]

There is an issue in Ostrich/Princess that affects String evaluation and is blocking us from using the partial model for now. I've opened an issue here: uuverifiers/ostrich#94

[daniel-raffler]

Other than that it seems to be working fine. I've updated the Princess backend and ran some benchmarks with CPAchecker:

The timeout is 60 seconds and --option cpa.predicate.encodeFloatAs=RATIONAL was used to specifically test rational formulas as they used to cause crashes when being evaluated. The results on the left are with the current version, and the new version that uses the partial model can be found on the right. The old version produces a large number of incorrect false results that are avoided with the new code. However, these runs will still result in an Assertion error with the new version, and the message reads "Found imprecise counterexample with BMC".

The new version also returns fewer correct results, and performance seems to be slower, especially for more expensive runs:

Here the blue/green line is the old version, and the brown line is with the new version that uses the partial model. I would suggest we still update as soon as the bug is fixed as this will allow us to remove the current workaround for the partial model from our code.