Klever

Model function comments are redundant and harmful. In fact they try to duplicate corresponding actions inside corresponding function bodies. Usually this is done not so good, so they hide important things. Moreover, in principle it is impossible to reflect various paths, e.g. when a model function returns an error and not, using one sentence.

The issue spans over several places from rule specifications to witnesses preprocessing.