We need to improve the simplification of expressions with various variable instances.
We could try to do something similar to constant propagation, and to flattening variable derivation chains.
For example:

Here I would want the most simplified version to be something like "b >= 100 && b + 100" is not a subtype of Byte(b). Then
We could try using constraint simplification via equivalence analysis, as an algorithm like:
- Find equivalences (in variables for this case)
- Pick canonical names - use vars from code and not internal vars if possible
- Substitute Equivalences - Simplify equivalences, remove duplicate checks
- Remove redundancies
In that example:
- Equivalences:
{b, b_34, b_38}
- Use
b
#b_39 == #b_38 + 100 → #b_39 == b + 100
#b_38 == #b_34 → (redundant, defines equivalence)
#b_34 >= 100 → b >= 100
b > 0 → b > 0
#b_34 > 0 → b > 0 (duplicate)
b == #b_34 → (redundant, defines equivalence)
simplifies to
#b_39 == b + 100 && b >= 100 && b > 0
4) b > 100 -> b > 0 so we can drop the weaker constraint.
This is open for discussion!