With aggressive pruning, admissibility check for a group may drop critical definitions of the enclosing structure, resulting in Buggy Boogie. (This is related to the syntax change in 7ed71cef38b6). Repro attached.