{"abstract":"The bounded replacement selection certificate reports an incorrect next.","category":"Heap invariants","checks":7,"contract":"A replacement-selection external-sort heap receives last emitted key and new records [id,key]. Keys >=last remain active for current run; smaller keys freeze for next run. Return active ids, frozen ids, active sorted order, frozen sorted order, next current-run key, and end-run flag. Equal keys stay active.","evaluation_group":"s3-heap-model-replacement-selection","failed_approach":"The local patch uses last if not active else active[0][1] and still violates the stated relation.","family":"s3-heap-replacement-selection-next","id":"FA-41091","implementations":{"attempt":{"sha256":"adddc1321596adbde9cb5814967e2a37a84ae98211a62a127a481c8c19d7e5ea","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(d):\n    last=d['last']; a=d['arrivals']; active=[x for x in a if x[1]>=last]; frozen=[x for x in a if x[1]<last]\n    return {'active': [x[0] for x in active],\n    'frozen': [x[0] for x in frozen],\n    'active_order': [x[0] for x in sorted(active,key=lambda x:x[1])],\n    'frozen_order': [x[0] for x in sorted(frozen,key=lambda x:x[1])],\n    'next': last if not active else active[0][1],\n    'run_ended': not active}\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncases = [[({'last': 3, 'arrivals': []}, {'active': [], 'frozen': [], 'active_order': [], 'frozen_order': [], 'next': None, 'run_ended': True}), ({'last': 3, 'arrivals': [['a', 3]]}, {'active': ['a'], 'frozen': [], 'active_order': ['a'], 'frozen_order': [], 'next': 3, 'run_ended': False}), ({'last': 5, 'arrivals': [['a', 7], ['b', 2], ['c', 5], ['d', 1], ['e', 6]]}, {'active': ['a', 'c', 'e'], 'frozen': ['b', 'd'], 'active_order': ['c', 'e', 'a'], 'frozen_order': ['d', 'b'], 'next': 5, 'run_ended': False}), ({'last': 8, 'arrivals': [['a', 4], ['b', 2], ['c', 6]]}, {'active': [], 'frozen': ['a', 'b', 'c'], 'active_order': [], 'frozen_order': ['b', 'a', 'c'], 'next': None, 'run_ended': True}), ({'last': 0, 'arrivals': [['a', 3], ['b', 1], ['c', 2]]}, {'active': ['a', 'b', 'c'], 'frozen': [], 'active_order': ['b', 'c', 'a'], 'frozen_order': [], 'next': 1, 'run_ended': False}), ({'last': 4, 'arrivals': [['a', 4], ['b', 4], ['c', 3]]}, {'active': ['a', 'b'], 'frozen': ['c'], 'active_order': ['a', 'b'], 'frozen_order': ['c'], 'next': 4, 'run_ended': False}), ({'last': 5, 'arrivals': [['a', 4], ['b', 4], ['c', 3]]}, {'active': [], 'frozen': ['a', 'b', 'c'], 'active_order': [], 'frozen_order': ['c', 'a', 'b'], 'next': None, 'run_ended': True})], [({'last': 3, 'arrivals': []}, {'active': [], 'frozen': [], 'active_order': [], 'frozen_order': [], 'next': None, 'run_ended': True}), ({'last': 3, 'arrivals': [['a', 3]]}, {'active': ['a'], 'frozen': [], 'active_order': ['a'], 'frozen_order': [], 'next': 3, 'run_ended': False}), ({'last': 5, 'arrivals': [['a', 7], ['b', 2], ['c', 5], ['d', 1], ['e', 6]]}, {'active': ['a', 'c', 'e'], 'frozen': ['b', 'd'], 'active_order': ['c', 'e', 'a'], 'frozen_order': ['d', 'b'], 'next': 5, 'run_ended': False}), ({'last': 8, 'arrivals': [['a', 4], ['b', 2], ['c', 6]]}, {'active': [], 'frozen': ['a', 'b', 'c'], 'active_order': [], 'frozen_order': ['b', 'a', 'c'], 'next': None, 'run_ended': True}), ({'last': 0, 'arrivals': [['a', 3], ['b', 1], ['c', 2]]}, {'active': ['a', 'b', 'c'], 'frozen': [], 'active_order': ['b', 'c', 'a'], 'frozen_order': [], 'next': 1, 'run_ended': False}), ({'last': 4, 'arrivals': [['a', 4], ['b', 4], ['c', 3]]}, {'active': ['a', 'b'], 'frozen': ['c'], 'active_order': ['a', 'b'], 'frozen_order': ['c'], 'next': 4, 'run_ended': False}), ({'last': 6, 'arrivals': [['a', 4], ['b', 4], ['c', 3]]}, {'active': [], 'frozen': ['a', 'b', 'c'], 'active_order': [], 'frozen_order': ['c', 'a', 'b'], 'next': None, 'run_ended': True})], [({'last': 3, 'arrivals': []}, {'active': [], 'frozen': [], 'active_order': [], 'frozen_order': [], 'next': None, 'run_ended': True}), ({'last': 3, 'arrivals': [['a', 3]]}, {'active': ['a'], 'frozen': [], 'active_order': ['a'], 'frozen_order': [], 'next': 3, 'run_ended': False}), ({'last': 5, 'arrivals': [['a', 7], ['b', 2], ['c', 5], ['d', 1], ['e', 6]]}, {'active': ['a', 'c', 'e'], 'frozen': ['b', 'd'], 'active_order': ['c', 'e', 'a'], 'frozen_order': ['d', 'b'], 'next': 5, 'run_ended': False}), ({'last': 8, 'arrivals': [['a', 4], ['b', 2], ['c', 6]]}, {'active': [], 'frozen': ['a', 'b', 'c'], 'active_order': [], 'frozen_order': ['b', 'a', 'c'], 'next': None, 'run_ended': True}), ({'last': 0, 'arrivals': [['a', 3], ['b', 1], ['c', 2]]}, {'active': ['a', 'b', 'c'], 'frozen': [], 'active_order': ['b', 'c', 'a'], 'frozen_order': [], 'next': 1, 'run_ended': False}), ({'last': 4, 'arrivals': [['a', 4], ['b', 4], ['c', 3]]}, {'active': ['a', 'b'], 'frozen': ['c'], 'active_order': ['a', 'b'], 'frozen_order': ['c'], 'next': 4, 'run_ended': False}), ({'last': 7, 'arrivals': [['a', 4], ['b', 4], ['c', 3]]}, {'active': [], 'frozen': ['a', 'b', 'c'], 'active_order': [], 'frozen_order': ['c', 'a', 'b'], 'next': None, 'run_ended': True})], [({'last': 3, 'arrivals': []}, {'active': [], 'frozen': [], 'active_order': [], 'frozen_order': [], 'next': None, 'run_ended': True}), ({'last': 3, 'arrivals': [['a', 3]]}, {'active': ['a'], 'frozen': [], 'active_order': ['a'], 'frozen_order': [], 'next': 3, 'run_ended': False}), ({'last': 5, 'arrivals': [['a', 7], ['b', 2], ['c', 5], ['d', 1], ['e', 6]]}, {'active': ['a', 'c', 'e'], 'frozen': ['b', 'd'], 'active_order': ['c', 'e', 'a'], 'frozen_order': ['d', 'b'], 'next': 5, 'run_ended': False}), ({'last': 8, 'arrivals': [['a', 4], ['b', 2], ['c', 6]]}, {'active': [], 'frozen': ['a', 'b', 'c'], 'active_order': [], 'frozen_order': ['b', 'a', 'c'], 'next': None, 'run_ended': True}), ({'last': 0, 'arrivals': [['a', 3], ['b', 1], ['c', 2]]}, {'active': ['a', 'b', 'c'], 'frozen': [], 'active_order': ['b', 'c', 'a'], 'frozen_order': [], 'next': 1, 'run_ended': False}), ({'last': 4, 'arrivals': [['a', 4], ['b', 4], ['c', 3]]}, {'active': ['a', 'b'], 'frozen': ['c'], 'active_order': ['a', 'b'], 'frozen_order': ['c'], 'next': 4, 'run_ended': False}), ({'last': 8, 'arrivals': [['a', 4], ['b', 4], ['c', 3]]}, {'active': [], 'frozen': ['a', 'b', 'c'], 'active_order': [], 'frozen_order': ['c', 'a', 'b'], 'next': None, 'run_ended': True})], [({'last': 3, 'arrivals': []}, {'active': [], 'frozen': [], 'active_order': [], 'frozen_order': [], 'next': None, 'run_ended': True}), ({'last': 3, 'arrivals': [['a', 3]]}, {'active': ['a'], 'frozen': [], 'active_order': ['a'], 'frozen_order': [], 'next': 3, 'run_ended': False}), ({'last': 5, 'arrivals': [['a', 7], ['b', 2], ['c', 5], ['d', 1], ['e', 6]]}, {'active': ['a', 'c', 'e'], 'frozen': ['b', 'd'], 'active_order': ['c', 'e', 'a'], 'frozen_order': ['d', 'b'], 'next': 5, 'run_ended': False}), ({'last': 8, 'arrivals': [['a', 4], ['b', 2], ['c', 6]]}, {'active': [], 'frozen': ['a', 'b', 'c'], 'active_order': [], 'frozen_order': ['b', 'a', 'c'], 'next': None, 'run_ended': True}), ({'last': 0, 'arrivals': [['a', 3], ['b', 1], ['c', 2]]}, {'active': ['a', 'b', 'c'], 'frozen': [], 'active_order': ['b', 'c', 'a'], 'frozen_order': [], 'next': 1, 'run_ended': False}), ({'last': 4, 'arrivals': [['a', 4], ['b', 4], ['c', 3]]}, {'active': ['a', 'b'], 'frozen': ['c'], 'active_order': ['a', 'b'], 'frozen_order': ['c'], 'next': 4, 'run_ended': False}), ({'last': 9, 'arrivals': [['a', 4], ['b', 4], ['c', 3]]}, {'active': [], 'frozen': ['a', 'b', 'c'], 'active_order': [], 'frozen_order': ['c', 'a', 'b'], 'next': None, 'run_ended': True})]][N-1]\ncheck('regression certificate 1', solve(cases[0][0]), cases[0][1])\ncheck('regression certificate 2', solve(cases[1][0]), cases[1][1])\ncheck('regression certificate 3', solve(cases[2][0]), cases[2][1])\ncheck('regression certificate 4', solve(cases[3][0]), cases[3][1])\ncheck('regression certificate 5', solve(cases[4][0]), cases[4][1])\ncheck('regression certificate 6', solve(cases[5][0]), cases[5][1])\ncheck('variant-dependent certificate', solve(cases[6][0]), cases[6][1])\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":"0fb992832b611f2767f2aebad5912045795e21152e45bff4aab614a4a6883b9b","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(d):\n    last=d['last']; a=d['arrivals']; active=[x for x in a if x[1]>=last]; frozen=[x for x in a if x[1]<last]\n    return {'active': [x[0] for x in active],\n    'frozen': [x[0] for x in frozen],\n    'active_order': [x[0] for x in sorted(active,key=lambda x:x[1])],\n    'frozen_order': [x[0] for x in sorted(frozen,key=lambda x:x[1])],\n    'next': min((x[1] for x in a),default=None),\n    'run_ended': not active}\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncases = [[({'last': 3, 'arrivals': []}, {'active': [], 'frozen': [], 'active_order': [], 'frozen_order': [], 'next': None, 'run_ended': True}), ({'last': 3, 'arrivals': [['a', 3]]}, {'active': ['a'], 'frozen': [], 'active_order': ['a'], 'frozen_order': [], 'next': 3, 'run_ended': False}), ({'last': 5, 'arrivals': [['a', 7], ['b', 2], ['c', 5], ['d', 1], ['e', 6]]}, {'active': ['a', 'c', 'e'], 'frozen': ['b', 'd'], 'active_order': ['c', 'e', 'a'], 'frozen_order': ['d', 'b'], 'next': 5, 'run_ended': False}), ({'last': 8, 'arrivals': [['a', 4], ['b', 2], ['c', 6]]}, {'active': [], 'frozen': ['a', 'b', 'c'], 'active_order': [], 'frozen_order': ['b', 'a', 'c'], 'next': None, 'run_ended': True}), ({'last': 0, 'arrivals': [['a', 3], ['b', 1], ['c', 2]]}, {'active': ['a', 'b', 'c'], 'frozen': [], 'active_order': ['b', 'c', 'a'], 'frozen_order': [], 'next': 1, 'run_ended': False}), ({'last': 4, 'arrivals': [['a', 4], ['b', 4], ['c', 3]]}, {'active': ['a', 'b'], 'frozen': ['c'], 'active_order': ['a', 'b'], 'frozen_order': ['c'], 'next': 4, 'run_ended': False}), ({'last': 5, 'arrivals': [['a', 4], ['b', 4], ['c', 3]]}, {'active': [], 'frozen': ['a', 'b', 'c'], 'active_order': [], 'frozen_order': ['c', 'a', 'b'], 'next': None, 'run_ended': True})], [({'last': 3, 'arrivals': []}, {'active': [], 'frozen': [], 'active_order': [], 'frozen_order': [], 'next': None, 'run_ended': True}), ({'last': 3, 'arrivals': [['a', 3]]}, {'active': ['a'], 'frozen': [], 'active_order': ['a'], 'frozen_order': [], 'next': 3, 'run_ended': False}), ({'last': 5, 'arrivals': [['a', 7], ['b', 2], ['c', 5], ['d', 1], ['e', 6]]}, {'active': ['a', 'c', 'e'], 'frozen': ['b', 'd'], 'active_order': ['c', 'e', 'a'], 'frozen_order': ['d', 'b'], 'next': 5, 'run_ended': False}), ({'last': 8, 'arrivals': [['a', 4], ['b', 2], ['c', 6]]}, {'active': [], 'frozen': ['a', 'b', 'c'], 'active_order': [], 'frozen_order': ['b', 'a', 'c'], 'next': None, 'run_ended': True}), ({'last': 0, 'arrivals': [['a', 3], ['b', 1], ['c', 2]]}, {'active': ['a', 'b', 'c'], 'frozen': [], 'active_order': ['b', 'c', 'a'], 'frozen_order': [], 'next': 1, 'run_ended': False}), ({'last': 4, 'arrivals': [['a', 4], ['b', 4], ['c', 3]]}, {'active': ['a', 'b'], 'frozen': ['c'], 'active_order': ['a', 'b'], 'frozen_order': ['c'], 'next': 4, 'run_ended': False}), ({'last': 6, 'arrivals': [['a', 4], ['b', 4], ['c', 3]]}, {'active': [], 'frozen': ['a', 'b', 'c'], 'active_order': [], 'frozen_order': ['c', 'a', 'b'], 'next': None, 'run_ended': True})], [({'last': 3, 'arrivals': []}, {'active': [], 'frozen': [], 'active_order': [], 'frozen_order': [], 'next': None, 'run_ended': True}), ({'last': 3, 'arrivals': [['a', 3]]}, {'active': ['a'], 'frozen': [], 'active_order': ['a'], 'frozen_order': [], 'next': 3, 'run_ended': False}), ({'last': 5, 'arrivals': [['a', 7], ['b', 2], ['c', 5], ['d', 1], ['e', 6]]}, {'active': ['a', 'c', 'e'], 'frozen': ['b', 'd'], 'active_order': ['c', 'e', 'a'], 'frozen_order': ['d', 'b'], 'next': 5, 'run_ended': False}), ({'last': 8, 'arrivals': [['a', 4], ['b', 2], ['c', 6]]}, {'active': [], 'frozen': ['a', 'b', 'c'], 'active_order': [], 'frozen_order': ['b', 'a', 'c'], 'next': None, 'run_ended': True}), ({'last': 0, 'arrivals': [['a', 3], ['b', 1], ['c', 2]]}, {'active': ['a', 'b', 'c'], 'frozen': [], 'active_order': ['b', 'c', 'a'], 'frozen_order': [], 'next': 1, 'run_ended': False}), ({'last': 4, 'arrivals': [['a', 4], ['b', 4], ['c', 3]]}, {'active': ['a', 'b'], 'frozen': ['c'], 'active_order': ['a', 'b'], 'frozen_order': ['c'], 'next': 4, 'run_ended': False}), ({'last': 7, 'arrivals': [['a', 4], ['b', 4], ['c', 3]]}, {'active': [], 'frozen': ['a', 'b', 'c'], 'active_order': [], 'frozen_order': ['c', 'a', 'b'], 'next': None, 'run_ended': True})], [({'last': 3, 'arrivals': []}, {'active': [], 'frozen': [], 'active_order': [], 'frozen_order': [], 'next': None, 'run_ended': True}), ({'last': 3, 'arrivals': [['a', 3]]}, {'active': ['a'], 'frozen': [], 'active_order': ['a'], 'frozen_order': [], 'next': 3, 'run_ended': False}), ({'last': 5, 'arrivals': [['a', 7], ['b', 2], ['c', 5], ['d', 1], ['e', 6]]}, {'active': ['a', 'c', 'e'], 'frozen': ['b', 'd'], 'active_order': ['c', 'e', 'a'], 'frozen_order': ['d', 'b'], 'next': 5, 'run_ended': False}), ({'last': 8, 'arrivals': [['a', 4], ['b', 2], ['c', 6]]}, {'active': [], 'frozen': ['a', 'b', 'c'], 'active_order': [], 'frozen_order': ['b', 'a', 'c'], 'next': None, 'run_ended': True}), ({'last': 0, 'arrivals': [['a', 3], ['b', 1], ['c', 2]]}, {'active': ['a', 'b', 'c'], 'frozen': [], 'active_order': ['b', 'c', 'a'], 'frozen_order': [], 'next': 1, 'run_ended': False}), ({'last': 4, 'arrivals': [['a', 4], ['b', 4], ['c', 3]]}, {'active': ['a', 'b'], 'frozen': ['c'], 'active_order': ['a', 'b'], 'frozen_order': ['c'], 'next': 4, 'run_ended': False}), ({'last': 8, 'arrivals': [['a', 4], ['b', 4], ['c', 3]]}, {'active': [], 'frozen': ['a', 'b', 'c'], 'active_order': [], 'frozen_order': ['c', 'a', 'b'], 'next': None, 'run_ended': True})], [({'last': 3, 'arrivals': []}, {'active': [], 'frozen': [], 'active_order': [], 'frozen_order': [], 'next': None, 'run_ended': True}), ({'last': 3, 'arrivals': [['a', 3]]}, {'active': ['a'], 'frozen': [], 'active_order': ['a'], 'frozen_order': [], 'next': 3, 'run_ended': False}), ({'last': 5, 'arrivals': [['a', 7], ['b', 2], ['c', 5], ['d', 1], ['e', 6]]}, {'active': ['a', 'c', 'e'], 'frozen': ['b', 'd'], 'active_order': ['c', 'e', 'a'], 'frozen_order': ['d', 'b'], 'next': 5, 'run_ended': False}), ({'last': 8, 'arrivals': [['a', 4], ['b', 2], ['c', 6]]}, {'active': [], 'frozen': ['a', 'b', 'c'], 'active_order': [], 'frozen_order': ['b', 'a', 'c'], 'next': None, 'run_ended': True}), ({'last': 0, 'arrivals': [['a', 3], ['b', 1], ['c', 2]]}, {'active': ['a', 'b', 'c'], 'frozen': [], 'active_order': ['b', 'c', 'a'], 'frozen_order': [], 'next': 1, 'run_ended': False}), ({'last': 4, 'arrivals': [['a', 4], ['b', 4], ['c', 3]]}, {'active': ['a', 'b'], 'frozen': ['c'], 'active_order': ['a', 'b'], 'frozen_order': ['c'], 'next': 4, 'run_ended': False}), ({'last': 9, 'arrivals': [['a', 4], ['b', 4], ['c', 3]]}, {'active': [], 'frozen': ['a', 'b', 'c'], 'active_order': [], 'frozen_order': ['c', 'a', 'b'], 'next': None, 'run_ended': True})]][N-1]\ncheck('regression certificate 1', solve(cases[0][0]), cases[0][1])\ncheck('regression certificate 2', solve(cases[1][0]), cases[1][1])\ncheck('regression certificate 3', solve(cases[2][0]), cases[2][1])\ncheck('regression certificate 4', solve(cases[3][0]), cases[3][1])\ncheck('regression certificate 5', solve(cases[4][0]), cases[4][1])\ncheck('regression certificate 6', solve(cases[5][0]), cases[5][1])\ncheck('variant-dependent certificate', solve(cases[6][0]), cases[6][1])\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"},"fixed":{"sha256":"9e1e99e97427693a96676d3ebfcd8047b77347935d344db25c769f8be901d5b7","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(d):\n    last=d['last']; a=d['arrivals']; active=[x for x in a if x[1]>=last]; frozen=[x for x in a if x[1]<last]\n    return {'active': [x[0] for x in active],\n    'frozen': [x[0] for x in frozen],\n    'active_order': [x[0] for x in sorted(active,key=lambda x:x[1])],\n    'frozen_order': [x[0] for x in sorted(frozen,key=lambda x:x[1])],\n    'next': min((x[1] for x in active),default=None),\n    'run_ended': not active}\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncases = [[({'last': 3, 'arrivals': []}, {'active': [], 'frozen': [], 'active_order': [], 'frozen_order': [], 'next': None, 'run_ended': True}), ({'last': 3, 'arrivals': [['a', 3]]}, {'active': ['a'], 'frozen': [], 'active_order': ['a'], 'frozen_order': [], 'next': 3, 'run_ended': False}), ({'last': 5, 'arrivals': [['a', 7], ['b', 2], ['c', 5], ['d', 1], ['e', 6]]}, {'active': ['a', 'c', 'e'], 'frozen': ['b', 'd'], 'active_order': ['c', 'e', 'a'], 'frozen_order': ['d', 'b'], 'next': 5, 'run_ended': False}), ({'last': 8, 'arrivals': [['a', 4], ['b', 2], ['c', 6]]}, {'active': [], 'frozen': ['a', 'b', 'c'], 'active_order': [], 'frozen_order': ['b', 'a', 'c'], 'next': None, 'run_ended': True}), ({'last': 0, 'arrivals': [['a', 3], ['b', 1], ['c', 2]]}, {'active': ['a', 'b', 'c'], 'frozen': [], 'active_order': ['b', 'c', 'a'], 'frozen_order': [], 'next': 1, 'run_ended': False}), ({'last': 4, 'arrivals': [['a', 4], ['b', 4], ['c', 3]]}, {'active': ['a', 'b'], 'frozen': ['c'], 'active_order': ['a', 'b'], 'frozen_order': ['c'], 'next': 4, 'run_ended': False}), ({'last': 5, 'arrivals': [['a', 4], ['b', 4], ['c', 3]]}, {'active': [], 'frozen': ['a', 'b', 'c'], 'active_order': [], 'frozen_order': ['c', 'a', 'b'], 'next': None, 'run_ended': True})], [({'last': 3, 'arrivals': []}, {'active': [], 'frozen': [], 'active_order': [], 'frozen_order': [], 'next': None, 'run_ended': True}), ({'last': 3, 'arrivals': [['a', 3]]}, {'active': ['a'], 'frozen': [], 'active_order': ['a'], 'frozen_order': [], 'next': 3, 'run_ended': False}), ({'last': 5, 'arrivals': [['a', 7], ['b', 2], ['c', 5], ['d', 1], ['e', 6]]}, {'active': ['a', 'c', 'e'], 'frozen': ['b', 'd'], 'active_order': ['c', 'e', 'a'], 'frozen_order': ['d', 'b'], 'next': 5, 'run_ended': False}), ({'last': 8, 'arrivals': [['a', 4], ['b', 2], ['c', 6]]}, {'active': [], 'frozen': ['a', 'b', 'c'], 'active_order': [], 'frozen_order': ['b', 'a', 'c'], 'next': None, 'run_ended': True}), ({'last': 0, 'arrivals': [['a', 3], ['b', 1], ['c', 2]]}, {'active': ['a', 'b', 'c'], 'frozen': [], 'active_order': ['b', 'c', 'a'], 'frozen_order': [], 'next': 1, 'run_ended': False}), ({'last': 4, 'arrivals': [['a', 4], ['b', 4], ['c', 3]]}, {'active': ['a', 'b'], 'frozen': ['c'], 'active_order': ['a', 'b'], 'frozen_order': ['c'], 'next': 4, 'run_ended': False}), ({'last': 6, 'arrivals': [['a', 4], ['b', 4], ['c', 3]]}, {'active': [], 'frozen': ['a', 'b', 'c'], 'active_order': [], 'frozen_order': ['c', 'a', 'b'], 'next': None, 'run_ended': True})], [({'last': 3, 'arrivals': []}, {'active': [], 'frozen': [], 'active_order': [], 'frozen_order': [], 'next': None, 'run_ended': True}), ({'last': 3, 'arrivals': [['a', 3]]}, {'active': ['a'], 'frozen': [], 'active_order': ['a'], 'frozen_order': [], 'next': 3, 'run_ended': False}), ({'last': 5, 'arrivals': [['a', 7], ['b', 2], ['c', 5], ['d', 1], ['e', 6]]}, {'active': ['a', 'c', 'e'], 'frozen': ['b', 'd'], 'active_order': ['c', 'e', 'a'], 'frozen_order': ['d', 'b'], 'next': 5, 'run_ended': False}), ({'last': 8, 'arrivals': [['a', 4], ['b', 2], ['c', 6]]}, {'active': [], 'frozen': ['a', 'b', 'c'], 'active_order': [], 'frozen_order': ['b', 'a', 'c'], 'next': None, 'run_ended': True}), ({'last': 0, 'arrivals': [['a', 3], ['b', 1], ['c', 2]]}, {'active': ['a', 'b', 'c'], 'frozen': [], 'active_order': ['b', 'c', 'a'], 'frozen_order': [], 'next': 1, 'run_ended': False}), ({'last': 4, 'arrivals': [['a', 4], ['b', 4], ['c', 3]]}, {'active': ['a', 'b'], 'frozen': ['c'], 'active_order': ['a', 'b'], 'frozen_order': ['c'], 'next': 4, 'run_ended': False}), ({'last': 7, 'arrivals': [['a', 4], ['b', 4], ['c', 3]]}, {'active': [], 'frozen': ['a', 'b', 'c'], 'active_order': [], 'frozen_order': ['c', 'a', 'b'], 'next': None, 'run_ended': True})], [({'last': 3, 'arrivals': []}, {'active': [], 'frozen': [], 'active_order': [], 'frozen_order': [], 'next': None, 'run_ended': True}), ({'last': 3, 'arrivals': [['a', 3]]}, {'active': ['a'], 'frozen': [], 'active_order': ['a'], 'frozen_order': [], 'next': 3, 'run_ended': False}), ({'last': 5, 'arrivals': [['a', 7], ['b', 2], ['c', 5], ['d', 1], ['e', 6]]}, {'active': ['a', 'c', 'e'], 'frozen': ['b', 'd'], 'active_order': ['c', 'e', 'a'], 'frozen_order': ['d', 'b'], 'next': 5, 'run_ended': False}), ({'last': 8, 'arrivals': [['a', 4], ['b', 2], ['c', 6]]}, {'active': [], 'frozen': ['a', 'b', 'c'], 'active_order': [], 'frozen_order': ['b', 'a', 'c'], 'next': None, 'run_ended': True}), ({'last': 0, 'arrivals': [['a', 3], ['b', 1], ['c', 2]]}, {'active': ['a', 'b', 'c'], 'frozen': [], 'active_order': ['b', 'c', 'a'], 'frozen_order': [], 'next': 1, 'run_ended': False}), ({'last': 4, 'arrivals': [['a', 4], ['b', 4], ['c', 3]]}, {'active': ['a', 'b'], 'frozen': ['c'], 'active_order': ['a', 'b'], 'frozen_order': ['c'], 'next': 4, 'run_ended': False}), ({'last': 8, 'arrivals': [['a', 4], ['b', 4], ['c', 3]]}, {'active': [], 'frozen': ['a', 'b', 'c'], 'active_order': [], 'frozen_order': ['c', 'a', 'b'], 'next': None, 'run_ended': True})], [({'last': 3, 'arrivals': []}, {'active': [], 'frozen': [], 'active_order': [], 'frozen_order': [], 'next': None, 'run_ended': True}), ({'last': 3, 'arrivals': [['a', 3]]}, {'active': ['a'], 'frozen': [], 'active_order': ['a'], 'frozen_order': [], 'next': 3, 'run_ended': False}), ({'last': 5, 'arrivals': [['a', 7], ['b', 2], ['c', 5], ['d', 1], ['e', 6]]}, {'active': ['a', 'c', 'e'], 'frozen': ['b', 'd'], 'active_order': ['c', 'e', 'a'], 'frozen_order': ['d', 'b'], 'next': 5, 'run_ended': False}), ({'last': 8, 'arrivals': [['a', 4], ['b', 2], ['c', 6]]}, {'active': [], 'frozen': ['a', 'b', 'c'], 'active_order': [], 'frozen_order': ['b', 'a', 'c'], 'next': None, 'run_ended': True}), ({'last': 0, 'arrivals': [['a', 3], ['b', 1], ['c', 2]]}, {'active': ['a', 'b', 'c'], 'frozen': [], 'active_order': ['b', 'c', 'a'], 'frozen_order': [], 'next': 1, 'run_ended': False}), ({'last': 4, 'arrivals': [['a', 4], ['b', 4], ['c', 3]]}, {'active': ['a', 'b'], 'frozen': ['c'], 'active_order': ['a', 'b'], 'frozen_order': ['c'], 'next': 4, 'run_ended': False}), ({'last': 9, 'arrivals': [['a', 4], ['b', 4], ['c', 3]]}, {'active': [], 'frozen': ['a', 'b', 'c'], 'active_order': [], 'frozen_order': ['c', 'a', 'b'], 'next': None, 'run_ended': True})]][N-1]\ncheck('regression certificate 1', solve(cases[0][0]), cases[0][1])\ncheck('regression certificate 2', solve(cases[1][0]), cases[1][1])\ncheck('regression certificate 3', solve(cases[2][0]), cases[2][1])\ncheck('regression certificate 4', solve(cases[3][0]), cases[3][1])\ncheck('regression certificate 5', solve(cases[4][0]), cases[4][1])\ncheck('regression certificate 6', solve(cases[5][0]), cases[5][1])\ncheck('variant-dependent certificate', solve(cases[6][0]), cases[6][1])\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 stipulated offline diagnostic model; it does not implement a production allocator, concurrency protocol, or complete heap library. 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":"s3-heap-replacement-selection-next","generated_at":"2026-09-29T14:43:37.556756+00:00","license":"CC0-1.0","python":"3.12.14","seed":1,"split":"open-access"},"relevance":"This isolates an internal heap representation or priority-structure invariant using deterministic finite records.","repair":"Derive next using min((x[1] for x in active),default=None) under the stated bounded certificate contract.","root_cause":"Replacement selection has no current candidate when every replacement is frozen.","sha256":"b19b7c2b3d6c8ad88909218f36bd683f986e08e3e4f2ffe7f945d646425dd28a","title":"Replacement selection has no current candidate when every replacement is frozen · case 01","variant":1,"variant_policy":"Six explicit regression certificates are retained; a seventh changes structural size, position, priority, or bounds with N.","verification":{"attempt":{"elapsed_ms":45.296,"exit_code":1,"observations":[{"actual":{"active":[],"active_order":[],"frozen":[],"frozen_order":[],"next":3,"run_ended":true},"check":"regression certificate 1","expected":{"active":[],"active_order":[],"frozen":[],"frozen_order":[],"next":null,"run_ended":true},"passed":false},{"actual":{"active":["a"],"active_order":["a"],"frozen":[],"frozen_order":[],"next":3,"run_ended":false},"check":"regression certificate 2","expected":{"active":["a"],"active_order":["a"],"frozen":[],"frozen_order":[],"next":3,"run_ended":false},"passed":true},{"actual":{"active":["a","c","e"],"active_order":["c","e","a"],"frozen":["b","d"],"frozen_order":["d","b"],"next":7,"run_ended":false},"check":"regression certificate 3","expected":{"active":["a","c","e"],"active_order":["c","e","a"],"frozen":["b","d"],"frozen_order":["d","b"],"next":5,"run_ended":false},"passed":false},{"actual":{"active":[],"active_order":[],"frozen":["a","b","c"],"frozen_order":["b","a","c"],"next":8,"run_ended":true},"check":"regression certificate 4","expected":{"active":[],"active_order":[],"frozen":["a","b","c"],"frozen_order":["b","a","c"],"next":null,"run_ended":true},"passed":false},{"actual":{"active":["a","b","c"],"active_order":["b","c","a"],"frozen":[],"frozen_order":[],"next":3,"run_ended":false},"check":"regression certificate 5","expected":{"active":["a","b","c"],"active_order":["b","c","a"],"frozen":[],"frozen_order":[],"next":1,"run_ended":false},"passed":false},{"actual":{"active":["a","b"],"active_order":["a","b"],"frozen":["c"],"frozen_order":["c"],"next":4,"run_ended":false},"check":"regression certificate 6","expected":{"active":["a","b"],"active_order":["a","b"],"frozen":["c"],"frozen_order":["c"],"next":4,"run_ended":false},"passed":true},{"actual":{"active":[],"active_order":[],"frozen":["a","b","c"],"frozen_order":["c","a","b"],"next":5,"run_ended":true},"check":"variant-dependent certificate","expected":{"active":[],"active_order":[],"frozen":["a","b","c"],"frozen_order":["c","a","b"],"next":null,"run_ended":true},"passed":false}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"regression certificate 1\", \"actual\": {\"active\": [], \"frozen\": [], \"active_order\": [], \"frozen_order\": [], \"next\": 3, \"run_ended\": true}, \"expected\": {\"active\": [], \"frozen\": [], \"active_order\": [], \"frozen_order\": [], \"next\": null, \"run_ended\": true}, \"passed\": false}, {\"check\": \"regression certificate 2\", \"actual\": {\"active\": [\"a\"], \"frozen\": [], \"active_order\": [\"a\"], \"frozen_order\": [], \"next\": 3, \"run_ended\": false}, \"expected\": {\"active\": [\"a\"], \"frozen\": [], \"active_order\": [\"a\"], \"frozen_order\": [], \"next\": 3, \"run_ended\": false}, \"passed\": true}, {\"check\": \"regression certificate 3\", \"actual\": {\"active\": [\"a\", \"c\", \"e\"], \"frozen\": [\"b\", \"d\"], \"active_order\": [\"c\", \"e\", \"a\"], \"frozen_order\": [\"d\", \"b\"], \"next\": 7, \"run_ended\": false}, \"expected\": {\"active\": [\"a\", \"c\", \"e\"], \"frozen\": [\"b\", \"d\"], \"active_order\": [\"c\", \"e\", \"a\"], \"frozen_order\": [\"d\", \"b\"], \"next\": 5, \"run_ended\": false}, \"passed\": false}, {\"check\": \"regression certificate 4\", \"actual\": {\"active\": [], \"frozen\": [\"a\", \"b\", \"c\"], \"active_order\": [], \"frozen_order\": [\"b\", \"a\", \"c\"], \"next\": 8, \"run_ended\": true}, \"expected\": {\"active\": [], \"frozen\": [\"a\", \"b\", \"c\"], \"active_order\": [], \"frozen_order\": [\"b\", \"a\", \"c\"], \"next\": null, \"run_ended\": true}, \"passed\": false}, {\"check\": \"regression certificate 5\", \"actual\": {\"active\": [\"a\", \"b\", \"c\"], \"frozen\": [], \"active_order\": [\"b\", \"c\", \"a\"], \"frozen_order\": [], \"next\": 3, \"run_ended\": false}, \"expected\": {\"active\": [\"a\", \"b\", \"c\"], \"frozen\": [], \"active_order\": [\"b\", \"c\", \"a\"], \"frozen_order\": [], \"next\": 1, \"run_ended\": false}, \"passed\": false}, {\"check\": \"regression certificate 6\", \"actual\": {\"active\": [\"a\", \"b\"], \"frozen\": [\"c\"], \"active_order\": [\"a\", \"b\"], \"frozen_order\": [\"c\"], \"next\": 4, \"run_ended\": false}, \"expected\": {\"active\": [\"a\", \"b\"], \"frozen\": [\"c\"], \"active_order\": [\"a\", \"b\"], \"frozen_order\": [\"c\"], \"next\": 4, \"run_ended\": false}, \"passed\": true}, {\"check\": \"variant-dependent certificate\", \"actual\": {\"active\": [], \"frozen\": [\"a\", \"b\", \"c\"], \"active_order\": [], \"frozen_order\": [\"c\", \"a\", \"b\"], \"next\": 5, \"run_ended\": true}, \"expected\": {\"active\": [], \"frozen\": [\"a\", \"b\", \"c\"], \"active_order\": [], \"frozen_order\": [\"c\", \"a\", \"b\"], \"next\": null, \"run_ended\": true}, \"passed\": false}], \"passed\": false}\n"},"broken":{"elapsed_ms":45.785,"exit_code":1,"observations":[{"actual":{"active":[],"active_order":[],"frozen":[],"frozen_order":[],"next":null,"run_ended":true},"check":"regression certificate 1","expected":{"active":[],"active_order":[],"frozen":[],"frozen_order":[],"next":null,"run_ended":true},"passed":true},{"actual":{"active":["a"],"active_order":["a"],"frozen":[],"frozen_order":[],"next":3,"run_ended":false},"check":"regression certificate 2","expected":{"active":["a"],"active_order":["a"],"frozen":[],"frozen_order":[],"next":3,"run_ended":false},"passed":true},{"actual":{"active":["a","c","e"],"active_order":["c","e","a"],"frozen":["b","d"],"frozen_order":["d","b"],"next":1,"run_ended":false},"check":"regression certificate 3","expected":{"active":["a","c","e"],"active_order":["c","e","a"],"frozen":["b","d"],"frozen_order":["d","b"],"next":5,"run_ended":false},"passed":false},{"actual":{"active":[],"active_order":[],"frozen":["a","b","c"],"frozen_order":["b","a","c"],"next":2,"run_ended":true},"check":"regression certificate 4","expected":{"active":[],"active_order":[],"frozen":["a","b","c"],"frozen_order":["b","a","c"],"next":null,"run_ended":true},"passed":false},{"actual":{"active":["a","b","c"],"active_order":["b","c","a"],"frozen":[],"frozen_order":[],"next":1,"run_ended":false},"check":"regression certificate 5","expected":{"active":["a","b","c"],"active_order":["b","c","a"],"frozen":[],"frozen_order":[],"next":1,"run_ended":false},"passed":true},{"actual":{"active":["a","b"],"active_order":["a","b"],"frozen":["c"],"frozen_order":["c"],"next":3,"run_ended":false},"check":"regression certificate 6","expected":{"active":["a","b"],"active_order":["a","b"],"frozen":["c"],"frozen_order":["c"],"next":4,"run_ended":false},"passed":false},{"actual":{"active":[],"active_order":[],"frozen":["a","b","c"],"frozen_order":["c","a","b"],"next":3,"run_ended":true},"check":"variant-dependent certificate","expected":{"active":[],"active_order":[],"frozen":["a","b","c"],"frozen_order":["c","a","b"],"next":null,"run_ended":true},"passed":false}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"regression certificate 1\", \"actual\": {\"active\": [], \"frozen\": [], \"active_order\": [], \"frozen_order\": [], \"next\": null, \"run_ended\": true}, \"expected\": {\"active\": [], \"frozen\": [], \"active_order\": [], \"frozen_order\": [], \"next\": null, \"run_ended\": true}, \"passed\": true}, {\"check\": \"regression certificate 2\", \"actual\": {\"active\": [\"a\"], \"frozen\": [], \"active_order\": [\"a\"], \"frozen_order\": [], \"next\": 3, \"run_ended\": false}, \"expected\": {\"active\": [\"a\"], \"frozen\": [], \"active_order\": [\"a\"], \"frozen_order\": [], \"next\": 3, \"run_ended\": false}, \"passed\": true}, {\"check\": \"regression certificate 3\", \"actual\": {\"active\": [\"a\", \"c\", \"e\"], \"frozen\": [\"b\", \"d\"], \"active_order\": [\"c\", \"e\", \"a\"], \"frozen_order\": [\"d\", \"b\"], \"next\": 1, \"run_ended\": false}, \"expected\": {\"active\": [\"a\", \"c\", \"e\"], \"frozen\": [\"b\", \"d\"], \"active_order\": [\"c\", \"e\", \"a\"], \"frozen_order\": [\"d\", \"b\"], \"next\": 5, \"run_ended\": false}, \"passed\": false}, {\"check\": \"regression certificate 4\", \"actual\": {\"active\": [], \"frozen\": [\"a\", \"b\", \"c\"], \"active_order\": [], \"frozen_order\": [\"b\", \"a\", \"c\"], \"next\": 2, \"run_ended\": true}, \"expected\": {\"active\": [], \"frozen\": [\"a\", \"b\", \"c\"], \"active_order\": [], \"frozen_order\": [\"b\", \"a\", \"c\"], \"next\": null, \"run_ended\": true}, \"passed\": false}, {\"check\": \"regression certificate 5\", \"actual\": {\"active\": [\"a\", \"b\", \"c\"], \"frozen\": [], \"active_order\": [\"b\", \"c\", \"a\"], \"frozen_order\": [], \"next\": 1, \"run_ended\": false}, \"expected\": {\"active\": [\"a\", \"b\", \"c\"], \"frozen\": [], \"active_order\": [\"b\", \"c\", \"a\"], \"frozen_order\": [], \"next\": 1, \"run_ended\": false}, \"passed\": true}, {\"check\": \"regression certificate 6\", \"actual\": {\"active\": [\"a\", \"b\"], \"frozen\": [\"c\"], \"active_order\": [\"a\", \"b\"], \"frozen_order\": [\"c\"], \"next\": 3, \"run_ended\": false}, \"expected\": {\"active\": [\"a\", \"b\"], \"frozen\": [\"c\"], \"active_order\": [\"a\", \"b\"], \"frozen_order\": [\"c\"], \"next\": 4, \"run_ended\": false}, \"passed\": false}, {\"check\": \"variant-dependent certificate\", \"actual\": {\"active\": [], \"frozen\": [\"a\", \"b\", \"c\"], \"active_order\": [], \"frozen_order\": [\"c\", \"a\", \"b\"], \"next\": 3, \"run_ended\": true}, \"expected\": {\"active\": [], \"frozen\": [\"a\", \"b\", \"c\"], \"active_order\": [], \"frozen_order\": [\"c\", \"a\", \"b\"], \"next\": null, \"run_ended\": true}, \"passed\": false}], \"passed\": false}\n"},"fixed":{"elapsed_ms":46.901,"exit_code":0,"observations":[{"actual":{"active":[],"active_order":[],"frozen":[],"frozen_order":[],"next":null,"run_ended":true},"check":"regression certificate 1","expected":{"active":[],"active_order":[],"frozen":[],"frozen_order":[],"next":null,"run_ended":true},"passed":true},{"actual":{"active":["a"],"active_order":["a"],"frozen":[],"frozen_order":[],"next":3,"run_ended":false},"check":"regression certificate 2","expected":{"active":["a"],"active_order":["a"],"frozen":[],"frozen_order":[],"next":3,"run_ended":false},"passed":true},{"actual":{"active":["a","c","e"],"active_order":["c","e","a"],"frozen":["b","d"],"frozen_order":["d","b"],"next":5,"run_ended":false},"check":"regression certificate 3","expected":{"active":["a","c","e"],"active_order":["c","e","a"],"frozen":["b","d"],"frozen_order":["d","b"],"next":5,"run_ended":false},"passed":true},{"actual":{"active":[],"active_order":[],"frozen":["a","b","c"],"frozen_order":["b","a","c"],"next":null,"run_ended":true},"check":"regression certificate 4","expected":{"active":[],"active_order":[],"frozen":["a","b","c"],"frozen_order":["b","a","c"],"next":null,"run_ended":true},"passed":true},{"actual":{"active":["a","b","c"],"active_order":["b","c","a"],"frozen":[],"frozen_order":[],"next":1,"run_ended":false},"check":"regression certificate 5","expected":{"active":["a","b","c"],"active_order":["b","c","a"],"frozen":[],"frozen_order":[],"next":1,"run_ended":false},"passed":true},{"actual":{"active":["a","b"],"active_order":["a","b"],"frozen":["c"],"frozen_order":["c"],"next":4,"run_ended":false},"check":"regression certificate 6","expected":{"active":["a","b"],"active_order":["a","b"],"frozen":["c"],"frozen_order":["c"],"next":4,"run_ended":false},"passed":true},{"actual":{"active":[],"active_order":[],"frozen":["a","b","c"],"frozen_order":["c","a","b"],"next":null,"run_ended":true},"check":"variant-dependent certificate","expected":{"active":[],"active_order":[],"frozen":["a","b","c"],"frozen_order":["c","a","b"],"next":null,"run_ended":true},"passed":true}],"passed":true,"stderr":"","stdout":"{\"observations\": [{\"check\": \"regression certificate 1\", \"actual\": {\"active\": [], \"frozen\": [], \"active_order\": [], \"frozen_order\": [], \"next\": null, \"run_ended\": true}, \"expected\": {\"active\": [], \"frozen\": [], \"active_order\": [], \"frozen_order\": [], \"next\": null, \"run_ended\": true}, \"passed\": true}, {\"check\": \"regression certificate 2\", \"actual\": {\"active\": [\"a\"], \"frozen\": [], \"active_order\": [\"a\"], \"frozen_order\": [], \"next\": 3, \"run_ended\": false}, \"expected\": {\"active\": [\"a\"], \"frozen\": [], \"active_order\": [\"a\"], \"frozen_order\": [], \"next\": 3, \"run_ended\": false}, \"passed\": true}, {\"check\": \"regression certificate 3\", \"actual\": {\"active\": [\"a\", \"c\", \"e\"], \"frozen\": [\"b\", \"d\"], \"active_order\": [\"c\", \"e\", \"a\"], \"frozen_order\": [\"d\", \"b\"], \"next\": 5, \"run_ended\": false}, \"expected\": {\"active\": [\"a\", \"c\", \"e\"], \"frozen\": [\"b\", \"d\"], \"active_order\": [\"c\", \"e\", \"a\"], \"frozen_order\": [\"d\", \"b\"], \"next\": 5, \"run_ended\": false}, \"passed\": true}, {\"check\": \"regression certificate 4\", \"actual\": {\"active\": [], \"frozen\": [\"a\", \"b\", \"c\"], \"active_order\": [], \"frozen_order\": [\"b\", \"a\", \"c\"], \"next\": null, \"run_ended\": true}, \"expected\": {\"active\": [], \"frozen\": [\"a\", \"b\", \"c\"], \"active_order\": [], \"frozen_order\": [\"b\", \"a\", \"c\"], \"next\": null, \"run_ended\": true}, \"passed\": true}, {\"check\": \"regression certificate 5\", \"actual\": {\"active\": [\"a\", \"b\", \"c\"], \"frozen\": [], \"active_order\": [\"b\", \"c\", \"a\"], \"frozen_order\": [], \"next\": 1, \"run_ended\": false}, \"expected\": {\"active\": [\"a\", \"b\", \"c\"], \"frozen\": [], \"active_order\": [\"b\", \"c\", \"a\"], \"frozen_order\": [], \"next\": 1, \"run_ended\": false}, \"passed\": true}, {\"check\": \"regression certificate 6\", \"actual\": {\"active\": [\"a\", \"b\"], \"frozen\": [\"c\"], \"active_order\": [\"a\", \"b\"], \"frozen_order\": [\"c\"], \"next\": 4, \"run_ended\": false}, \"expected\": {\"active\": [\"a\", \"b\"], \"frozen\": [\"c\"], \"active_order\": [\"a\", \"b\"], \"frozen_order\": [\"c\"], \"next\": 4, \"run_ended\": false}, \"passed\": true}, {\"check\": \"variant-dependent certificate\", \"actual\": {\"active\": [], \"frozen\": [\"a\", \"b\", \"c\"], \"active_order\": [], \"frozen_order\": [\"c\", \"a\", \"b\"], \"next\": null, \"run_ended\": true}, \"expected\": {\"active\": [], \"frozen\": [\"a\", \"b\", \"c\"], \"active_order\": [], \"frozen_order\": [\"c\", \"a\", \"b\"], \"next\": null, \"run_ended\": true}, \"passed\": true}], \"passed\": true}\n"}},"verified":true,"visibility":"public"}