#switchMatch function causes invalid branches

The #switchMatch function used in the implementation of SwitchInt (via selectBlock):

  syntax Bool ::= #switchMatch   ( MIRInt , TypedValue ) [function]

  rule #switchMatch(0, typedValue(BoolVal(B)           , _, _)) => notBool B
  rule #switchMatch(1, typedValue(BoolVal(B)           , _, _)) => B
  rule #switchMatch(I, typedValue(Integer(I2, WIDTH, _), _, _)) => I ==Int bitRangeInt(I2, 0, WIDTH)

There are two potential problems:

• (minor) the symbolic backend does not have a bitRangeInt hook. We should use truncate instead, which is a simple bitmask here (result is unsigned).
• (major) The way it is defined allows #switchMatch to yield true for more than one case, e.g. #switchMatch(0, <expression>) and #switchMatch(1, <expression>) can both be in the same path condition (This has been observed in symbolic execution traces). This is conceptually not possible, at most one instance for the 1st argument may yield true for the same <expression> as the 2nd argument.
  The second issue is particularly relevant in interaction with #lookupDiscriminant

Start at the #switchMatch definition used by SwitchInt through selectBlock, and inspect how it interacts with #lookupDiscriminant in symbolic execution traces. Check the existing bitRangeInt usage and symbolic backend support; done means truncation is supported there and one expression cannot make multiple switch branches true on the same path.