Update proofs to new why3

[xldenis]

Why3 updated making all our proofs obsolete.

I also took advantage of to try and clean up our Z3 and CVC versions, but I've noticed two major problems:

• 874 sees a ~100x regression going from 0.06s with z3 4.11.2 to 9s with z3 4.12.2, this seems weird.
• 03_std_iterators has one loop invariant which only proves with CVC4 1.8 I can't figure out why.

[jhjourdan]

I'll have a look, but I'm not surprised. I've just merged this: https://gitlab.inria.fr/why3/why3/-/merge_requests/830, which is usually better than the previous behavior, but can have a big impact on proof automation.

[xldenis]

I'll have a look, but I'm not surprised

It might also be related to the prover upgrades; the failing proofs all involved proof goals where I didn't use the original proof goal as well.

[xldenis]

note: we need to update CI

[jhjourdan]

874 sees a ~100x regression going from 0.06s with z3 4.11.2 to 9s with z3 4.12.2, this seems weird.

At least for this one, I observe comparable execution times for both versions of Z3. It just seems that the Why3 changes made triggers not instantiate quantifiers the right way here...

[jhjourdan]

Well, actually, I'm not able to prove the goal at all with Z3 4.11.2...

[jhjourdan]

03_std_iterators has one loop invariant which only proves with CVC4 1.8 I can't figure out why.

For this one, I can make the proof pass with CVC5 by unfolding the predicate.

But do we want to forbid CVC4? What's the point?

[xldenis]

But do we want to forbid CVC4? What's the point?

I'd like to yes, at least in our CI; it keeps things simpler, I don't want to keep CVC4 around for a single goal.

[xldenis]

I can't figure out how to fix heapsort_generic, one invariant is broken. If anyone can figure out the missing assertion that would be greatly appreciated