======================================
L_TUPLES (invariant admissibility)
Successfully verified.
======================================
L_TUPLES.make (creator)
Successfully verified.
======================================
L_TUPLES.good
Successfully verified.
======================================
L_TUPLES.bad
Verification failed.

Line: 51. Check may be violated (untagged).
--------------------------------------
Line: 54. Check may be violated (untagged).
--------------------------------------
Line: 57. Check may be violated (untagged).
======================================
L_TUPLES.update_good
Successfully verified.
======================================
L_TUPLES.update_bad
Verification failed.

Line: 79. Check may be violated (untagged).
--------------------------------------
Line: 84. Check may be violated (untagged).