slow processing of large file
ada__model.mlw ada___skp__events.mlw _gnatprove_standard.mlw _gnatprove_standard_th.why ada__model_th.why
Dear Why3 team,
the attached file ada___skp__events.mlw
(support files also attached) is very slow to be processed by Why3. Just doing a split_goal_right
on the main task takes roughly one minute ...
For the background, this comes from Ada code which contains a large array constant, where each field is a record, which contains arrays, which contain .... There are also predicates on several of the substructures, which have to be proved for the constant. Overall, the Ada constant spans 5000 lines.
While the why3 translation joined here is certainly not optimal, it doesn't look too bad given the above. However it seems that why3 gets slower and slower the more fields are added to the array.
Is there anything that we can do to make things easier for why3, or is there some obvious performance issue somewhere?
Thank you in advance