Measure and communicate Z3 rlimit value

[robin-aws]

This can be used as a more stable cost metric than wall clock time, which depends on the local CPU speed and can be artificially inflated when running multiple verification processes in parallel.

[parno]

FWIW, if you run Z3 from the command line with the -st option, it will report the rlimit value it used. Unfortunately, if you try to pass this via Boogie, Boogie's low-level text channel to Z3 can't seem to handle the response and will drop the data Z3 supplies.

[robin-aws]

Thanks for the suggestion @parno! I seem to have something working based on sending (get-info :rlimit) to Z3 through the channel instead.

[atomb]

Part of this exists now that boogie-org/boogie#482 is merged.