code: private /*@ helper @*/ void multAddMe(int iv, int addend) {
          long v = iv & LONG_MASK;
          // unroll 0th iteration, doing addition.
          long p = v * (data[0] & LONG_MASK) + (addend & LONG_MASK);
          data[0] = (int) p;
          p >>>= 32;
          for (int i = 1; i < nWords; i++) {
              p += v * (data[i] & LONG_MASK);
              data[i] = (int) p;
              p >>>= 32;
          }
          if (p != 0L) {
              data[nWords++] = (int) p; // will fail noisily if illegal!
          }
      }
docs: /*@
  @ requires this.value()*UNSIGNED(iv) + UNSIGNED(addend) < ((\bigint)1) << ((this.data.length + this.offset)*32);
  @ assignable this.data[*];
  @ ensures this.value() == \old(this.value()*UNSIGNED(iv) + UNSIGNED(addend));
  @