Remove runtime checks

[xldenis]

Rather self-explanatory, but taking the time to eliminate all runtime checks would be very beneficial to the proof itself.

[sarsko]

Agreed.

It should be noted that all runtime checks are not equal.

The worst kind (which currently occur in a couple of places) are the ones that return an Err if they fail. Currently that happens if the formula has conflicting units in the initial formula (could be proven away, I havent prioritized it) and before returning a satisfying assignment (blocked on the proof of 2WL).

Removing this "bad" kind is in my opinion important.

The other kind is to check something runtime which could be proven statically, but which does not result in an Err or similar. An example of this is the linear pass at the end of VMTF to check that we actually have a complete assignment.

Removing these checks are in my opinion much less important. Some of them have a (perhaps) noticeable runtime cost, and are thus as important to prove as any other optimisation which would yield that amount of performance. Proving statically properties which cause basically no performance improvement (i.e. the VMTF check) is not worth it in my opinion.