On Thursday, 7 August 2014 at 15:35:30 UTC, Ola Fosheim Grøstad wrote: > assume(input!=0) is ok… it does not say unreachable. > It says, postconditions are not required to hold for input==0… And… assume(false) is a precondition that says that you don't have to care about the postconditions at all… Basically, "assume anything"…