The idea is that every big WP is built from "explainable" subformulas.
So, when we split for the first time, we stop at these subformulas.
The subsequent split will split them further.

Note that split_goal removes "stop_split" labels. Thus, if we have
an atomic assertion ("expl:precondition" "stop_split" true), then
the split_goal transformation will succeed and return a _different_
task, with the goal: ("expl:precondition" true). However, the second
split will return the same task exactly. Should we fix it?

At the moment, we lack explanation annotations over postconditions.