Array bounds failure

.js

'reach 0.1';

export const main = Reach.App(() => {
  const Alice = Participant('Alice', {
    noticeAlice: Fun([], Null),
  });
  const Bob = Participant('Bob', {
    noticeBob: Fun([], Null),
  });
  deploy();
  const arr = array(UInt, [0, 1, 2, 3, 4]);

  Anybody.publish();

  var i = 0;
  invariant(balance() == 0);
  while (i < 8) {
    commit();
    Anybody.publish();

    const temp = i < 5 ? arr[i] : i;
    i = i + 1;
    continue;
  }

  commit();
  exit();
});

//------------------------------------

/*
❯ ./reach compile
Verifying knowledge assertions
Verifying for generic connector
  Verifying when ALL participants are honest
Verification failed:
  when ALL participants are honest
  of theorem: assert
  msg: "array bounds check"
  at ./index.rsh:21:29:array ref

  // Violation witness
  const i/22 = 5;
  //    ^ from loop variable at ./index.rsh:17:3:while

  // Theorem formalization
  assert(i/22 < 5);

Verification failed:
  when ALL participants are honest
  of theorem: assert
  msg: "array bounds check"
  at ./index.rsh:21:29:array ref

  (details omitted on repeat)
Verification failed:
  when ALL participants are honest
  of theorem: assert
  msg: "array bounds check"
  at ./index.rsh:21:29:array ref

  (details omitted on repeat)
Verification failed:
  when ALL participants are honest
  of theorem: assert
  msg: "array bounds check"
  at ./index.rsh:21:29:array ref

  (details omitted on repeat)
  Verifying when NO participants are honest
Verification failed:
  when NO participants are honest
  of theorem: assert
  msg: "array bounds check"
  at ./index.rsh:21:29:array ref

  (details omitted on repeat)
Verification failed:
  when NO participants are honest
  of theorem: assert
  msg: "array bounds check"
  at ./index.rsh:21:29:array ref

  (details omitted on repeat)
Verification failed:
  when NO participants are honest
  of theorem: assert
  msg: "array bounds check"
  at ./index.rsh:21:29:array ref

  (details omitted on repeat)
Verification failed:
  when NO participants are honest
  of theorem: assert
  msg: "array bounds check"
  at ./index.rsh:21:29:array ref

  (details omitted on repeat)
  Verifying when ONLY "Alice" is honest
Verification failed:
  when ONLY "Alice" is honest
  of theorem: assert
  msg: "array bounds check"
  at ./index.rsh:21:29:array ref

  (details omitted on repeat)
Verification failed:
  when ONLY "Alice" is honest
  of theorem: assert
  msg: "array bounds check"
  at ./index.rsh:21:29:array ref

  (details omitted on repeat)
Verification failed:
  when ONLY "Alice" is honest
  of theorem: assert
  msg: "array bounds check"
  at ./index.rsh:21:29:array ref

  (details omitted on repeat)
Verification failed:
  when ONLY "Alice" is honest
  of theorem: assert
  msg: "array bounds check"
  at ./index.rsh:21:29:array ref

  (details omitted on repeat)
  Verifying when ONLY "Bob" is honest
Verification failed:
  when ONLY "Bob" is honest
  of theorem: assert
  msg: "array bounds check"
  at ./index.rsh:21:29:array ref

  (details omitted on repeat)
Verification failed:
  when ONLY "Bob" is honest
  of theorem: assert
  msg: "array bounds check"
  at ./index.rsh:21:29:array ref

  (details omitted on repeat)
Verification failed:
  when ONLY "Bob" is honest
  of theorem: assert
  msg: "array bounds check"
  at ./index.rsh:21:29:array ref

  (details omitted on repeat)
Verification failed:
  when ONLY "Bob" is honest
  of theorem: assert
  msg: "array bounds check"
  at ./index.rsh:21:29:array ref

  (details omitted on repeat)
Checked 54 theorems; 16 failures. :'(
*/