Currently, the default (range-based) constraint manager supports symbolic expressions of the format symbol + integer or symbol - integer to compare them to another integer. However, multiplication and division is not supported yet.
An example where multiplication (and division) could be useful is the checking whether a pointer operation or an array index is out of the bounds of the memory region. The index is often a first-degree expression of the format a*x + b (e.g. for special sparse matrices, such as triangular ones).
In this patch we only support multiplication and division for two kinds of symbolic comparisons: the == and the != operators. The rest is to follow in a subsequent patch. Negative multipliers and divisors are not supported yet.
I believe that this code should be moved directly into getRange(). If it's about looking at a single symbol and figuring out what range information about it do we already have, it should go into getRange(). This way we don't need to duplicate it in all the assume...() functions, and also it's exactly what getRange() is supposed to accomplish.