Create BitVec div-no-overflow check expression. Determines that BitVec arithmetic signed division does not overflow.