Optionally skip re-verification of well-definedness

[marcoeilers]

Silicon verifies that predicate bodies, function preconditions, and method pre- and postconditions are self-framing and well-defined. As a result, it is not necessary to re-verify well-definedness when using them (but Silicon always does so anyway).

This PR adds a flag in the state that expresses whether well-definedness of the currently consumed or produced assertion needs to be checked. By default, this flag does nothing, but setting a command line option will lead to Silicon actually skipping the checks in those cases.

Additionally, it introduced another flag that expresses whether any conditions (well-definedness or correctness) should currently be checked or assumed. This is for later usage to enable us to skip verification of parts of methods if they are already known to be correct.

[Aurel300]

Do we want this to become the default? I am guessing this improves performance.

[marcoeilers]

I hoped it would, but it actually leads to worse performance on SCION code. So for now I basically just wanted to have this option available to experiment with.

[superaxander]

I would be interested in using this flag. I tried it out and for my file it makes the difference between it (nondeterministically) failing to verify and verifying. I think this is because I have a lot of heap chunks in the state at the call site of my method. All these extra heap chunks slow down the check for permissions when inhaling the postcondition of my method. However, I don't think there is any reason these permissions need to be checked since they've just been inhaled by the postcondition and the method itself has already been verified. (and that verification of the method itself was really fast because the method only deals with a handful of heap chunks)