Regression with JavaSMT 3.1.0 and SMTInterpol
WIth the latest update of JavaSMT and SMTInterpol, several analyses produce exceptions or run into timeout. We need to investigate this and find a solution.
Most problems come from SMTInterpol when using LassoRanker in termination analysis. This needs to get fixed. For the ldv-analysis, some tasks switched from RESULT to TIMEOUT or vice versa. This is a regression, but the effect is not that bad.
The last wanted solution is to revert JavaSMT. Reporting the problems to SMTInterpol or finding a direct solution would be prefered.
BuildBot tables are available for termination analysis and ldv analysis.