Invariant checker takes as an input two files. A set of invariants and a trace. If the trace does not violate the invariants, invariant checker gives an ok. If the invariants are violated, the violating part of the trace is printed.
Given a dinv trace, invariants, and a shivz output annotate run invariant checker on the trace an invariants. If the trace violates an invariant annotate the corresponding cut in the shiviz log.
[Issue created by wantonsolutions: 2017-02-10]