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.