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

[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.

I incorporated the sequence axiom change you asked for.