Changed the coerce_postcondition in the vector contract to specify that the two results must be multipliable.