Runtime-check fails when removing imprecision and adding fold to the specification.

[icmccorm]

The following error was observed while testing out a change to the permuter. This new mode removes imprecision from methods and predicates if all of their specifications are complete, and if none of the predicates used in the specifications are incomplete.

Permutation 149/153 of BST verifies and runs successfully. Then, Permutation 150 of BST adds the following specification component within create_tree_helper:

//@fold bst(root->right, root->val + 1, max);

This completes the full specification for create_tree_helper, and since bst has already been completed, all imprecision is removed from create_tree_helper. This verifies, but causes a failing run-time check for acc(Node.left) within tree_remove_helper on line #552.

I've attached 149, 150, and the version of 150 with run-time checks inserted. Compiling 150 should reproduce the failure.

Additionally, here's the output from running diff on 149 and 150:

132a133
> m.create_tree_helper.3.fold.pred_inst.8
205,206c206,207
<   //@requires ? && min <= val && val <= max;
<   //@ensures ? && bst(\result, min, max);
---
>   //@requires min <= val && val <= max;
>   //@ensures bst(\result, min, max);
213a215
>   //@fold bst(root->right, root->val + 1, max);