Fixing all variables to a solver-found solution gives UNSAT with nested tree globals

[Yılmaz]

Hi all,

I have a MiniZinc model with:

• A top-level tree constraint (global tree).

• Nested tree(...) constraints for sub-groups, where they re-use the global tree node and edge variables by slicing.

(Please see the bottom of my email)

I ran the solver (Chuffed) for feasibility, and obtained a solution.

Now, when I activate assignment constraints to force all variables to these found values, I get UNSATISFIABLE. And the solution that was found was indeed violating some of the local tree constraints.

I just wanted to ask if this is technically possible, or should I report a bug?

Best regards,

Yılmaz

constraint tree( ND, NE, ud, vd, var_r, var_dn, var_de);

constraint forall(p in 1..NP) ( let { array[1..snil[p]] of var bool: var_sn = [ var_dn[i] | i in sni[ snis[p]..snis[p] + snil[p] - 1 ] ];
array[1..sel[p]] of var bool: var_se = [ var_de[i] | i in sei[ seil[p]..seil[p] + sel[p] - 1 ] ];
array[1..sel[p]] of int: u = array1d(1..sel[p], [ us[i] | i in ses[p]..ses[p] + sel[p] - 1 ]);
array[1..sel[p]] of int: v = array1d(1..sel[p], [ vs[i] | i in ses[p]..ses[p] + sel[p] - 1 ]); } in
tree( snil[p], sel[p], u, v, var_sr[p], var_sn, var_se ));