FIXED: CLP(B): Correctly handle duplicate variables in cardinality constraint.
FIXED: CLP(B): Correctly handle duplicate variables in cardinality constraint.

Witness:

   ?- Vs = [X1,X3,X2,X4], labeling(Vs), Sat1 = sat(X1+X2), Sat2 = sat(card([0,1],[X3,X4])), X3 = X4, X3 = X2, Sat1, Sat2.
   %@ Vs = [1, 0, 0, 0],
   %@ X1 = 1,
   %@ X3 = X2, X2 = X4, X4 = 0,
   %@ Sat1 = sat(1+0),
   %@ Sat2 = sat(card([0, 1], [0, 0])) ;
   %@ false.

vs.:

   ?- Vs = [X1,X3,X2,X4], Sat1 = sat(X1+X2), Sat2 = sat(card([0,1],[X3,X4])), Sat1, Sat2, X3 = X4, X3 = X2, labeling(Vs).
   %@ Vs = [0, 1, 1, 1],
   %@ X1 = 0,
   %@ X3 = X2, X2 = X4, X4 = 1,
   %@ Sat1 = sat(0+1),
   %@ Sat2 = sat(card([0, 1], [1, 1])) ;
   %@ Vs = [1, 0, 0, 0],
   %@ X1 = 1,
   %@ X3 = X2, X2 = X4, X4 = 0,
   %@ Sat1 = sat(1+0),
   %@ Sat2 = sat(card([0, 1], [0, 0])) ;
   %@ Vs = [1, 1, 1, 1],
   %@ X1 = X3, X3 = X2, X2 = X4, X4 = 1,
   %@ Sat1 = sat(1+1),
   %@ Sat2 = sat(card([0, 1], [1, 1])).

Test case:

    :- use_module(library(clpb)).

    sat(_)  --> [].
    sat(X*Y) --> [_], sat(X), sat(Y).
    sat(X+Y) --> [_], sat(X), sat(Y).
    sat(X#Y) --> [_], sat(X), sat(Y).
    sat(card([0,1],[X,Y])) --> [_], sat(X), sat(Y).

    vs_eqs(Vs, Eqs) :- phrase(vs_eqs(Vs), Eqs).

    vs_eqs([]) --> [].
    vs_eqs([V|Vs]) --> vs_eqs_(Vs, V), vs_eqs(Vs).

    vs_eqs_([], _) --> [].
    vs_eqs_([V|Vs], X) --> vs_eqs_(Vs, X), ( [X=V] ; [] ).

    run(N) :-
            length(Ls, N),
            portray_clause(N),
            phrase(sat(Sat1), Ls),
            phrase(sat(Sat2), Ls),
            term_variables(Sat1-Sat2, Vs0),
            permutation(Vs0, Vs),
            vs_eqs(Vs, Eqs),
            findall(Vs, (sat(Sat1),sat(Sat2),maplist(call, Eqs),labeling(Vs)), Sols1),
            findall(Vs, (labeling(Vs),maplist(call,Eqs),sat(Sat1*Sat2)), Sols2),
            (   sort(Sols1, Sols), sort(Sols2, Sols) -> true
            ;   throw(neq-Sat1-Sat2-Eqs-Vs0-Vs-Sols1-Sols2)
            ),
            false.

    run :- run(_).

Yielding:

    ?- run.
    %@ 0.
    %@ 1.
    %@ ERROR: Unhandled exception: neq- (_G340+_G341)-card([0,1],[_G352,_G355])-[_G352=_G355,_G352=_G341,_G341=_G355]-[_G340,_G341,_G352,_G355]-[_G340,_G352,_G341,_G355]-[[0,1,1,1],[1,0,0,0],[1,1,1,1]]-[[1,0,0,0]]

koryonik/swipl-devel,jn7163/swipl-devel,koryonik/swipl-devel,jn7163/swipl-devel,mndrix/swipl-devel,edechter/swipl-devel,koryonik/swipl-devel,mndrix/swipl-devel,jn7163/swipl-devel,jn7163/swipl-devel,edechter/swipl-devel,koryonik/swipl-devel,mndrix/swipl-devel,edechter/swipl-devel,mndrix/swipl-devel,edechter/swipl-devel,mndrix/swipl-devel,jn7163/swipl-devel,koryonik/swipl-devel,edechter/swipl-devel