[BUG] Integer overflow when composing nested affine views produces incorrect results #1244

Describe the bug

Composing two affine integer expressions can overflow while Choco flattens the
nested views, even when every value that the expression can actually take is
well within Choco's recommended integer bounds.

The corrupted view can affect correctness in both directions:

• a valid solution can be removed and the model reported unsatisfiable;
• an assignment that violates the posted constraint can be returned as a
  solution.

The issue is reproducible through the public arithmetic-expression API, with
views enabled (the default).

To reproduce

The following complete example demonstrates both effects:

import org.chocosolver.solver.Model;
import org.chocosolver.solver.variables.IntVar;

public class NestedAffineViewOverflow {

    public static void main(String[] args) {
        falseUnsat();
        invalidSolution();
    }

    private static void falseUnsat() {
        Model model = new Model();
        IntVar x = model.intVar("x", 46_341, 46_342, false);
        IntVar result = x.sub(46_341).mul(46_341).intVar();

        result.eq(0).post();

        boolean solved = model.getSolver().solve();
        System.out.println("eq(0): " + solved);
        // Actual:   false
        // Expected: true, with x = 46_341
    }

    private static void invalidSolution() {
        Model model = new Model();
        IntVar x = model.intVar("x", 46_341, 46_342, false);
        IntVar result = x.sub(46_341).mul(46_341).intVar();

        result.ne(0).post();

        while (model.getSolver().solve()) {
            System.out.println("ne(0): x = " + x.getValue() + ", result = " + result.getValue());
        }
        // Actual:   x = 46341, result = 0; then x = 46342, result = 46341
        // Expected: x = 46342 only
    }
}

The first example uses the default Model settings. It prints:

eq(0): false

The second example also uses the default Model settings and prints:

ne(0): x = 46341, result = 0
ne(0): x = 46342, result = 46341

Changing the first model to use

new Model(SettingsBuilder.init().setEnableViews(false))

makes it find the expected solution x = 46_341.

The problem occurs with both bounded and enumerated domains for x.

Expected behavior

The expression has only two possible mathematical values:

x = 46341 -> (46341 - 46341) * 46341 = 0
x = 46342 -> (46342 - 46341) * 46341 = 46341

Therefore:

• result.eq(0) must have the single solution x = 46_341;
• result.ne(0) must have the single solution x = 46_342.

Both possible expression values, 0 and 46_341, are well below
IntVar.MAX_INT_BOUND (21_474_836). The model itself does not require an
out-of-range value.

Scope

Targeted checks show that the same corrupted affine view affects all six
relational operators: =, !=, <, <=, > and >=. Depending on the
operator, a valid value can be removed, an invalid value can be kept, or the
default solution checker can raise InvalidSolutionException after propagation
accepts an invalid assignment.

The != case in the main reproducer is particularly important: with the
default settings, Choco returns x = 46_341 even though result = 0, without
raising an exception or emitting a warning. The solution checker evaluates the
constraint through the same corrupted view and does not detect the violation.

For example, the following model has the valid solution x = 46_342, for which
result = 46_341:

Model model = new Model();
IntVar x = model.intVar("x", 46_341, 46_342, false);
IntVar result = x.sub(46_341).mul(46_341).intVar();
model.arithm(result, ">=", 1).post();

model.getSolver().solve();

Instead of returning that solution, solve() raises
InvalidSolutionException. The corrupted view first leads the solver to the
invalid assignment x = 46_341, which is then rejected by the default solution
checker.

With the solution checker disabled by the production settings, the same
propagation error becomes directly observable in the returned solutions:

Model model = new Model(SettingsBuilder.prod());
IntVar x = model.intVar("x", 46_341, 46_342, false);
IntVar result = x.sub(46_341).mul(46_341).intVar();
model.arithm(result, ">=", 1).post();

while (model.getSolver().solve()) {
    System.out.println("x = " + x.getValue() + ", result = " + result.getValue());
}

The output is:

x = 46341, result = 0
x = 46342, result = 46341

Only x = 46_342 is valid. For x = 46_341, the expression is equal to zero
and therefore violates result >= 1.

The observed results for the same expression are:

Possible cause

The nested affine view is flattened in IViewFactory.intView(...). The
composed coefficients are currently calculated as int:

int av = (view.p ? 1 : -1) * view.a * a;
int bv = a * view.b + b;

For (x - 46_341) * 46_341, the expanded constant is:

-46341 * 46341 = -2,147,488,281

This is only 4,633 below Integer.MIN_VALUE, so the int calculation wraps
to:

2,147,479,015

The overflow concerns the constant of the expanded representation, not a value
that the original expression can take on its domain.

46_341 is also a compact boundary case: 46_340 * 46_340 = 2,147,395,600
still fits in an int, whereas 46_341 * 46_341 = 2,147,488,281 does not.

Possible solution

Calculating only the composed coefficients in long and checking av and
bv is not sufficient. For example:

IntVar x = model.intVar("x", 46_273, 46_276, false);
IntVar result = x.sub(46_273).mul(46_406).intVar();
result.eq(139_218).post();

The valid solution is x = 46_276, but Choco returns no solution. The flattened
coefficients are both representable:

av = 46,406
bv = -2,147,344,838

However, av * 46,276 = 2,147,484,056 is not representable as an int.
During inverse propagation, the equivalent calculation
139,218 - (-2,147,344,838) reaches the same value and overflows before the
division by av.

One possible approach is therefore to check both the composed coefficients and
the scaled and shifted endpoint values before flattening. Otherwise, the
original view can be kept nested:

static boolean fitsInt(long value) {
    return value >= Integer.MIN_VALUE && value <= Integer.MAX_VALUE;
}

long lav = (view.p ? 1L : -1L) * view.a * a;
long lbv = (long) a * view.b + b;
if (!fitsInt(lav) || !fitsInt(lbv)) {
    return new IntAffineView<>(var, a, b);
}

IntVar base = view.getVariable();
long scaledLB = lav * base.getLB();
long scaledUB = lav * base.getUB();
if (!fitsInt(scaledLB) || !fitsInt(scaledUB)
        || !fitsInt(scaledLB + lbv) || !fitsInt(scaledUB + lbv)) {
    return new IntAffineView<>(var, a, b);
}

int av = (int) lav;
int bv = (int) lbv;

This fallback uses the same new IntAffineView<>(var, a, b) construction that
is already used by the current non-flattening branch; it does not require a new
view type.

No remaining correctness failure was observed in the tested scope. The extended
guard fixes all identified counterexamples and the targeted checks for all six
relational operators. The existing Choco view tests also pass with this guard.
This remains a suggested implementation; a more efficient solution may be
possible while preserving the same view invariants.

Environment

• Choco-solver: 6.0.1
• JRE used for the reproduction: OpenJDK 26.0.1
• LCG: not enabled