Great! :-)

I created a test task to validate the correct behaviour of my code. This way I
also found out that the same behaviour was caused by the optional simplification
step (in simplify.py) after the validation in sas_task.py. Since we want to
guarantee cleaned up effect conditions for the search component, I nevertheless
merged my changes. The documentation of the validation requirements has been
updated.

Sorry for the late reply! Feel free to merge if you don't think someone else
should look at the code. Have you also updated the documentation of the
validation requirements in sas_tasks.py?

Regarding the part of the documentation that you quoted, I don't think I
encountered this anywhere. I just thought about which odd things might possibly
exist in the input.

I only consider contradictions that become apparent from conflicting variable
values (not any additional information from mutex groups). While being at it, I
also remove facts from effect conditions that are already operator pre- or
prevail conditions.

I updated build_sas_operator in translate.py accordingly and updated the
validation so that effect conditions may not mention any variables from pre- and
prevail conditions.

These changes have no effect on any of our benchmark instances. The only
differences were in two large trucks instances but these were due to a different
encoding caused by the time out of the invariant synthesis.

Malte, in the documentation of the sas task validation you wrote

     Odd things that are *not* illegal:
        - Effect conditions that contradict a precondition or prevail
          condition are permitted.

How did you encounter this? Did you run an extra test case?

Should I just merge the changes or do you want to have a look at the code?

This should easily be possible in build_sas_operator of translate.py. If we do
this, we should also update SASOperator.validate().