There is a whole list of issues on the dif/2 constrained. See e.g. dif/2 incorrect Ⅴ · Issue #122 · SWI-Prolog/issues · GitHub. The original code was barely documented. In previous attempts to fix it I added some comments, but I’m even unsure all are correct. Surely the code is still broken 
There is a simple implementation that has thus far always proved correct:
dif(X,Y) :- when(?=(X,Y), X \= Y).
This is in some scenarios rather inefficient and doesn’t give back a nice residual constraint in case the constraint is not yet resolved.
I do have some test helpers, among which predicates that generate random test cases, although Uwe Neumerkel seems to have better test case generators.
If someone is interested in resolving this, please contact me. A compensation can be negotiated.