X86 verification delays assuming preconditions too long

[robdockins]

When performing X86 verification, specification preconditions are not assumed prior to symbolically executing the function to be verified. Instead, they are only assumed during the assertPost phase, immediately before asserting the collected postconditions.

As a result, safety conditions that arise during symbolic simulation do not get to assume the specification preconditions, which can make them impossible to discharge if their safety, in fact, depends on those preconditions.

[chameco]

See also #1095, which failed to consider this case. I suspect we can easily reuse some LLVM helper function for this (probably setupPrestateConditions), and also grab the precondition vacuity checking feature.

[robdockins]

Fixed via #1705