Gecode 6.3.0 fails to recognize an unsatisfiable model when using alldifferent

[JakubDob]

For the given input model:

include "globals.mzn";
array [0..2] of var 0..2: a;
constraint a[0]=1;
constraint a[1]=1;

constraint alldifferent([a[0],a[1],a[2]]);
solve satisfy;

It returns: a = [0: 1, 1: 1, 2: 0];

Tested here: https://play.minizinc.dev/ and using the npm version. Coin-bc correctly reports unsat.

The pc version of Gecode 6.3.0 returns: =====UNSATISFIABLE=====

[Dekker1]

I suspect that this is an issue with the internal Gecode interface that occurs when part of the input of an all_different constraint is already fixed.

The version of Gecode packaged with the MiniZinc bundle does not have the same problem.

[JakubDob]

Interestingly, the order of constraints in the model seems to matter:

include "globals.mzn";
array [0..2] of var 0..2: a;
constraint alldifferent([a[0],a[1],a[2]]);
constraint a[0]=1;
constraint a[1]=1;
solve satisfy;

Here the js version returns unsat.