Chuffed returns a solution that is infeasible

[Hector Perez]

Consider the following problem I am trying to solve with Chuffed (to get all feasible solutions):

```
var bool: x_D;
var bool: x_E;
var bool: x_S1;
var bool: x_I;
var bool: x_H;
var bool: x_C;
var bool: x_S3;
var bool: x_S5;
var bool: x_S2;
var bool: x_A;
var bool: x_F;
var bool: x_G;
var bool: x_S0;
var bool: x_B;
var bool: x_S4;
constraint -1*x_D + 1*x_S5 + 1*x_S4 = 0;
constraint 1*x_A = 1;
constraint 1*x_S1 + -1*x_A + 1*x_S0 = 0;
constraint -1*x_C + 1*x_S3 + 1*x_S2 = 0;
constraint -1*x_F + -1*x_G + 1*x_S4 >= -1;
constraint -1*x_E + 1*x_S3 >= 0;
constraint -1*x_E + 1*x_S2 >= 0;
constraint -1*x_D + 1*x_S1 + -1*x_I + -1*x_C >= -2;
constraint 1*x_S0 + -1*x_B >= 0;
constraint -1*x_H + 1*x_S5 >= 0;
constraint -1*x_E + 1*x_S2 <= 0;
constraint -1*x_E + 1*x_S3 <= 0;
constraint -1*x_F + 1*x_S4 <= 0;
constraint 1*x_S1 + -1*x_I <= 0;
constraint -1*x_H + 1*x_S5 <= 0;
constraint 1*x_S0 + -1*x_B <= 0;
constraint -1*x_G + 1*x_S4 <= 0;
constraint 1*x_S1 + -1*x_C <= 0;
constraint -1*x_D + 1*x_S1 <= 0;
solve satisfy;
```

The output is:
```
x_D = false;
x_E = false;
x_S1 = false;
x_I = false;
x_H = false;
x_C = false;
x_S3 = false;
x_S5 = false;
x_S2 = false;
x_A = true;
x_F = false;
x_G = false;
x_S0 = true;
x_B = false;
x_S4 = false;
```

This is WRONG. Note that this constraint is violated: constraint 1*x_S0 + -1*x_B <= 0;
If x_S0 = 1 and x_B = 0, then this gives 1 <= 0. 

Is this the best place to report this bug? Or is there another place I should post this issue?

Thank you

[jason.nguyen]

Hi,

Thanks for the bug report. This seems likely to be a MiniZinc bug as I've been able to reproduce it in both Chuffed and Gecode.

It would be great if you could report it in the MiniZinc compiler bug tracker (if you have a GitHub account).

Best regards,

Jason

[Ons Huis]

I added this to the model

var int: t1;

var int: t2;

var int: t3;

..

constraint t1 =1*x_S0;

constraint t2 =-1*x_B;

constraint t3 =t1 +t2

and the output became:

x_S0 = true;

x_B = true;

x_S4 = false;

t1 = 1;

t2 = -1;

t3 = 0;

Op donderdag 3 juli 2025 om 03:24:33 UTC schreef jason.nguyen: