I'm using GNU Prolog. If I ask:
| ?- X #= Y+1, Y #< 4, Y #\= 2.
I get:
X = _#20(1..4)
Y = _#3(0..1:3)
but, since Y!=2 and X=Y+1, I was expecting also that X!=3.
What is this behavior due to?
Constraint solving over integers works by maintaining, for each variable, a domain (set of possible values). When a constraint is added, a consistency algorithm is responsible of updating the domain of involved variables by removing some impossible values. Indeed, it would be too costly to remove all impossible values (and thus practically impossible). There are thus several consistency techniques which differ on their degree of precision (the more precise they are the longer they take to execute).
Generally, for equations, only the bounds of the domains (lower and upper value) are updated (this is called bound consistency). This is the case in your example with X #= Y+1. When Y #\= 2 is added, the domain of Y is modified (removing 2) but since this does not change neither its lower bound (0) nor its upper bound (3), the domain of X is not reconsidered. Hence the domains you obtain:
X = _#20(1..4)
Y = _#3(0..1:3)
The domains are thus an approximation : actual solutions only contain values in the domains but not all values of the domains are part of a solution. From the correctness point of view, this is not a problem, since at the end, a search phase (also called labeling) will discover solutions by trying remaining values in the domains. If an impossible value remains it will give rise to a failure and another value will be tried (see fd_labeling).
Finally, under gprolog, you can ask for a more precise consistency algorithm (called domain consistency / arc-consistency) where all values are tested one by one. For this we use X #=# Y+1 and we can see that 3 has been removed from the domain of X.
| ?- X #=# Y+1, Y #< 4, Y #\= 2.
X = _#20(1..2:4)
Y = _#3(0..1:3)
Obviously, this is more expensive in terms of execution time. On the other hand it will avoid testing more impossible values at labeling.