Change Details

If we load rd_seq after goal rd_seq may have already advanced beyond goal making the comparison incorrect. While here fix up the limits on invariants kernels because it was polling way too frequently.