When computing negated axioms (in the default value axioms task transformation) we currently use a trivial overapproximation for derived variables with cyclic dependencies. The reason for this is that simply negating the formula is not correct (see issue453). We could compute the negated axioms exactly by using unrolling.
|