This essentially just ignores the issue in the int domains (specifically the reduced product of them) instead of fixing it. I don't think this is the right solution because it still violates the narrowing property $a \sqcap b \sqsubseteq a \mathbin{\Delta} b \sqsubseteq a$. If $a = b$, then this reduces to $a \sqsubseteq a \mathbin{\Delta} a \sqsubseteq a$, which implies $a \mathbin{\Delta} a = a$. The TD3 paper makes this assumption, so we can't just gloss over this.

Before this, HConsed presented to TD3 a narrowing which obeys this property. It only failed the additional verification for suddenly becoming more precise. After this, the narrow presented to TD3 fails this property, so TD3 might no longer behave as it's supposed to.

What it essentially means is that a stable sequence might become unstable out of nowhere, instead of remaining ultimately stable. Therefore, the TD3 termination proof falls apart.

Ok, we can argue that this should not close the issue then, and the issue should be renamed ("invalid narrowing in the presence of refinement" or something).

However, I still think it is an improvement: The main thing this currently does is make the behavior consistent between having hash-consing on or off. Hash-consing should be a performance optimization only, there should not be any difference observable between the case where it is enabled or disabled. This conflates issues unnecessarily.

The point where your concern applies is immediately when we define the meet and narrow to refine, violating the properties you described above. Hashconsing accidentally fixing that again is not really the way to go.

Edit: Might also be interesting to see to what extent it is relevant that the concretizations remain the same in both cases.

Relevant paper by Cortesi: https://www.dsi.unive.it/~cortesi/paperi/CL_2011.pdf

Actually, narrow not being idempotent might not be a problem for termination in practice. It might be in the proof but in practice we don't check if the sequence is ultimately stable. We only check if it's stable for one iteration and end narrowing there. Unlike widening, it's perfectly fine to end narrowing at any point. It doesn't even have to reach one step stability. We can just get a less precise result maybe.

That narrowing property is just what implies that one step stability means ultimate stability.

Merging this as per discussion at the GobCon yesterday.