sosy-lab/sv-benchmarks

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

holznerst opened this issue · 1 comments

holznerst commented

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:

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 commented

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.