Would it be likely that I could get around that problem just by using arena allocation? Do you think the allocation patterns of a symbolic checker fit that sort of "just allocate everything and forget about it, then free it all at once" pattern? Does Rust make it easy to punt that way?