Scryer-prolog: clpz: unexpected redundant answer

[UWN]

?- A in 0..1, B in 1..3,A*B#>C,labeling([],[A,B]),B=1, A=1, v(A,C)=v(1,0).
   A = 1, B = 1, C = 0
;  false.
?- A in 0..1, B in 1..3,A*B#>C,labeling([],[A,B]),B=1,      v(A,C)=v(1,0).
   A = 1, B = 1, C = 0
;  A = 1, B = 1, C = 0            % unexpected
;  false.

[UWN]

?- A in 0..1, B in 1..3,A*B#>C,(A=0;A=1),labeling([],[B]), ( B=0 ; v(A,C) = v(1,0) ).

   A = 1, B = 1, C = 0
;  A = 1, B = 0, clpz:(C+1#=_A), clpz:(0#>=_A), clpz:(_A in inf..3), clpz:(C in inf..2)   % unexpected
;  A = 1, B = 0, C = 0                                                                    % unexpected
;  A = 1, B = 1, C = 0
;  A = 1, B = 2, C = 0
;  A = 1, B = 3, C = 0

[UWN]

?- A in 0..1, B in 1..3,A*B#>=C,(A=0;A=1),labeling([],[B]), ( B=0 ; v(A,C) = v(1,0), false ).
   A = 1, B = 0, clpz:(0#>=C), clpz:(C in inf..3)    % unexpected
;  false.

And here the residual should be just C inf..0 if that would be a meaningful result, but due to B = 0 that is impossible

[triska]

It seems to me that this issue is connected to simultaneous unifications.

@mthom, please consider this example, which works as intended:

?- A in 0..1, B in 1..3,A*B#>C,labeling([],[A,B]), B = 1, A = 1, C = 0.
%@    A = 1, B = 1, C = 0
%@ ;  false.

However, when I perform the last two unifications simultaneously, I get:

?- A in 0..1, B in 1..3,A*B#>C,labeling([],[A,B]), B = 1, v(A,C) = v(1,0).
%@    A = 1, B = 1, C = 0
%@ ;  A = 1, B = 1, C = 0
%@ ;  false.

In such cases (A-C = X-Y), all newly created bindings must be undone before verify_attributes/3 is invoked. Is this currently the case?

One naive (and possibly slower) workaround is to queue all bindings, and then work them off one after the other. For instance, in the cases above, v(A,C) = v(1,0) would be internally treated as A = 1, followed by C = 0, with verify_attributes/3 invoked after each such binding.