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"…
