transformation split_intros_goal_wp always produces a new subgoal
Transformation split_intros_goal_wp always produces a new subgoal, even when it should instead report an absence of progrss.
As a consequence, strategy 1 loops forever on unprovable goals, repeatedly applying split_intros_goal_wp successfully then provers unsuccessfully.
To reproduce the issue, use an input file limited to "goal G: false" and launch strategy 1 from why3 ide.
Note: strategy "2", on the contrary, terminates. But it uses split_all_full instead.