Seperate SMT Analysis Stages

[d-xo]

The SMT backend currently performs two checks:

1. Invariants hold
2. Postconditions are implied by preconditions

These checks are currenlty performed in a single pass, and we currenlty force the second to be run for all specs by inserting an implicit true invariant on all contracts. This is pretty hacky and makes the smt output a little messy (as the implicit invariant shows up in the output). This also fails if the spec does not include a construcor.

We should rework the SMT backend to work in multiple passes. This will lay the foundation for future analyis stages (e.g. exhaustiveness, bounds checking), and make generating nice output from the smt backend easier.

[MrChico]

Related #14