Show warning on proofs with loop-depth bounded nodes #1973
Description
As suggested by @ehildenb (#1963 (comment)), we should have a loud warning on passed proofs if any nodes are passed because they are bounded, something like "Proof passed, but NNN nodes were loop-depth bounded at MMM iterations, re-run with --unbounded-loops for full verification."