MZN 2.5.3 flattening bug: xorall

[matsc-at-sics-se]

Illustration:

$ cat foo.mzn
var 0..1: A;
var 0..1: B;
constraint
    xorall(p in [A=1])(p) <-> B=1;
$ minizinc -c foo.mzn 
$ minizinc -a foo.mzn 
A = 1;
B = 1;
----------
==========
$ cat foo.fzn
var 1..1: A;
var 1..1: B;
solve  satisfy;

There should be a second solution: A=0, B=0. The flattener does some invalid transformation, it seems. The bug surfaces for lists of length greater than one as well.

[matsc-at-sics-se]

It's more general than that. The bug surfaces if you replace xorall by exists or forall as well.

[zayenz]

As an additional data-point, breaking out the array comprehension into it's own variable like this

var 0..1: A;
var 0..1: B;
array [1..1] of var bool: X = [A=1];
constraint xorall(X) <-> B=1;

gives the expected behavior with two solutions.