Run tests using why3find

[Lysxia]

Sequel to #1205

Run tests with why3find by default.

Some test cases must still be run with why3 because they use ad hoc transformations, they are indicated by a new header WHY3PROVE.

There is one test case that requires inline_goal (iterators/10_once.rs), enabled with the header TACTIC +inline_goal.

[Lysxia]

There is still a detail I need to figure out about how why3find records prover times. I asked about it on the why3find issue tracker: https://git.frama-c.com/pub/why3find/-/issues/117

[jhjourdan]

We should update .gitattribute in order to not show diffs of the json files, just as is already done for xml files.

[jhjourdan]

Also, now that we are using Why3find, which is supposed to be more stable than why3 wrt. proof replay failure, would it be relevant to remove the "UNSTABLE" annotation of some tests? (Recall: this annotation tells CI to skip these tests, because they are too unstable.)

@xldenis ; anything to say?

[xldenis]

I would love to remove that annotation if it does become more stable!