This commit adds an additional check if there are choices in domains of
positively stratified atom occurences. Such occurrences are demoted to
stratified occurrences if the test suceedes. This should only affect
multi-shot solving, for example, when rules have been added previously
via the backend. It might classify some occurences as stratified that
were correctly classified positively stratified before. Since the
classification is just about optimizing a corner case, this should not
matter much in practice.