var bool: reif :: output_var;

var 1..3: x1 :: output_var;
var 1..3: x2 :: output_var;
var 1..3: x3 :: output_var;

constraint int_lin_eq_reif([-1, 1, 2], [x1, x2, x3], 5, reif);

solve satisfy;