Inconsistency in unreach-call verdicts for verifythis: tree_del_rec.yml, tree_del_iter.yml and tree_max.yml

[holznerst]

There is a inconsistency in the verify this reach-ability category: There are three benchmark tasks which were split into a safe version and a incorrect version with bug fixes in #851:

• verifythis/tree_del_iter.yml
• verifythis/tree_del_iter_incorrect.yml
• verifythis/tree_del_rec.yml
• verifythis/tree_del_rec_incorrect.yml
• verifythis/tree_max.yml
• verifythis/tree_max_incorrect.yml

In #923 the unreach-call verdicts of the safe tasks were changed to false. We now have a safe version and a incorrect version of each task there both have a false verdict. I don't think this matches the intention of the author, who provided bug fixes for the original tasks.

If I'm right, I would propose to undo the verdict changes and rather fix the tasks if possible. @gernst could you please have a look, what do you think?

[gernst]

Sorry for my late reply. I recall there was some discussion about these tasks, specifically, that the original version had errors despite the goal of being correct. Hence, I support your proposal, but I don't know really where these bugs were, but memcleanup is of course not valid. Not sure whether memcleanup should be considered, a recursive free method for trees might cause the unreach-call task to become harder as well, which I would not like.