OR construct in forall constraint not satisfied

[marvinvis]

Using MiniZinc Version 2.8.2 (1107726878)
I have inconsitent results betewen OrTools and Gecode, running the following model:

set of int: Range = 1..9;
array[Range] of var 0..10: a;
var int: mx = 5;

% the OR messes up the constraint
var bool: obj1::output = (forall(i in Range where i <= mx) (a[i] = 1 \/ a[i] = 2));
constraint obj1 = true;

constraint a[1] = 0;

solve satisfy;

Gecode gives:

Warning: model inconsistency detected
=====UNSATISFIABLE=====
Finished in 192msec.

which is correct.

Ortools however gives:

a = [0, 0, 0, 0, 0, 0, 0, 0, 0];
obj1 = true;
----------
==========
Finished in 264msec.

Which is incorrect.

the FZN towards Ortools is:

var 0..10: X_INTRODUCED_1_;
var 0..10: X_INTRODUCED_2_;
var 0..10: X_INTRODUCED_3_;
var 0..10: X_INTRODUCED_4_;
var 0..10: X_INTRODUCED_5_;
var 0..10: X_INTRODUCED_6_;
var 0..10: X_INTRODUCED_7_;
var 0..10: X_INTRODUCED_8_;
array [1..9] of var int: a:: output_array([1..9]) = [0,X_INTRODUCED_1_,X_INTRODUCED_2_,X_INTRODUCED_3_,X_INTRODUCED_4_,X_INTRODUCED_5_,X_INTRODUCED_6_,X_INTRODUCED_7_,X_INTRODUCED_8_];
solve  satisfy;

To dig deeper in the cause I experimented with different constructions that are similar:

When I use an AND construction for obj1 as follows:

% similar construction, with an AND works fine
var bool: obj2::output = (forall(i in Range where i <= mx) (a[i] <= 2 /\ a[i] > 0));
constraint obj2 = true;

both solvers correctly state:
=====UNSATISFIABLE=====

When I use a fixed boundary in the where, for obj1 as follows:

% with a par max range obj3 is not satisfied to be true
var bool: obj3::output = (forall(i in Range where i <= 5) (a[i] = 1 \/ a[i] = 2));
constraint obj3 = true;

both solvers correctly state:
=====UNSATISFIABLE=====