The following static verification error occurs intermittently during mass benchmarking of AVL, but not when the same programs are verified locally.
Unfolding avlh(node, h) might fail. Fraction write might be negative.
This error is flaky; programs that pass during one benchmarking run may fail during the next. I have verified that the occurrence for permutation #7689 of AVL has been logged correctly in the benchmarking database. Since the behavior is similar to #43, it's possible that it's being caused by the same underlying issue. The attached programs have exhibited this behavior.
The following static verification error occurs intermittently during mass benchmarking of AVL, but not when the same programs are verified locally.
This error is flaky; programs that pass during one benchmarking run may fail during the next. I have verified that the occurrence for permutation #7689 of AVL has been logged correctly in the benchmarking database. Since the behavior is similar to #43, it's possible that it's being caused by the same underlying issue. The attached programs have exhibited this behavior.
avl_7689.c0
avl_10154.c0