Soundness hole in split_vc
When using split_vc on a goal with several existentials with the same name, split_vc does not use different variables for the different existentials. This is a soundness hole, as demonstrated in the following WhyML and session files: