WyIL: Initial support for checking div-by-zero.

The VcGenerator must now generate its own precondition checks for
expressions.  Previously, they were inlined using the RuntimeAssertions
phase.  I have now added rudimentary support for this, but more needs to
be done!