Gecode 6.3.0 incorrectly thinks model is unsat

[Wout4]

The following model returns 'unsatisfiable' when using Gecode 6.3.0, we can easily verify that it is satisfiable by using another solver, or by adding constraint p == false; after the other constraints.

var bool: p;
var 0..10: n_neg;
var 0..5: IV8708;
var 0..5: IV8709;
var 0..5: IV8710;
var bool: BV32799;
var bool: BV32800;
var bool: BV32801;
var bool: BV32798;
constraint (p) -> (((n_neg) div 2) < (true));
constraint (p) -> (((n_neg) div 2) < (true));
constraint (p) -> (((n_neg) div 2) < 1);
constraint not(((not((p) -> (((n_neg) div 2) < (true)))) + (not((p) -> (((n_neg) div 2) < (true))))) == 1);
constraint ((n_neg) div 2) == (IV8708);
constraint (p) -> ((IV8708) < 1);
constraint ((BV32799) + (BV32801)) != 1;
constraint ((p) /\ (BV32798)) == (BV32799);
constraint ((n_neg) div 2) == (IV8709);
constraint ((IV8709) >= 1) == (BV32798);
constraint ((p) /\ (BV32800)) == (BV32801);
constraint ((n_neg) div 2) == (IV8710);
constraint ((IV8710) >= 1) == (BV32800);
constraint ((not(((not((p) -> (((n_neg) div 2) < (true)))) + (not((p) -> (((n_neg) div 2) < (true))))) == 1)) + (not(((BV32799) + (BV32801)) != 1))) == 1;

solve satisfy;

[Wout4]

Found another smaller model with the same problem:

var -3..5: x;
var -3..5: y;
var -3..5: z;
var 0..10: l;
var bool: p;
constraint not(((not(((not(((max([x,y,z])) < (l)) == (p))) + (not(((max([x,y,z])) < (l)) == (p)))) == 1)) + (((max([x,y,z])) < (l)) == (p))) == 1);
solve satisfy;

[zayenz]

This is really interesting, and also quite scary. Thanks for creating a smaller example, and especially one that does not contain div (that is a partial function, and partiality and negation are tricky things to understand fully).

I've checked the behavior as well, and it does seem to do something quite erroneous. OR-Tools solves it, as does HiGHS. OR-Tools gets the same FlatZInc output, so it should not be something that depends on Gecode-particular translations. I also translated using the HiGHS library to FlatZinc, and that model Gecode solves correctly.