Allow proposed invariants

[agacek]

JKind should support proposed invariants, e.g.

--%INVARIANT inv0;

These are slightly different than properties:

1. We don't report if they are true or unknown
2. We report some kind of warning if they are false
3. We slice away invariants which are not related to the properties of interest
4. We should probably treat subrange declarations on locals and outputs as these types of invariants

But these invariants should be handled by the base and inductive step processes rather than the invariant generation process. These are things we expect to be true and perhaps useful, so we want them checked quickly. Invariant generation is more speculative and takes longer to run.