This is the discussion from #100 that is still relevant

The join in Def-Exc is not-associative:

a: Not {1}([-63,63]) 
b: 0
c: -1

join(a,b): Not {1}([-63,63]) 
join(join(a,b),c): Not {1}([-63,63])

join(b,c): Unknown int([-7,7]) 
join(a, join(b,c)): Unknown int([-63,63])

These exclusion sets have been explored in this SAS paper. In particular, Example 6 "any minimal quasi-join for the donut domain over intervals is non-associative". I haven't taken a very deep look at what remedies they suggest, but I think a deep read of that paper may be useful.

It seems that Def_Exc as it is currently implemented (on top of not being a lattice) is also not a quasi-lattice as defined in the SAS '13 paper.
For the quasi-lattice, they require the join to give a minimal upper bound on two values (but not necessarily a least upper bound, i.e. there may exists several minimal upper bounds that are incomparable).

For Def_Exc, this is violated for the join of Definite a and Definite b values as we in this case go to Excluded {} [r] for some range R, but there exists a smaller element in the domain namely Excluded { r | r in R, r !=a, r != b} [r]. However, excluding everything in the range except a and b is the same as keeping a definite set of values, so this is definitely undesirable.

In order to make it at least into a quasi-lattice, it would be possible to limit the number of excluded values. But then these would be chosen randomly, so this is probably not desirable either.

The interesting questions is if we leave Def_Exc as it is (and accept that is neither lattice nor quasi-lattice), can this cause solving to not terminate or some other weird issue?

Vesal's idea: Maybe the safest approach is to limit the content of these sets to only zero and constant values that occur in case statements (or all conditional guards). If we have a fixed finite subset of select values V after pre-processing, the least upper bound of definite values is expanded to all other values a ⊔ b = Excl (V \ {a,b}). This should be safe, but it can impact performance. We have to normalize the sets after operations, so one can't preserve (x != 0) after x++; x-- unless 1 is in V. I don't think it's that's a serious drawback, but I also don't know if non-termination is caused by this for the solvers we use. It would be good to know more certainly if this can cause non-termination for the TD3 solver.