[chore] stabilise SMT and bump provers

[fdupress]

@EasyCrypt/developers I need quick eyes on this, and for you to tell me how much of a pain in the arse it is to bump z3 to 4.16 and cvc5 to 1.1.x as a requirement for easycrypt dev.

I use arch (btw), so my own setup can follow SMT solvers relatively closely, but I recognise that not everybody likes to spend their weekend fixing their bootloader...

As a side note, most of the proof breakage is in places where the solver would need to recall that witness exists in all types, and to instantiate a universal quantification with it for the sake of a proof. I assume that both z3 and cvc5 have made a move towards more "constructive-compatible" heuristics in places, as they work to better integrate with ITPs.

[namasikanam]

As a side note, most of the proof breakage is in places where the solver would need to recall that witness exists in all types, and to instantiate a universal quantification with it for the sake of a proof. I assume that both z3 and cvc5 have made a move towards more "constructive-compatible" heuristics in places, as they work to better integrate with ITPs.

Just for my understanding, upgrading z3 and cvc5 makes their capability worse on dealing with witness?

[fdupress]

One of our two provers is such that the version we used in CI before this PR had no issue proving "(forall x, A x) => (forall x, A x => B) => B" whereas its new version stalls on it, or at least on instances of it that requires pulling witness out of a hat because there is no other x in context.

I won't try and speculate as to why this prover lost that capability. I will simply note in passing that the formula above is true only if types cannot be empty.