Low values of :rlimit have no effect

[robin-aws]

I ran into this when trying to verify my project setup was correct by setting an :rlimit of 1 (which before #796 was multiplied to 1000, but that was still far too low) to check that I got a build failure, but verification succeeded anyway.

From discussions with @atomb it seems likely that Z3 (in my case) can easily succeed before it does the first periodic check against such limits. If so, this also might be a concern for reproducible builds, if whether the solver checks the limit in time is non-deterministic.

I'd suggest that when an rlimit is set, Boogie does its own post-hoc check against the limit, for a consistent experience. Alternatively we could reject rlimit values that are too low to have any effect, but that would be solver-specific and may be hard to pin down reliably.