Possible bug in :solve-classic

[gciatto]

problem(X,Y,Z) :- 
    ins([X,Y,Z], '..'(1, 3)), 
    in(W, 2),
    in(V, 1),
    global_cardinality([X,Y,Z],['-'(1,W), '-'(2,V)]).

When execution reaches global_cardinality, information about the rewriting history of W is lost.

How to reproduce

https://github.com/giuseppeboezio/ChocoKt/blob/9b74304d5cdf1e223fc66c722cbcf39bf8d3f998/clpfd/src/test/kotlin/clpfd/global/GlobalCardinalityTwoTest.kt#L14

Hypothesis

The problem is in StateGoalSelection.
When popping the current EC, the substitution is update by only keeping variables which are interesting for the parent EC.
This is ok.
But the "dirty" substitution containing uninteresting variables may have already been applied to the subsequent goals because of the mapping:

val goalsWithSubstitution = context.goals.map { it[context.substitution] }

We should consider avoiding mapping, but rather applying the current substitution to the current goal, whenever the current goal is needed

[gciatto]

@giuseppeboezio watch this issue

[gciatto]

Solved in #413.
A new flag has been introduced, track_variables which is off by default.
When on, the new flag lets the classic solver track variables in a more memory-requiring way, which prevents the issue described here