The difference between option_fail.rs and option.rs lies in the assumption that y > 0, yet the standard value for y is set as 2u64 so the assertion is not failing in option_fail.
Is there an error in that the y standard value is supposed to be 0u64 so that the verifier::unreachable! macro is called or am I missing another scenario where it is supposed to fail?