When modeling truncated differential paths, an XOR of two non-zero differences can lead to either no difference or some difference. However, in the first case, a linear constraint should be created. For example:
a + b = c with a, b, c on 8 bits, will be represented as A + B = C where A, B, C are binary values. However, in the case where C = 0 and A=B=1, we need to create separately a linear constrain a = b.
When modeling truncated differential paths, an XOR of two non-zero differences can lead to either no difference or some difference. However, in the first case, a linear constraint should be created. For example: a + b = c with a, b, c on 8 bits, will be represented as A + B = C where A, B, C are binary values. However, in the case where C = 0 and A=B=1, we need to create separately a linear constrain a = b.