# This check is needed because the contract can appear after the introduction.
if unsafe_mtype.has_mproperty(visited_method.mpropdef.mclassdef.mmodule, contract_facet) then
# This check is needed because the contract can appear after the introduction.
if unsafe_mtype.has_mproperty(visited_method.mpropdef.mclassdef.mmodule, contract_facet) then