Wrong semantics of x86 instruction BT when operand is in memory

[vbgl]

The following (safe) program produces zero in Jasmin semantics but one when run on hardware after compilation.

export fn test() -> reg u8 {
  reg bool cf;
  stack u64[2] s;
  s[0] = 0;
  s[1] = 1;
  reg u64 ofs = 64;
  cf = #BT(s[0], ofs);
  reg u8 r = #SETcc(cf);
  return r;
}