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.