Here is a simple CLPFD relation:
1 #= 81 mod X.
This returns:
X in inf.. -1\/1..sup,
81 mod X#=1.
Unless my math is completely incorrect, shouldn't the domain of X be -80.. -1\/1..80?
First things first:
Is there a mistake in the constraint solver?
No(t necessarily), because all admissible solutions are still contained in the domain that is deduced, and no wrong solutions are reported. The domain that you deduced is a proper subset of what the solver reports.
Does the constraint solver propagate as well as it could in this case?
No, obviously not, as your stronger bounds already show. In fact, the admissible domain is even smaller than what you deduced: X in 2..80 would also be valid, because X can definitely not be negative, and it also cannot be equal to 1.
Exercise: Is X in 2..80 the smallest (with respect to set inclusion) domain that can be deduced in this case? Why (not)? And in what, if any, sense is it minimal?
So, what is going on here?
The explanation is rather easy: Implementing (mod)/2, (rem)/2, (div)/2 and—to somewhat lesser extent—even (*)/2 in such a way that they propagate as much as possible in all cases is brutally difficult to get right, and was clearly not done in this case.
Do we have to live with this shortcoming?
No, because we can improve the constraint solver to handle such cases too! That is, we can add logic so that it propagates more strongly! Doing this elegantly and correctly is an unsolved problem in general, and subject of active research. See for example Finite Domain Constraint Solver Learning, the references included therein, and several other papers. Of course, the dream would be to somehow derive the propagation directly from the specification of these operations, which is at least decades away. Until then, such issues are found and improved rather ad hoc.