{"abstract":"The last case of every tableswitch is unreachable.","category":"Bytecode virtual machines","checks":8,"contract":"code is a method's bytes; at addr is tableswitch (0xAA) or lookupswitch (0xAB). After the opcode, 0-3 padding bytes align the next byte to a multiple of 4 from the method start; then big-endian signed 32-bit words: default, and either low, high and high-low+1 offsets, or npairs followed by sorted (match, offset) pairs. Branch offsets are relative to the switch opcode address. Return the target address, or [\"VerifyError\", reason] for low > high, negative npairs, keys not strictly increasing, another opcode, or truncated operands.","contract_signature":"code, addr, key","evaluation_group":"w2-bytecode-virtual-machines-switch-dispatch","failed_approach":"Excluding low instead makes the first case unreachable.","family":"w2-bytecode-virtual-machines-switch-dispatch-table-bounds-inclusivity","id":"FA-90271","implementations":{"attempt":{"sha256":"9bc30a897a318367d4d06c0bca8d4d31ec56cd2891ebceb7b989d89496cba89f","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(code, addr, key):\n def s32(p):\n v = (code[p] << 24) | (code[p + 1] << 16) | (code[p + 2] << 8) | code[p + 3]\n return v - (1 << 32) if v & 0x80000000 else v\n def dispatch():\n op = code[addr]\n p = addr + 1\n p += (4 - p % 4) % 4\n default = s32(p)\n if op == 0xAA:\n low, high = s32(p + 4), s32(p + 8)\n if low > high:\n return ['VerifyError', 'low>high']\n if low < key <= high:\n return addr + s32(p + 12 + 4 * (key - low))\n return addr + default\n if op == 0xAB:\n npairs = s32(p + 4)\n if npairs < 0:\n return ['VerifyError', 'npairs']\n pairs = [(s32(p + 8 + 8 * i), s32(p + 12 + 8 * i)) for i in range(npairs)]\n if any(pairs[i][0] >= pairs[i + 1][0] for i in range(npairs - 1)):\n return ['VerifyError', 'unsorted']\n lo, hi = 0, npairs - 1\n while lo <= hi:\n mid = (lo + hi) // 2\n if pairs[mid][0] == key:\n return addr + pairs[mid][1]\n if pairs[mid][0] < key:\n lo = mid + 1\n else:\n hi = mid - 1\n return addr + default\n return ['VerifyError', 'opcode']\n try:\n return dispatch()\n except IndexError:\n return ['VerifyError', 'truncated']\ndef check(label, actual, expected):\n observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncases = [[('regression: tableswitch hit with aligned operands',\n ([0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 170,\n 255,\n 255,\n 255,\n 248,\n 255,\n 255,\n 255,\n 254,\n 0,\n 0,\n 0,\n 1,\n 0,\n 0,\n 0,\n 20,\n 0,\n 0,\n 0,\n 31,\n 0,\n 0,\n 0,\n 40,\n 0,\n 0,\n 0,\n 50,\n 177],\n 7,\n 0),\n 47),\n ('tableswitch hit at the high bound',\n ([0,\n 170,\n 0,\n 0,\n 255,\n 255,\n 255,\n 248,\n 255,\n 255,\n 255,\n 254,\n 0,\n 0,\n 0,\n 1,\n 0,\n 0,\n 0,\n 20,\n 0,\n 0,\n 0,\n 31,\n 0,\n 0,\n 0,\n 40,\n 0,\n 0,\n 0,\n 50,\n 177],\n 1,\n 1),\n 51),\n ('tableswitch hit at the low bound',\n ([0,\n 0,\n 170,\n 0,\n 255,\n 255,\n 255,\n 248,\n 255,\n 255,\n 255,\n 254,\n 0,\n 0,\n 0,\n 1,\n 0,\n 0,\n 0,\n 20,\n 0,\n 0,\n 0,\n 31,\n 0,\n 0,\n 0,\n 40,\n 0,\n 0,\n 0,\n 50,\n 177],\n 2,\n -2),\n 22),\n ('tableswitch miss takes the backward default',\n ([0,\n 170,\n 0,\n 0,\n 255,\n 255,\n 255,\n 248,\n 255,\n 255,\n 255,\n 254,\n 0,\n 0,\n 0,\n 1,\n 0,\n 0,\n 0,\n 20,\n 0,\n 0,\n 0,\n 31,\n 0,\n 0,\n 0,\n 40,\n 0,\n 0,\n 0,\n 50,\n 177],\n 1,\n 5),\n -7),\n ('lookupswitch hit with negative offset',\n ([0,\n 171,\n 0,\n 0,\n 0,\n 0,\n 0,\n 12,\n 0,\n 0,\n 0,\n 4,\n 255,\n 255,\n 255,\n 251,\n 0,\n 0,\n 0,\n 16,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 24,\n 0,\n 0,\n 0,\n 7,\n 0,\n 0,\n 0,\n 33,\n 0,\n 0,\n 0,\n 100,\n 255,\n 255,\n 255,\n 252,\n 177],\n 1,\n 100),\n -3),\n ('lookupswitch miss',\n ([0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 171,\n 0,\n 0,\n 0,\n 12,\n 0,\n 0,\n 0,\n 4,\n 255,\n 255,\n 255,\n 251,\n 0,\n 0,\n 0,\n 16,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 24,\n 0,\n 0,\n 0,\n 7,\n 0,\n 0,\n 0,\n 33,\n 0,\n 0,\n 0,\n 100,\n 255,\n 255,\n 255,\n 252,\n 177],\n 7,\n 3),\n 19),\n ('lookupswitch with duplicate keys is rejected',\n ([0, 171, 0, 0, 0, 0, 0, 12, 0, 0, 0, 2, 0, 0, 0, 1, 0, 0, 0, 8, 0, 0, 0, 1, 0, 0, 0, 12, 177], 1, 1),\n ['VerifyError', 'unsorted']),\n ('control: low greater than high',\n ([0, 170, 0, 0, 0, 0, 0, 4, 0, 0, 0, 5, 0, 0, 0, 2, 177], 1, 3),\n ['VerifyError', 'low>high'])],\n [('regression: tableswitch hit with aligned operands',\n ([0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 170,\n 255,\n 255,\n 255,\n 248,\n 255,\n 255,\n 255,\n 254,\n 0,\n 0,\n 0,\n 1,\n 0,\n 0,\n 0,\n 20,\n 0,\n 0,\n 0,\n 32,\n 0,\n 0,\n 0,\n 40,\n 0,\n 0,\n 0,\n 50,\n 177],\n 11,\n 0),\n 51),\n ('tableswitch hit at the high bound',\n ([0,\n 0,\n 170,\n 0,\n 255,\n 255,\n 255,\n 248,\n 255,\n 255,\n 255,\n 254,\n 0,\n 0,\n 0,\n 1,\n 0,\n 0,\n 0,\n 20,\n 0,\n 0,\n 0,\n 32,\n 0,\n 0,\n 0,\n 40,\n 0,\n 0,\n 0,\n 50,\n 177],\n 2,\n 1),\n 52),\n ('tableswitch hit at the low bound',\n ([0,\n 0,\n 0,\n 170,\n 255,\n 255,\n 255,\n 248,\n 255,\n 255,\n 255,\n 254,\n 0,\n 0,\n 0,\n 1,\n 0,\n 0,\n 0,\n 20,\n 0,\n 0,\n 0,\n 32,\n 0,\n 0,\n 0,\n 40,\n 0,\n 0,\n 0,\n 50,\n 177],\n 3,\n -2),\n 23),\n ('tableswitch miss takes the backward default',\n ([0,\n 0,\n 170,\n 0,\n 255,\n 255,\n 255,\n 248,\n 255,\n 255,\n 255,\n 254,\n 0,\n 0,\n 0,\n 1,\n 0,\n 0,\n 0,\n 20,\n 0,\n 0,\n 0,\n 32,\n 0,\n 0,\n 0,\n 40,\n 0,\n 0,\n 0,\n 50,\n 177],\n 2,\n 5),\n -6),\n ('lookupswitch hit with negative offset',\n ([0,\n 0,\n 171,\n 0,\n 0,\n 0,\n 0,\n 12,\n 0,\n 0,\n 0,\n 4,\n 255,\n 255,\n 255,\n 251,\n 0,\n 0,\n 0,\n 16,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 24,\n 0,\n 0,\n 0,\n 7,\n 0,\n 0,\n 0,\n 34,\n 0,\n 0,\n 0,\n 100,\n 255,\n 255,\n 255,\n 252,\n 177],\n 2,\n 100),\n -2),\n ('lookupswitch miss',\n ([0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 171,\n 0,\n 0,\n 0,\n 12,\n 0,\n 0,\n 0,\n 4,\n 255,\n 255,\n 255,\n 251,\n 0,\n 0,\n 0,\n 16,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 24,\n 0,\n 0,\n 0,\n 7,\n 0,\n 0,\n 0,\n 34,\n 0,\n 0,\n 0,\n 100,\n 255,\n 255,\n 255,\n 252,\n 177],\n 11,\n 3),\n 23),\n ('lookupswitch with duplicate keys is rejected',\n ([0, 0, 171, 0, 0, 0, 0, 12, 0, 0, 0, 2, 0, 0, 0, 1, 0, 0, 0, 8, 0, 0, 0, 1, 0, 0, 0, 12, 177], 2, 1),\n ['VerifyError', 'unsorted']),\n ('control: low greater than high',\n ([0, 0, 170, 0, 0, 0, 0, 4, 0, 0, 0, 5, 0, 0, 0, 2, 177], 2, 3),\n ['VerifyError', 'low>high'])],\n [('regression: tableswitch hit with aligned operands',\n ([0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 170,\n 255,\n 255,\n 255,\n 248,\n 255,\n 255,\n 255,\n 254,\n 0,\n 0,\n 0,\n 1,\n 0,\n 0,\n 0,\n 20,\n 0,\n 0,\n 0,\n 33,\n 0,\n 0,\n 0,\n 40,\n 0,\n 0,\n 0,\n 50,\n 177],\n 15,\n 0),\n 55),\n ('tableswitch hit at the high bound',\n ([0,\n 0,\n 0,\n 170,\n 255,\n 255,\n 255,\n 248,\n 255,\n 255,\n 255,\n 254,\n 0,\n 0,\n 0,\n 1,\n 0,\n 0,\n 0,\n 20,\n 0,\n 0,\n 0,\n 33,\n 0,\n 0,\n 0,\n 40,\n 0,\n 0,\n 0,\n 50,\n 177],\n 3,\n 1),\n 53),\n ('tableswitch hit at the low bound',\n ([0,\n 0,\n 0,\n 0,\n 170,\n 0,\n 0,\n 0,\n 255,\n 255,\n 255,\n 248,\n 255,\n 255,\n 255,\n 254,\n 0,\n 0,\n 0,\n 1,\n 0,\n 0,\n 0,\n 20,\n 0,\n 0,\n 0,\n 33,\n 0,\n 0,\n 0,\n 40,\n 0,\n 0,\n 0,\n 50,\n 177],\n 4,\n -2),\n 24),\n ('tableswitch miss takes the backward default',\n ([0,\n 0,\n 0,\n 170,\n 255,\n 255,\n 255,\n 248,\n 255,\n 255,\n 255,\n 254,\n 0,\n 0,\n 0,\n 1,\n 0,\n 0,\n 0,\n 20,\n 0,\n 0,\n 0,\n 33,\n 0,\n 0,\n 0,\n 40,\n 0,\n 0,\n 0,\n 50,\n 177],\n 3,\n 5),\n -5),\n ('lookupswitch hit with negative offset',\n ([0,\n 0,\n 0,\n 171,\n 0,\n 0,\n 0,\n 12,\n 0,\n 0,\n 0,\n 4,\n 255,\n 255,\n 255,\n 251,\n 0,\n 0,\n 0,\n 16,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 24,\n 0,\n 0,\n 0,\n 7,\n 0,\n 0,\n 0,\n 35,\n 0,\n 0,\n 0,\n 100,\n 255,\n 255,\n 255,\n 252,\n 177],\n 3,\n 100),\n -1),\n ('lookupswitch miss',\n ([0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 171,\n 0,\n 0,\n 0,\n 12,\n 0,\n 0,\n 0,\n 4,\n 255,\n 255,\n 255,\n 251,\n 0,\n 0,\n 0,\n 16,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 24,\n 0,\n 0,\n 0,\n 7,\n 0,\n 0,\n 0,\n 35,\n 0,\n 0,\n 0,\n 100,\n 255,\n 255,\n 255,\n 252,\n 177],\n 15,\n 3),\n 27),\n ('lookupswitch with duplicate keys is rejected',\n ([0, 0, 0, 171, 0, 0, 0, 12, 0, 0, 0, 2, 0, 0, 0, 1, 0, 0, 0, 8, 0, 0, 0, 1, 0, 0, 0, 12, 177], 3, 1),\n ['VerifyError', 'unsorted']),\n ('control: low greater than high',\n ([0, 0, 0, 170, 0, 0, 0, 4, 0, 0, 0, 5, 0, 0, 0, 2, 177], 3, 3),\n ['VerifyError', 'low>high'])],\n [('regression: tableswitch hit with aligned operands',\n ([0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 170,\n 255,\n 255,\n 255,\n 248,\n 255,\n 255,\n 255,\n 254,\n 0,\n 0,\n 0,\n 1,\n 0,\n 0,\n 0,\n 20,\n 0,\n 0,\n 0,\n 34,\n 0,\n 0,\n 0,\n 40,\n 0,\n 0,\n 0,\n 50,\n 177],\n 19,\n 0),\n 59),\n ('tableswitch hit at the high bound',\n ([0,\n 0,\n 0,\n 0,\n 170,\n 0,\n 0,\n 0,\n 255,\n 255,\n 255,\n 248,\n 255,\n 255,\n 255,\n 254,\n 0,\n 0,\n 0,\n 1,\n 0,\n 0,\n 0,\n 20,\n 0,\n 0,\n 0,\n 34,\n 0,\n 0,\n 0,\n 40,\n 0,\n 0,\n 0,\n 50,\n 177],\n 4,\n 1),\n 54),\n ('tableswitch hit at the low bound',\n ([0,\n 0,\n 0,\n 0,\n 0,\n 170,\n 0,\n 0,\n 255,\n 255,\n 255,\n 248,\n 255,\n 255,\n 255,\n 254,\n 0,\n 0,\n 0,\n 1,\n 0,\n 0,\n 0,\n 20,\n 0,\n 0,\n 0,\n 34,\n 0,\n 0,\n 0,\n 40,\n 0,\n 0,\n 0,\n 50,\n 177],\n 5,\n -2),\n 25),\n ('tableswitch miss takes the backward default',\n ([0,\n 0,\n 0,\n 0,\n 170,\n 0,\n 0,\n 0,\n 255,\n 255,\n 255,\n 248,\n 255,\n 255,\n 255,\n 254,\n 0,\n 0,\n 0,\n 1,\n 0,\n 0,\n 0,\n 20,\n 0,\n 0,\n 0,\n 34,\n 0,\n 0,\n 0,\n 40,\n 0,\n 0,\n 0,\n 50,\n 177],\n 4,\n 5),\n -4),\n ('lookupswitch hit with negative offset',\n ([0,\n 0,\n 0,\n 0,\n 171,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 12,\n 0,\n 0,\n 0,\n 4,\n 255,\n 255,\n 255,\n 251,\n 0,\n 0,\n 0,\n 16,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 24,\n 0,\n 0,\n 0,\n 7,\n 0,\n 0,\n 0,\n 36,\n 0,\n 0,\n 0,\n 100,\n 255,\n 255,\n 255,\n 252,\n 177],\n 4,\n 100),\n 0),\n ('lookupswitch miss',\n ([0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 171,\n 0,\n 0,\n 0,\n 12,\n 0,\n 0,\n 0,\n 4,\n 255,\n 255,\n 255,\n 251,\n 0,\n 0,\n 0,\n 16,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 24,\n 0,\n 0,\n 0,\n 7,\n 0,\n 0,\n 0,\n 36,\n 0,\n 0,\n 0,\n 100,\n 255,\n 255,\n 255,\n 252,\n 177],\n 19,\n 3),\n 31),\n ('lookupswitch with duplicate keys is rejected',\n ([0, 0, 0, 0, 171, 0, 0, 0, 0, 0, 0, 12, 0, 0, 0, 2, 0, 0, 0, 1, 0, 0, 0, 8, 0, 0, 0, 1, 0, 0, 0, 12, 177],\n 4,\n 1),\n ['VerifyError', 'unsorted']),\n ('control: low greater than high',\n ([0, 0, 0, 0, 170, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 5, 0, 0, 0, 2, 177], 4, 3),\n ['VerifyError', 'low>high'])],\n [('regression: tableswitch hit with aligned operands',\n ([0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 170,\n 255,\n 255,\n 255,\n 248,\n 255,\n 255,\n 255,\n 254,\n 0,\n 0,\n 0,\n 1,\n 0,\n 0,\n 0,\n 20,\n 0,\n 0,\n 0,\n 35,\n 0,\n 0,\n 0,\n 40,\n 0,\n 0,\n 0,\n 50,\n 177],\n 23,\n 0),\n 63),\n ('tableswitch hit at the high bound',\n ([0,\n 0,\n 0,\n 0,\n 0,\n 170,\n 0,\n 0,\n 255,\n 255,\n 255,\n 248,\n 255,\n 255,\n 255,\n 254,\n 0,\n 0,\n 0,\n 1,\n 0,\n 0,\n 0,\n 20,\n 0,\n 0,\n 0,\n 35,\n 0,\n 0,\n 0,\n 40,\n 0,\n 0,\n 0,\n 50,\n 177],\n 5,\n 1),\n 55),\n ('tableswitch hit at the low bound',\n ([0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 170,\n 0,\n 255,\n 255,\n 255,\n 248,\n 255,\n 255,\n 255,\n 254,\n 0,\n 0,\n 0,\n 1,\n 0,\n 0,\n 0,\n 20,\n 0,\n 0,\n 0,\n 35,\n 0,\n 0,\n 0,\n 40,\n 0,\n 0,\n 0,\n 50,\n 177],\n 6,\n -2),\n 26),\n ('tableswitch miss takes the backward default',\n ([0,\n 0,\n 0,\n 0,\n 0,\n 170,\n 0,\n 0,\n 255,\n 255,\n 255,\n 248,\n 255,\n 255,\n 255,\n 254,\n 0,\n 0,\n 0,\n 1,\n 0,\n 0,\n 0,\n 20,\n 0,\n 0,\n 0,\n 35,\n 0,\n 0,\n 0,\n 40,\n 0,\n 0,\n 0,\n 50,\n 177],\n 5,\n 5),\n -3),\n ('lookupswitch hit with negative offset',\n ([0,\n 0,\n 0,\n 0,\n 0,\n 171,\n 0,\n 0,\n 0,\n 0,\n 0,\n 12,\n 0,\n 0,\n 0,\n 4,\n 255,\n 255,\n 255,\n 251,\n 0,\n 0,\n 0,\n 16,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 24,\n 0,\n 0,\n 0,\n 7,\n 0,\n 0,\n 0,\n 37,\n 0,\n 0,\n 0,\n 100,\n 255,\n 255,\n 255,\n 252,\n 177],\n 5,\n 100),\n 1),\n ('lookupswitch miss',\n ([0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 171,\n 0,\n 0,\n 0,\n 12,\n 0,\n 0,\n 0,\n 4,\n 255,\n 255,\n 255,\n 251,\n 0,\n 0,\n 0,\n 16,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 24,\n 0,\n 0,\n 0,\n 7,\n 0,\n 0,\n 0,\n 37,\n 0,\n 0,\n 0,\n 100,\n 255,\n 255,\n 255,\n 252,\n 177],\n 23,\n 3),\n 35),\n ('lookupswitch with duplicate keys is rejected',\n ([0, 0, 0, 0, 0, 171, 0, 0, 0, 0, 0, 12, 0, 0, 0, 2, 0, 0, 0, 1, 0, 0, 0, 8, 0, 0, 0, 1, 0, 0, 0, 12, 177],\n 5,\n 1),\n ['VerifyError', 'unsorted']),\n ('control: low greater than high',\n ([0, 0, 0, 0, 0, 170, 0, 0, 0, 0, 0, 4, 0, 0, 0, 5, 0, 0, 0, 2, 177], 5, 3),\n ['VerifyError', 'low>high'])]]\nfor label, args, expected in cases[N - 1]:\n check(label, solve(*args), expected)\nprint(json.dumps({\"observations\": observations, \"passed\": all(x[\"passed\"] for x in observations)}, ensure_ascii=False))\nraise SystemExit(0 if all(x[\"passed\"] for x in observations) else 1)\n"},"broken":{"sha256":"772622df8a3d1c461e4b16d4ce90ba4cb6d8dccd963bb54451976238ce852177","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(code, addr, key):\n def s32(p):\n v = (code[p] << 24) | (code[p + 1] << 16) | (code[p + 2] << 8) | code[p + 3]\n return v - (1 << 32) if v & 0x80000000 else v\n def dispatch():\n op = code[addr]\n p = addr + 1\n p += (4 - p % 4) % 4\n default = s32(p)\n if op == 0xAA:\n low, high = s32(p + 4), s32(p + 8)\n if low > high:\n return ['VerifyError', 'low>high']\n if low <= key < high:\n return addr + s32(p + 12 + 4 * (key - low))\n return addr + default\n if op == 0xAB:\n npairs = s32(p + 4)\n if npairs < 0:\n return ['VerifyError', 'npairs']\n pairs = [(s32(p + 8 + 8 * i), s32(p + 12 + 8 * i)) for i in range(npairs)]\n if any(pairs[i][0] >= pairs[i + 1][0] for i in range(npairs - 1)):\n return ['VerifyError', 'unsorted']\n lo, hi = 0, npairs - 1\n while lo <= hi:\n mid = (lo + hi) // 2\n if pairs[mid][0] == key:\n return addr + pairs[mid][1]\n if pairs[mid][0] < key:\n lo = mid + 1\n else:\n hi = mid - 1\n return addr + default\n return ['VerifyError', 'opcode']\n try:\n return dispatch()\n except IndexError:\n return ['VerifyError', 'truncated']\ndef check(label, actual, expected):\n observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncases = [[('regression: tableswitch hit with aligned operands',\n ([0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 170,\n 255,\n 255,\n 255,\n 248,\n 255,\n 255,\n 255,\n 254,\n 0,\n 0,\n 0,\n 1,\n 0,\n 0,\n 0,\n 20,\n 0,\n 0,\n 0,\n 31,\n 0,\n 0,\n 0,\n 40,\n 0,\n 0,\n 0,\n 50,\n 177],\n 7,\n 0),\n 47),\n ('tableswitch hit at the high bound',\n ([0,\n 170,\n 0,\n 0,\n 255,\n 255,\n 255,\n 248,\n 255,\n 255,\n 255,\n 254,\n 0,\n 0,\n 0,\n 1,\n 0,\n 0,\n 0,\n 20,\n 0,\n 0,\n 0,\n 31,\n 0,\n 0,\n 0,\n 40,\n 0,\n 0,\n 0,\n 50,\n 177],\n 1,\n 1),\n 51),\n ('tableswitch hit at the low bound',\n ([0,\n 0,\n 170,\n 0,\n 255,\n 255,\n 255,\n 248,\n 255,\n 255,\n 255,\n 254,\n 0,\n 0,\n 0,\n 1,\n 0,\n 0,\n 0,\n 20,\n 0,\n 0,\n 0,\n 31,\n 0,\n 0,\n 0,\n 40,\n 0,\n 0,\n 0,\n 50,\n 177],\n 2,\n -2),\n 22),\n ('tableswitch miss takes the backward default',\n ([0,\n 170,\n 0,\n 0,\n 255,\n 255,\n 255,\n 248,\n 255,\n 255,\n 255,\n 254,\n 0,\n 0,\n 0,\n 1,\n 0,\n 0,\n 0,\n 20,\n 0,\n 0,\n 0,\n 31,\n 0,\n 0,\n 0,\n 40,\n 0,\n 0,\n 0,\n 50,\n 177],\n 1,\n 5),\n -7),\n ('lookupswitch hit with negative offset',\n ([0,\n 171,\n 0,\n 0,\n 0,\n 0,\n 0,\n 12,\n 0,\n 0,\n 0,\n 4,\n 255,\n 255,\n 255,\n 251,\n 0,\n 0,\n 0,\n 16,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 24,\n 0,\n 0,\n 0,\n 7,\n 0,\n 0,\n 0,\n 33,\n 0,\n 0,\n 0,\n 100,\n 255,\n 255,\n 255,\n 252,\n 177],\n 1,\n 100),\n -3),\n ('lookupswitch miss',\n ([0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 171,\n 0,\n 0,\n 0,\n 12,\n 0,\n 0,\n 0,\n 4,\n 255,\n 255,\n 255,\n 251,\n 0,\n 0,\n 0,\n 16,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 24,\n 0,\n 0,\n 0,\n 7,\n 0,\n 0,\n 0,\n 33,\n 0,\n 0,\n 0,\n 100,\n 255,\n 255,\n 255,\n 252,\n 177],\n 7,\n 3),\n 19),\n ('lookupswitch with duplicate keys is rejected',\n ([0, 171, 0, 0, 0, 0, 0, 12, 0, 0, 0, 2, 0, 0, 0, 1, 0, 0, 0, 8, 0, 0, 0, 1, 0, 0, 0, 12, 177], 1, 1),\n ['VerifyError', 'unsorted']),\n ('control: low greater than high',\n ([0, 170, 0, 0, 0, 0, 0, 4, 0, 0, 0, 5, 0, 0, 0, 2, 177], 1, 3),\n ['VerifyError', 'low>high'])],\n [('regression: tableswitch hit with aligned operands',\n ([0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 170,\n 255,\n 255,\n 255,\n 248,\n 255,\n 255,\n 255,\n 254,\n 0,\n 0,\n 0,\n 1,\n 0,\n 0,\n 0,\n 20,\n 0,\n 0,\n 0,\n 32,\n 0,\n 0,\n 0,\n 40,\n 0,\n 0,\n 0,\n 50,\n 177],\n 11,\n 0),\n 51),\n ('tableswitch hit at the high bound',\n ([0,\n 0,\n 170,\n 0,\n 255,\n 255,\n 255,\n 248,\n 255,\n 255,\n 255,\n 254,\n 0,\n 0,\n 0,\n 1,\n 0,\n 0,\n 0,\n 20,\n 0,\n 0,\n 0,\n 32,\n 0,\n 0,\n 0,\n 40,\n 0,\n 0,\n 0,\n 50,\n 177],\n 2,\n 1),\n 52),\n ('tableswitch hit at the low bound',\n ([0,\n 0,\n 0,\n 170,\n 255,\n 255,\n 255,\n 248,\n 255,\n 255,\n 255,\n 254,\n 0,\n 0,\n 0,\n 1,\n 0,\n 0,\n 0,\n 20,\n 0,\n 0,\n 0,\n 32,\n 0,\n 0,\n 0,\n 40,\n 0,\n 0,\n 0,\n 50,\n 177],\n 3,\n -2),\n 23),\n ('tableswitch miss takes the backward default',\n ([0,\n 0,\n 170,\n 0,\n 255,\n 255,\n 255,\n 248,\n 255,\n 255,\n 255,\n 254,\n 0,\n 0,\n 0,\n 1,\n 0,\n 0,\n 0,\n 20,\n 0,\n 0,\n 0,\n 32,\n 0,\n 0,\n 0,\n 40,\n 0,\n 0,\n 0,\n 50,\n 177],\n 2,\n 5),\n -6),\n ('lookupswitch hit with negative offset',\n ([0,\n 0,\n 171,\n 0,\n 0,\n 0,\n 0,\n 12,\n 0,\n 0,\n 0,\n 4,\n 255,\n 255,\n 255,\n 251,\n 0,\n 0,\n 0,\n 16,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 24,\n 0,\n 0,\n 0,\n 7,\n 0,\n 0,\n 0,\n 34,\n 0,\n 0,\n 0,\n 100,\n 255,\n 255,\n 255,\n 252,\n 177],\n 2,\n 100),\n -2),\n ('lookupswitch miss',\n ([0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 171,\n 0,\n 0,\n 0,\n 12,\n 0,\n 0,\n 0,\n 4,\n 255,\n 255,\n 255,\n 251,\n 0,\n 0,\n 0,\n 16,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 24,\n 0,\n 0,\n 0,\n 7,\n 0,\n 0,\n 0,\n 34,\n 0,\n 0,\n 0,\n 100,\n 255,\n 255,\n 255,\n 252,\n 177],\n 11,\n 3),\n 23),\n ('lookupswitch with duplicate keys is rejected',\n ([0, 0, 171, 0, 0, 0, 0, 12, 0, 0, 0, 2, 0, 0, 0, 1, 0, 0, 0, 8, 0, 0, 0, 1, 0, 0, 0, 12, 177], 2, 1),\n ['VerifyError', 'unsorted']),\n ('control: low greater than high',\n ([0, 0, 170, 0, 0, 0, 0, 4, 0, 0, 0, 5, 0, 0, 0, 2, 177], 2, 3),\n ['VerifyError', 'low>high'])],\n [('regression: tableswitch hit with aligned operands',\n ([0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 170,\n 255,\n 255,\n 255,\n 248,\n 255,\n 255,\n 255,\n 254,\n 0,\n 0,\n 0,\n 1,\n 0,\n 0,\n 0,\n 20,\n 0,\n 0,\n 0,\n 33,\n 0,\n 0,\n 0,\n 40,\n 0,\n 0,\n 0,\n 50,\n 177],\n 15,\n 0),\n 55),\n ('tableswitch hit at the high bound',\n ([0,\n 0,\n 0,\n 170,\n 255,\n 255,\n 255,\n 248,\n 255,\n 255,\n 255,\n 254,\n 0,\n 0,\n 0,\n 1,\n 0,\n 0,\n 0,\n 20,\n 0,\n 0,\n 0,\n 33,\n 0,\n 0,\n 0,\n 40,\n 0,\n 0,\n 0,\n 50,\n 177],\n 3,\n 1),\n 53),\n ('tableswitch hit at the low bound',\n ([0,\n 0,\n 0,\n 0,\n 170,\n 0,\n 0,\n 0,\n 255,\n 255,\n 255,\n 248,\n 255,\n 255,\n 255,\n 254,\n 0,\n 0,\n 0,\n 1,\n 0,\n 0,\n 0,\n 20,\n 0,\n 0,\n 0,\n 33,\n 0,\n 0,\n 0,\n 40,\n 0,\n 0,\n 0,\n 50,\n 177],\n 4,\n -2),\n 24),\n ('tableswitch miss takes the backward default',\n ([0,\n 0,\n 0,\n 170,\n 255,\n 255,\n 255,\n 248,\n 255,\n 255,\n 255,\n 254,\n 0,\n 0,\n 0,\n 1,\n 0,\n 0,\n 0,\n 20,\n 0,\n 0,\n 0,\n 33,\n 0,\n 0,\n 0,\n 40,\n 0,\n 0,\n 0,\n 50,\n 177],\n 3,\n 5),\n -5),\n ('lookupswitch hit with negative offset',\n ([0,\n 0,\n 0,\n 171,\n 0,\n 0,\n 0,\n 12,\n 0,\n 0,\n 0,\n 4,\n 255,\n 255,\n 255,\n 251,\n 0,\n 0,\n 0,\n 16,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 24,\n 0,\n 0,\n 0,\n 7,\n 0,\n 0,\n 0,\n 35,\n 0,\n 0,\n 0,\n 100,\n 255,\n 255,\n 255,\n 252,\n 177],\n 3,\n 100),\n -1),\n ('lookupswitch miss',\n ([0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 171,\n 0,\n 0,\n 0,\n 12,\n 0,\n 0,\n 0,\n 4,\n 255,\n 255,\n 255,\n 251,\n 0,\n 0,\n 0,\n 16,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 24,\n 0,\n 0,\n 0,\n 7,\n 0,\n 0,\n 0,\n 35,\n 0,\n 0,\n 0,\n 100,\n 255,\n 255,\n 255,\n 252,\n 177],\n 15,\n 3),\n 27),\n ('lookupswitch with duplicate keys is rejected',\n ([0, 0, 0, 171, 0, 0, 0, 12, 0, 0, 0, 2, 0, 0, 0, 1, 0, 0, 0, 8, 0, 0, 0, 1, 0, 0, 0, 12, 177], 3, 1),\n ['VerifyError', 'unsorted']),\n ('control: low greater than high',\n ([0, 0, 0, 170, 0, 0, 0, 4, 0, 0, 0, 5, 0, 0, 0, 2, 177], 3, 3),\n ['VerifyError', 'low>high'])],\n [('regression: tableswitch hit with aligned operands',\n ([0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 170,\n 255,\n 255,\n 255,\n 248,\n 255,\n 255,\n 255,\n 254,\n 0,\n 0,\n 0,\n 1,\n 0,\n 0,\n 0,\n 20,\n 0,\n 0,\n 0,\n 34,\n 0,\n 0,\n 0,\n 40,\n 0,\n 0,\n 0,\n 50,\n 177],\n 19,\n 0),\n 59),\n ('tableswitch hit at the high bound',\n ([0,\n 0,\n 0,\n 0,\n 170,\n 0,\n 0,\n 0,\n 255,\n 255,\n 255,\n 248,\n 255,\n 255,\n 255,\n 254,\n 0,\n 0,\n 0,\n 1,\n 0,\n 0,\n 0,\n 20,\n 0,\n 0,\n 0,\n 34,\n 0,\n 0,\n 0,\n 40,\n 0,\n 0,\n 0,\n 50,\n 177],\n 4,\n 1),\n 54),\n ('tableswitch hit at the low bound',\n ([0,\n 0,\n 0,\n 0,\n 0,\n 170,\n 0,\n 0,\n 255,\n 255,\n 255,\n 248,\n 255,\n 255,\n 255,\n 254,\n 0,\n 0,\n 0,\n 1,\n 0,\n 0,\n 0,\n 20,\n 0,\n 0,\n 0,\n 34,\n 0,\n 0,\n 0,\n 40,\n 0,\n 0,\n 0,\n 50,\n 177],\n 5,\n -2),\n 25),\n ('tableswitch miss takes the backward default',\n ([0,\n 0,\n 0,\n 0,\n 170,\n 0,\n 0,\n 0,\n 255,\n 255,\n 255,\n 248,\n 255,\n 255,\n 255,\n 254,\n 0,\n 0,\n 0,\n 1,\n 0,\n 0,\n 0,\n 20,\n 0,\n 0,\n 0,\n 34,\n 0,\n 0,\n 0,\n 40,\n 0,\n 0,\n 0,\n 50,\n 177],\n 4,\n 5),\n -4),\n ('lookupswitch hit with negative offset',\n ([0,\n 0,\n 0,\n 0,\n 171,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 12,\n 0,\n 0,\n 0,\n 4,\n 255,\n 255,\n 255,\n 251,\n 0,\n 0,\n 0,\n 16,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 24,\n 0,\n 0,\n 0,\n 7,\n 0,\n 0,\n 0,\n 36,\n 0,\n 0,\n 0,\n 100,\n 255,\n 255,\n 255,\n 252,\n 177],\n 4,\n 100),\n 0),\n ('lookupswitch miss',\n ([0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 171,\n 0,\n 0,\n 0,\n 12,\n 0,\n 0,\n 0,\n 4,\n 255,\n 255,\n 255,\n 251,\n 0,\n 0,\n 0,\n 16,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 24,\n 0,\n 0,\n 0,\n 7,\n 0,\n 0,\n 0,\n 36,\n 0,\n 0,\n 0,\n 100,\n 255,\n 255,\n 255,\n 252,\n 177],\n 19,\n 3),\n 31),\n ('lookupswitch with duplicate keys is rejected',\n ([0, 0, 0, 0, 171, 0, 0, 0, 0, 0, 0, 12, 0, 0, 0, 2, 0, 0, 0, 1, 0, 0, 0, 8, 0, 0, 0, 1, 0, 0, 0, 12, 177],\n 4,\n 1),\n ['VerifyError', 'unsorted']),\n ('control: low greater than high',\n ([0, 0, 0, 0, 170, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 5, 0, 0, 0, 2, 177], 4, 3),\n ['VerifyError', 'low>high'])],\n [('regression: tableswitch hit with aligned operands',\n ([0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 170,\n 255,\n 255,\n 255,\n 248,\n 255,\n 255,\n 255,\n 254,\n 0,\n 0,\n 0,\n 1,\n 0,\n 0,\n 0,\n 20,\n 0,\n 0,\n 0,\n 35,\n 0,\n 0,\n 0,\n 40,\n 0,\n 0,\n 0,\n 50,\n 177],\n 23,\n 0),\n 63),\n ('tableswitch hit at the high bound',\n ([0,\n 0,\n 0,\n 0,\n 0,\n 170,\n 0,\n 0,\n 255,\n 255,\n 255,\n 248,\n 255,\n 255,\n 255,\n 254,\n 0,\n 0,\n 0,\n 1,\n 0,\n 0,\n 0,\n 20,\n 0,\n 0,\n 0,\n 35,\n 0,\n 0,\n 0,\n 40,\n 0,\n 0,\n 0,\n 50,\n 177],\n 5,\n 1),\n 55),\n ('tableswitch hit at the low bound',\n ([0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 170,\n 0,\n 255,\n 255,\n 255,\n 248,\n 255,\n 255,\n 255,\n 254,\n 0,\n 0,\n 0,\n 1,\n 0,\n 0,\n 0,\n 20,\n 0,\n 0,\n 0,\n 35,\n 0,\n 0,\n 0,\n 40,\n 0,\n 0,\n 0,\n 50,\n 177],\n 6,\n -2),\n 26),\n ('tableswitch miss takes the backward default',\n ([0,\n 0,\n 0,\n 0,\n 0,\n 170,\n 0,\n 0,\n 255,\n 255,\n 255,\n 248,\n 255,\n 255,\n 255,\n 254,\n 0,\n 0,\n 0,\n 1,\n 0,\n 0,\n 0,\n 20,\n 0,\n 0,\n 0,\n 35,\n 0,\n 0,\n 0,\n 40,\n 0,\n 0,\n 0,\n 50,\n 177],\n 5,\n 5),\n -3),\n ('lookupswitch hit with negative offset',\n ([0,\n 0,\n 0,\n 0,\n 0,\n 171,\n 0,\n 0,\n 0,\n 0,\n 0,\n 12,\n 0,\n 0,\n 0,\n 4,\n 255,\n 255,\n 255,\n 251,\n 0,\n 0,\n 0,\n 16,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 24,\n 0,\n 0,\n 0,\n 7,\n 0,\n 0,\n 0,\n 37,\n 0,\n 0,\n 0,\n 100,\n 255,\n 255,\n 255,\n 252,\n 177],\n 5,\n 100),\n 1),\n ('lookupswitch miss',\n ([0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 171,\n 0,\n 0,\n 0,\n 12,\n 0,\n 0,\n 0,\n 4,\n 255,\n 255,\n 255,\n 251,\n 0,\n 0,\n 0,\n 16,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 0,\n 24,\n 0,\n 0,\n 0,\n 7,\n 0,\n 0,\n 0,\n 37,\n 0,\n 0,\n 0,\n 100,\n 255,\n 255,\n 255,\n 252,\n 177],\n 23,\n 3),\n 35),\n ('lookupswitch with duplicate keys is rejected',\n ([0, 0, 0, 0, 0, 171, 0, 0, 0, 0, 0, 12, 0, 0, 0, 2, 0, 0, 0, 1, 0, 0, 0, 8, 0, 0, 0, 1, 0, 0, 0, 12, 177],\n 5,\n 1),\n ['VerifyError', 'unsorted']),\n ('control: low greater than high',\n ([0, 0, 0, 0, 0, 170, 0, 0, 0, 0, 0, 4, 0, 0, 0, 5, 0, 0, 0, 2, 177], 5, 3),\n ['VerifyError', 'low>high'])]]\nfor label, args, expected in cases[N - 1]:\n check(label, solve(*args), expected)\nprint(json.dumps({\"observations\": observations, \"passed\": all(x[\"passed\"] for x in observations)}, ensure_ascii=False))\nraise SystemExit(0 if all(x[\"passed\"] for x in observations) else 1)\n"}},"limitations":"A deterministic, bounded teaching model of one bytecode virtual machine mechanism with a stipulated instruction encoding; it is not a production VM and claims no conformance to any real specification. This reproducer isolates one failure mechanism. Results cover the supplied fixtures. Variants within a family share a test contract and should remain grouped when constructing evaluation splits. Related mechanisms with a shared evaluation_group must also remain together; these controlled models are not independent production incidents.","method":"Deterministic executable model with adversarial boundary fixtures.","provenance":{"created_by":"Failure Map","dependencies":"Python standard library","family":"w2-bytecode-virtual-machines-switch-dispatch-table-bounds-inclusivity","generated_at":"2026-09-29T14:51:25.170552+00:00","license":"CC0-1.0","python":"3.12.14","seed":1,"split":"open-access"},"relevance":"Switch opcodes combine alignment, signed decoding and relative targets in one instruction.","root_cause":"The range test excludes high.","sha256":"09c3da882c746446526b2f30f41c12da5ef65b0ed378fda4a0bcb7de463803a9","title":"Switch dispatch: high bound handled by default ยท case 01","variant":1,"variant_policy":"Five numbered records share a model and may reuse boundary fixtures.","verified":true,"visibility":"public","verification":{"attempt":{"elapsed_ms":40.757,"exit_code":1,"observations":[{"actual":47,"check":"regression: tableswitch hit with aligned operands","expected":47,"passed":true},{"actual":51,"check":"tableswitch hit at the high bound","expected":51,"passed":true},{"actual":-6,"check":"tableswitch hit at the low bound","expected":22,"passed":false},{"actual":-7,"check":"tableswitch miss takes the backward default","expected":-7,"passed":true},{"actual":-3,"check":"lookupswitch hit with negative offset","expected":-3,"passed":true},{"actual":19,"check":"lookupswitch miss","expected":19,"passed":true},{"actual":["VerifyError","unsorted"],"check":"lookupswitch with duplicate keys is rejected","expected":["VerifyError","unsorted"],"passed":true},{"actual":["VerifyError","low>high"],"check":"control: low greater than high","expected":["VerifyError","low>high"],"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"regression: tableswitch hit with aligned operands\", \"actual\": 47, \"expected\": 47, \"passed\": true}, {\"check\": \"tableswitch hit at the high bound\", \"actual\": 51, \"expected\": 51, \"passed\": true}, {\"check\": \"tableswitch hit at the low bound\", \"actual\": -6, \"expected\": 22, \"passed\": false}, {\"check\": \"tableswitch miss takes the backward default\", \"actual\": -7, \"expected\": -7, \"passed\": true}, {\"check\": \"lookupswitch hit with negative offset\", \"actual\": -3, \"expected\": -3, \"passed\": true}, {\"check\": \"lookupswitch miss\", \"actual\": 19, \"expected\": 19, \"passed\": true}, {\"check\": \"lookupswitch with duplicate keys is rejected\", \"actual\": [\"VerifyError\", \"unsorted\"], \"expected\": [\"VerifyError\", \"unsorted\"], \"passed\": true}, {\"check\": \"control: low greater than high\", \"actual\": [\"VerifyError\", \"low>high\"], \"expected\": [\"VerifyError\", \"low>high\"], \"passed\": true}], \"passed\": false}\n"},"broken":{"elapsed_ms":43.546,"exit_code":1,"observations":[{"actual":47,"check":"regression: tableswitch hit with aligned operands","expected":47,"passed":true},{"actual":-7,"check":"tableswitch hit at the high bound","expected":51,"passed":false},{"actual":22,"check":"tableswitch hit at the low bound","expected":22,"passed":true},{"actual":-7,"check":"tableswitch miss takes the backward default","expected":-7,"passed":true},{"actual":-3,"check":"lookupswitch hit with negative offset","expected":-3,"passed":true},{"actual":19,"check":"lookupswitch miss","expected":19,"passed":true},{"actual":["VerifyError","unsorted"],"check":"lookupswitch with duplicate keys is rejected","expected":["VerifyError","unsorted"],"passed":true},{"actual":["VerifyError","low>high"],"check":"control: low greater than high","expected":["VerifyError","low>high"],"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"regression: tableswitch hit with aligned operands\", \"actual\": 47, \"expected\": 47, \"passed\": true}, {\"check\": \"tableswitch hit at the high bound\", \"actual\": -7, \"expected\": 51, \"passed\": false}, {\"check\": \"tableswitch hit at the low bound\", \"actual\": 22, \"expected\": 22, \"passed\": true}, {\"check\": \"tableswitch miss takes the backward default\", \"actual\": -7, \"expected\": -7, \"passed\": true}, {\"check\": \"lookupswitch hit with negative offset\", \"actual\": -3, \"expected\": -3, \"passed\": true}, {\"check\": \"lookupswitch miss\", \"actual\": 19, \"expected\": 19, \"passed\": true}, {\"check\": \"lookupswitch with duplicate keys is rejected\", \"actual\": [\"VerifyError\", \"unsorted\"], \"expected\": [\"VerifyError\", \"unsorted\"], \"passed\": true}, {\"check\": \"control: low greater than high\", \"actual\": [\"VerifyError\", \"low>high\"], \"expected\": [\"VerifyError\", \"low>high\"], \"passed\": true}], \"passed\": false}\n"}},"member_only":{"stages":["fixed"],"fields":["implementations.fixed","verification.fixed","harness","repair"],"note":"The verified repair, its recorded checks, the repair description, and the scoring harness are available to members."}}