Proof performance regressions from 2.4.0 to 2.4.1+

[AllanBlanchard]

I found a bunch of regressions while migrating my tutorial about C program proofs with Frama-C from Alt-Ergo 2.4.0 to 2.4.1 (the same happens with the master branch). They seem to be related to:

• the length of the formulas (number of variables and/or hypotheses?)
• the instantiation of lemmas

The following archive regressions.zip contains 3 examples, each of them containing several proofs obligations. It provides the original C file (that we try to verify with Frama-C), the generated Why3 proof goals that I have cleaned so that only the important part for the proof is kept, the generated alt-ergo files (some of them have been reorganized to that they can be easily compared) and the results of the verification for Alt-Ergo 2.4.0, 2.4.1 and master branch.

These issues are not critical, but as some of them are related to exercises that target beginners, it might be hard for them to understand what happens and why their proofs do not succeed while it could because all required information is here.

[Stevendeo]

It seems Alt-Ergo tries to transform its terms (+ a (+ b c)) into (+ a b c), which makes it somehow fail to deduce something (expr.ml, make_term, see https://github.com/OCamlPro/alt-ergo/pull/432) . While a quick fix is easy to write, I will investigate the reason of the regression as (+ a (+ b c)) and (+ a b c) should be equivalent.

[AllanBlanchard]

Thank you for this first patch! It indeed fixes all the regressions I have found (including another one that I found but was very similar to the examples facto and sum).

I have also two POs that were not proved with 2.4.0, are proved with 2.4.1 and are not proved anymore with #507 . I did not really expected to see these POs proved automatically (the reasoning to get them is not so direct) so on my side this is not a problem if they are not proved. But since you want to investigate on the reason of the regression, opposite examples might be useful : improved.zip.