clpz: somehow incorrect

[UWN]

?- v(B,C,D)=v(-2,-1,-2), [B,C,D]ins-2..0,0#==>B#>C/D.
   false.
?-                       [B,C,D]ins-2..0,0#==>B#>C/D,labeling([],[B,C,D]), v(B,C,D)=v(-2,-1,-2).
   B = -2, C = -1, D = -2
;  false.

At least one here must be incorrect.

[UWN]

Shorter:

?- D= -2, D in-2..0,0#==> -2#> -1/D.
   false.
?-        D in-2..0,0#==> -2#> -1/D, D = -2.
   D = -2
;  false, unexpected.

And where does this leftover choicepoint come from?

[UWN]

There are no comparable counterexamples with any three operators for div and //. Note that / is a rather special operator. All three try to mimic their counterparts in evaluable expressions:

?- X #= -1 // 2.
   X = 0.
?- X #= -1 div 2.
   X = -1.
?- X #= -1 / 2.
   false.
?- X is -1/2.
   X = -0.5.

Yet, (/)/2 is very special, as it fails. After all, its counterpart in evaluable expressions would be -0.5 which is not an integer. On the other hand they all fail for a zero divisor:

?- X #= -1 // 0.
   false.
?- X #= -1 div 0.
   false.
?- X #= -1 / 0.
   false.

So this situation is not that unique to (/)/2.

[UWN]

If this leftover choice point intended?

?- v(B,C,D)=v(-2,-1,-2), [B,C,D]ins-2..0,0#==>B#>C/D.
   B = -2, C = -1, D = -2
;  false. % unexpected leftover choice point

[triska]

The leftover choicepoint is due to #1502, this should ideally be addressed at the engine level for all such cases.

[UWN]

Ah, looks like #1028.

[triska]

With #1878 applied, I get:

?- v(B,C,D)=v(-2,-1,-2), [B,C,D]ins-2..0,0#==>B#>C/D.
   B = -2, C = -1, D = -2.