Various updates in preparation for Z3 version update

[marcoeilers]

We might want to update our used Z3 version from 4.8.7 to 4.16.0 soon. This version leads to some issues with the current version of Carbon, which I'm trying to address in this PR:

• Doing several asserts related to quantified permissions that we emit without triggers inside their own if (*) { ... assume false } block, to prevent them from being triggered in subsequent assertions.
• Dropping some Z3 flags
• Rewriting the axiom that states that for predicate P(x, y), P(x1, y1) == P(x2, y2) ==> x1 == x2 && y1 == y2 to one that uses getter functions for each parameter and therefore should not be multiplicative in the same way
• Some small changes to sequence axioms
• Introducing a timeout in the standard test suite

[alexanderjsummers]

Most of my comments are out-of-interest; the minor fix to the one axiom seems worth doing now

[alexanderjsummers]

I assume this option has gone? Not sure what it did, to be honest

[marcoeilers]

It still exists, and the other removed ones also still exist IIRC.
The changes align our options with the ones Dafny uses (https://github.com/dafny-lang/dafny/blob/f3c2fedfb2b88272af5b64f5e45d803a3bc0043a/docs/DafnyRef/UserGuide.md?plain=1#L2751), which is also on the Z3 version we want to move to (4.16.0). My impression was that we at some point basically just copied the options Dafny used back then, so if they've switched things up, we probably should as well.
I believe this improved performance or completeness with newer Z3, but I'll recheck.

[marcoeilers]

I checked, and the options change essentially makes no difference for performance or completeness, neither with old Z3 4.8.7 nor with new Z3 4.16.0. I still think we should make the change, since it would re-align the options we use in Silicon and Carbon, and those with Dafny as well.

[marcoeilers]

The changes do have some consequences independent of the Z3 version: Since more asserts are wrapped into if (*) { ...; assume false }, these asserts are not visible to the following code (that's the whole point). As a result, if these asserts fail, the rest of the code is verified without the assumption that the failed asserts holds, which we'd get in current Carbon. So we get a few more repeated errors than we currently do.

IMO this is worth it, since any later error that is currently hidden by some asserted-assumed-quantifier for which we don't have good triggers is also a potential performance problem. Any other solution to the same problem that I can think of (like adding artificial triggers to make sure the asserted quantifiers are never triggered) would have the same consequences. @Dev-XYS @alexanderjsummers Please speak up if you disagree.