Dif/2 call as implication premiss: is the implication's else part run? Should it be?

The general rule of thumb is that constraints and cuts (and thus if-then-else and negation) do not play together. It only works if all relevant constraints are resolved before committing. That is in general hard to predict. Constraint solvers have in general incomplete propagation and thus may have pending constraints even in cases where all constraints can be resolved. At debug time, call_residue_vars/2 can be used to verify there are no pending constraints. The implementation is fairly costly in terms of additional bookkeeping that, for example, protects constraints against garbage collection. This may prohibit usage at runtime.

2 Likes