{"abstract":"The bounded interval pop end certificate reports an incorrect size.","category":"Heap invariants","checks":7,"contract":"A bounded interval-tail removal receives intervals, and side low or high. Remove the requested endpoint from the final interval (singleton removed wholly), returning extracted tail replacement, remaining interval list, new logical size, singleton status, surviving endpoint, and array-node count. This isolates tail extraction before global bubbling.","evaluation_group":"s3-heap-model-interval-pop-end","failed_approach":"The local patch uses 2*len(out) and still violates the stated relation.","family":"s3-heap-interval-pop-end-size","id":"FA-40781","implementations":{"attempt":{"sha256":"67c876f25491e39d2aad41d28c57d6a921684beb479acf952e76b8cd46a3011e","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(d):\n    a=d['intervals']; side=d['side']; tail=a[-1] if a else []; k=0 if side=='low' else -1; v=tail[k] if tail else None; rest=tail[1:] if side=='low' else tail[:-1]; out=a[:-1]+([rest] if rest else []) if a else []\n    return {'replacement': v,\n    'remaining': out,\n    'size': 2*len(out),\n    'singleton': bool(out) and len(out[-1])==1,\n    'survivor': rest[0] if rest else None,\n    'nodes': len(out)}\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncases = [[({'intervals': [], 'side': 'low'}, {'replacement': None, 'remaining': [], 'size': 0, 'singleton': False, 'survivor': None, 'nodes': 0}), ({'intervals': [[4]], 'side': 'high'}, {'replacement': 4, 'remaining': [], 'size': 0, 'singleton': False, 'survivor': None, 'nodes': 0}), ({'intervals': [[1, 9]], 'side': 'low'}, {'replacement': 1, 'remaining': [[9]], 'size': 1, 'singleton': True, 'survivor': 9, 'nodes': 1}), ({'intervals': [[1, 9], [3, 7]], 'side': 'high'}, {'replacement': 7, 'remaining': [[1, 9], [3]], 'size': 3, 'singleton': True, 'survivor': 3, 'nodes': 2}), ({'intervals': [[1, 9], [3]], 'side': 'low'}, {'replacement': 3, 'remaining': [[1, 9]], 'size': 2, 'singleton': False, 'survivor': None, 'nodes': 1}), ({'intervals': [[1, 9], [2, 8], [4, 6]], 'side': 'low'}, {'replacement': 4, 'remaining': [[1, 9], [2, 8], [6]], 'size': 5, 'singleton': True, 'survivor': 6, 'nodes': 3}), ({'intervals': [[1, 9], [2, 8], [4, 7]], 'side': 'low'}, {'replacement': 4, 'remaining': [[1, 9], [2, 8], [7]], 'size': 5, 'singleton': True, 'survivor': 7, 'nodes': 3})], [({'intervals': [], 'side': 'low'}, {'replacement': None, 'remaining': [], 'size': 0, 'singleton': False, 'survivor': None, 'nodes': 0}), ({'intervals': [[4]], 'side': 'high'}, {'replacement': 4, 'remaining': [], 'size': 0, 'singleton': False, 'survivor': None, 'nodes': 0}), ({'intervals': [[1, 9]], 'side': 'low'}, {'replacement': 1, 'remaining': [[9]], 'size': 1, 'singleton': True, 'survivor': 9, 'nodes': 1}), ({'intervals': [[1, 9], [3, 7]], 'side': 'high'}, {'replacement': 7, 'remaining': [[1, 9], [3]], 'size': 3, 'singleton': True, 'survivor': 3, 'nodes': 2}), ({'intervals': [[1, 9], [3]], 'side': 'low'}, {'replacement': 3, 'remaining': [[1, 9]], 'size': 2, 'singleton': False, 'survivor': None, 'nodes': 1}), ({'intervals': [[1, 9], [2, 8], [4, 6]], 'side': 'low'}, {'replacement': 4, 'remaining': [[1, 9], [2, 8], [6]], 'size': 5, 'singleton': True, 'survivor': 6, 'nodes': 3}), ({'intervals': [[1, 9], [2, 8], [4, 8]], 'side': 'low'}, {'replacement': 4, 'remaining': [[1, 9], [2, 8], [8]], 'size': 5, 'singleton': True, 'survivor': 8, 'nodes': 3})], [({'intervals': [], 'side': 'low'}, {'replacement': None, 'remaining': [], 'size': 0, 'singleton': False, 'survivor': None, 'nodes': 0}), ({'intervals': [[4]], 'side': 'high'}, {'replacement': 4, 'remaining': [], 'size': 0, 'singleton': False, 'survivor': None, 'nodes': 0}), ({'intervals': [[1, 9]], 'side': 'low'}, {'replacement': 1, 'remaining': [[9]], 'size': 1, 'singleton': True, 'survivor': 9, 'nodes': 1}), ({'intervals': [[1, 9], [3, 7]], 'side': 'high'}, {'replacement': 7, 'remaining': [[1, 9], [3]], 'size': 3, 'singleton': True, 'survivor': 3, 'nodes': 2}), ({'intervals': [[1, 9], [3]], 'side': 'low'}, {'replacement': 3, 'remaining': [[1, 9]], 'size': 2, 'singleton': False, 'survivor': None, 'nodes': 1}), ({'intervals': [[1, 9], [2, 8], [4, 6]], 'side': 'low'}, {'replacement': 4, 'remaining': [[1, 9], [2, 8], [6]], 'size': 5, 'singleton': True, 'survivor': 6, 'nodes': 3}), ({'intervals': [[1, 9], [2, 8], [4, 9]], 'side': 'low'}, {'replacement': 4, 'remaining': [[1, 9], [2, 8], [9]], 'size': 5, 'singleton': True, 'survivor': 9, 'nodes': 3})], [({'intervals': [], 'side': 'low'}, {'replacement': None, 'remaining': [], 'size': 0, 'singleton': False, 'survivor': None, 'nodes': 0}), ({'intervals': [[4]], 'side': 'high'}, {'replacement': 4, 'remaining': [], 'size': 0, 'singleton': False, 'survivor': None, 'nodes': 0}), ({'intervals': [[1, 9]], 'side': 'low'}, {'replacement': 1, 'remaining': [[9]], 'size': 1, 'singleton': True, 'survivor': 9, 'nodes': 1}), ({'intervals': [[1, 9], [3, 7]], 'side': 'high'}, {'replacement': 7, 'remaining': [[1, 9], [3]], 'size': 3, 'singleton': True, 'survivor': 3, 'nodes': 2}), ({'intervals': [[1, 9], [3]], 'side': 'low'}, {'replacement': 3, 'remaining': [[1, 9]], 'size': 2, 'singleton': False, 'survivor': None, 'nodes': 1}), ({'intervals': [[1, 9], [2, 8], [4, 6]], 'side': 'low'}, {'replacement': 4, 'remaining': [[1, 9], [2, 8], [6]], 'size': 5, 'singleton': True, 'survivor': 6, 'nodes': 3}), ({'intervals': [[1, 9], [2, 8], [4, 10]], 'side': 'low'}, {'replacement': 4, 'remaining': [[1, 9], [2, 8], [10]], 'size': 5, 'singleton': True, 'survivor': 10, 'nodes': 3})], [({'intervals': [], 'side': 'low'}, {'replacement': None, 'remaining': [], 'size': 0, 'singleton': False, 'survivor': None, 'nodes': 0}), ({'intervals': [[4]], 'side': 'high'}, {'replacement': 4, 'remaining': [], 'size': 0, 'singleton': False, 'survivor': None, 'nodes': 0}), ({'intervals': [[1, 9]], 'side': 'low'}, {'replacement': 1, 'remaining': [[9]], 'size': 1, 'singleton': True, 'survivor': 9, 'nodes': 1}), ({'intervals': [[1, 9], [3, 7]], 'side': 'high'}, {'replacement': 7, 'remaining': [[1, 9], [3]], 'size': 3, 'singleton': True, 'survivor': 3, 'nodes': 2}), ({'intervals': [[1, 9], [3]], 'side': 'low'}, {'replacement': 3, 'remaining': [[1, 9]], 'size': 2, 'singleton': False, 'survivor': None, 'nodes': 1}), ({'intervals': [[1, 9], [2, 8], [4, 6]], 'side': 'low'}, {'replacement': 4, 'remaining': [[1, 9], [2, 8], [6]], 'size': 5, 'singleton': True, 'survivor': 6, 'nodes': 3}), ({'intervals': [[1, 9], [2, 8], [4, 11]], 'side': 'low'}, {'replacement': 4, 'remaining': [[1, 9], [2, 8], [11]], 'size': 5, 'singleton': True, 'survivor': 11, 'nodes': 3})]][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":"a052fd1096baba1dc67a2516ef0f68a887ccccecca987e4ae0497381ebf09c82","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(d):\n    a=d['intervals']; side=d['side']; tail=a[-1] if a else []; k=0 if side=='low' else -1; v=tail[k] if tail else None; rest=tail[1:] if side=='low' else tail[:-1]; out=a[:-1]+([rest] if rest else []) if a else []\n    return {'replacement': v,\n    'remaining': out,\n    'size': sum(map(len,a))-2 if a else 0,\n    'singleton': bool(out) and len(out[-1])==1,\n    'survivor': rest[0] if rest else None,\n    'nodes': len(out)}\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncases = [[({'intervals': [], 'side': 'low'}, {'replacement': None, 'remaining': [], 'size': 0, 'singleton': False, 'survivor': None, 'nodes': 0}), ({'intervals': [[4]], 'side': 'high'}, {'replacement': 4, 'remaining': [], 'size': 0, 'singleton': False, 'survivor': None, 'nodes': 0}), ({'intervals': [[1, 9]], 'side': 'low'}, {'replacement': 1, 'remaining': [[9]], 'size': 1, 'singleton': True, 'survivor': 9, 'nodes': 1}), ({'intervals': [[1, 9], [3, 7]], 'side': 'high'}, {'replacement': 7, 'remaining': [[1, 9], [3]], 'size': 3, 'singleton': True, 'survivor': 3, 'nodes': 2}), ({'intervals': [[1, 9], [3]], 'side': 'low'}, {'replacement': 3, 'remaining': [[1, 9]], 'size': 2, 'singleton': False, 'survivor': None, 'nodes': 1}), ({'intervals': [[1, 9], [2, 8], [4, 6]], 'side': 'low'}, {'replacement': 4, 'remaining': [[1, 9], [2, 8], [6]], 'size': 5, 'singleton': True, 'survivor': 6, 'nodes': 3}), ({'intervals': [[1, 9], [2, 8], [4, 7]], 'side': 'low'}, {'replacement': 4, 'remaining': [[1, 9], [2, 8], [7]], 'size': 5, 'singleton': True, 'survivor': 7, 'nodes': 3})], [({'intervals': [], 'side': 'low'}, {'replacement': None, 'remaining': [], 'size': 0, 'singleton': False, 'survivor': None, 'nodes': 0}), ({'intervals': [[4]], 'side': 'high'}, {'replacement': 4, 'remaining': [], 'size': 0, 'singleton': False, 'survivor': None, 'nodes': 0}), ({'intervals': [[1, 9]], 'side': 'low'}, {'replacement': 1, 'remaining': [[9]], 'size': 1, 'singleton': True, 'survivor': 9, 'nodes': 1}), ({'intervals': [[1, 9], [3, 7]], 'side': 'high'}, {'replacement': 7, 'remaining': [[1, 9], [3]], 'size': 3, 'singleton': True, 'survivor': 3, 'nodes': 2}), ({'intervals': [[1, 9], [3]], 'side': 'low'}, {'replacement': 3, 'remaining': [[1, 9]], 'size': 2, 'singleton': False, 'survivor': None, 'nodes': 1}), ({'intervals': [[1, 9], [2, 8], [4, 6]], 'side': 'low'}, {'replacement': 4, 'remaining': [[1, 9], [2, 8], [6]], 'size': 5, 'singleton': True, 'survivor': 6, 'nodes': 3}), ({'intervals': [[1, 9], [2, 8], [4, 8]], 'side': 'low'}, {'replacement': 4, 'remaining': [[1, 9], [2, 8], [8]], 'size': 5, 'singleton': True, 'survivor': 8, 'nodes': 3})], [({'intervals': [], 'side': 'low'}, {'replacement': None, 'remaining': [], 'size': 0, 'singleton': False, 'survivor': None, 'nodes': 0}), ({'intervals': [[4]], 'side': 'high'}, {'replacement': 4, 'remaining': [], 'size': 0, 'singleton': False, 'survivor': None, 'nodes': 0}), ({'intervals': [[1, 9]], 'side': 'low'}, {'replacement': 1, 'remaining': [[9]], 'size': 1, 'singleton': True, 'survivor': 9, 'nodes': 1}), ({'intervals': [[1, 9], [3, 7]], 'side': 'high'}, {'replacement': 7, 'remaining': [[1, 9], [3]], 'size': 3, 'singleton': True, 'survivor': 3, 'nodes': 2}), ({'intervals': [[1, 9], [3]], 'side': 'low'}, {'replacement': 3, 'remaining': [[1, 9]], 'size': 2, 'singleton': False, 'survivor': None, 'nodes': 1}), ({'intervals': [[1, 9], [2, 8], [4, 6]], 'side': 'low'}, {'replacement': 4, 'remaining': [[1, 9], [2, 8], [6]], 'size': 5, 'singleton': True, 'survivor': 6, 'nodes': 3}), ({'intervals': [[1, 9], [2, 8], [4, 9]], 'side': 'low'}, {'replacement': 4, 'remaining': [[1, 9], [2, 8], [9]], 'size': 5, 'singleton': True, 'survivor': 9, 'nodes': 3})], [({'intervals': [], 'side': 'low'}, {'replacement': None, 'remaining': [], 'size': 0, 'singleton': False, 'survivor': None, 'nodes': 0}), ({'intervals': [[4]], 'side': 'high'}, {'replacement': 4, 'remaining': [], 'size': 0, 'singleton': False, 'survivor': None, 'nodes': 0}), ({'intervals': [[1, 9]], 'side': 'low'}, {'replacement': 1, 'remaining': [[9]], 'size': 1, 'singleton': True, 'survivor': 9, 'nodes': 1}), ({'intervals': [[1, 9], [3, 7]], 'side': 'high'}, {'replacement': 7, 'remaining': [[1, 9], [3]], 'size': 3, 'singleton': True, 'survivor': 3, 'nodes': 2}), ({'intervals': [[1, 9], [3]], 'side': 'low'}, {'replacement': 3, 'remaining': [[1, 9]], 'size': 2, 'singleton': False, 'survivor': None, 'nodes': 1}), ({'intervals': [[1, 9], [2, 8], [4, 6]], 'side': 'low'}, {'replacement': 4, 'remaining': [[1, 9], [2, 8], [6]], 'size': 5, 'singleton': True, 'survivor': 6, 'nodes': 3}), ({'intervals': [[1, 9], [2, 8], [4, 10]], 'side': 'low'}, {'replacement': 4, 'remaining': [[1, 9], [2, 8], [10]], 'size': 5, 'singleton': True, 'survivor': 10, 'nodes': 3})], [({'intervals': [], 'side': 'low'}, {'replacement': None, 'remaining': [], 'size': 0, 'singleton': False, 'survivor': None, 'nodes': 0}), ({'intervals': [[4]], 'side': 'high'}, {'replacement': 4, 'remaining': [], 'size': 0, 'singleton': False, 'survivor': None, 'nodes': 0}), ({'intervals': [[1, 9]], 'side': 'low'}, {'replacement': 1, 'remaining': [[9]], 'size': 1, 'singleton': True, 'survivor': 9, 'nodes': 1}), ({'intervals': [[1, 9], [3, 7]], 'side': 'high'}, {'replacement': 7, 'remaining': [[1, 9], [3]], 'size': 3, 'singleton': True, 'survivor': 3, 'nodes': 2}), ({'intervals': [[1, 9], [3]], 'side': 'low'}, {'replacement': 3, 'remaining': [[1, 9]], 'size': 2, 'singleton': False, 'survivor': None, 'nodes': 1}), ({'intervals': [[1, 9], [2, 8], [4, 6]], 'side': 'low'}, {'replacement': 4, 'remaining': [[1, 9], [2, 8], [6]], 'size': 5, 'singleton': True, 'survivor': 6, 'nodes': 3}), ({'intervals': [[1, 9], [2, 8], [4, 11]], 'side': 'low'}, {'replacement': 4, 'remaining': [[1, 9], [2, 8], [11]], 'size': 5, 'singleton': True, 'survivor': 11, 'nodes': 3})]][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":"c2d9549ec39fb3315dac6c3ed90f7c75830dbf63ab083f7bf59e92bc6e9aedb4","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(d):\n    a=d['intervals']; side=d['side']; tail=a[-1] if a else []; k=0 if side=='low' else -1; v=tail[k] if tail else None; rest=tail[1:] if side=='low' else tail[:-1]; out=a[:-1]+([rest] if rest else []) if a else []\n    return {'replacement': v,\n    'remaining': out,\n    'size': sum(map(len,out)),\n    'singleton': bool(out) and len(out[-1])==1,\n    'survivor': rest[0] if rest else None,\n    'nodes': len(out)}\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncases = [[({'intervals': [], 'side': 'low'}, {'replacement': None, 'remaining': [], 'size': 0, 'singleton': False, 'survivor': None, 'nodes': 0}), ({'intervals': [[4]], 'side': 'high'}, {'replacement': 4, 'remaining': [], 'size': 0, 'singleton': False, 'survivor': None, 'nodes': 0}), ({'intervals': [[1, 9]], 'side': 'low'}, {'replacement': 1, 'remaining': [[9]], 'size': 1, 'singleton': True, 'survivor': 9, 'nodes': 1}), ({'intervals': [[1, 9], [3, 7]], 'side': 'high'}, {'replacement': 7, 'remaining': [[1, 9], [3]], 'size': 3, 'singleton': True, 'survivor': 3, 'nodes': 2}), ({'intervals': [[1, 9], [3]], 'side': 'low'}, {'replacement': 3, 'remaining': [[1, 9]], 'size': 2, 'singleton': False, 'survivor': None, 'nodes': 1}), ({'intervals': [[1, 9], [2, 8], [4, 6]], 'side': 'low'}, {'replacement': 4, 'remaining': [[1, 9], [2, 8], [6]], 'size': 5, 'singleton': True, 'survivor': 6, 'nodes': 3}), ({'intervals': [[1, 9], [2, 8], [4, 7]], 'side': 'low'}, {'replacement': 4, 'remaining': [[1, 9], [2, 8], [7]], 'size': 5, 'singleton': True, 'survivor': 7, 'nodes': 3})], [({'intervals': [], 'side': 'low'}, {'replacement': None, 'remaining': [], 'size': 0, 'singleton': False, 'survivor': None, 'nodes': 0}), ({'intervals': [[4]], 'side': 'high'}, {'replacement': 4, 'remaining': [], 'size': 0, 'singleton': False, 'survivor': None, 'nodes': 0}), ({'intervals': [[1, 9]], 'side': 'low'}, {'replacement': 1, 'remaining': [[9]], 'size': 1, 'singleton': True, 'survivor': 9, 'nodes': 1}), ({'intervals': [[1, 9], [3, 7]], 'side': 'high'}, {'replacement': 7, 'remaining': [[1, 9], [3]], 'size': 3, 'singleton': True, 'survivor': 3, 'nodes': 2}), ({'intervals': [[1, 9], [3]], 'side': 'low'}, {'replacement': 3, 'remaining': [[1, 9]], 'size': 2, 'singleton': False, 'survivor': None, 'nodes': 1}), ({'intervals': [[1, 9], [2, 8], [4, 6]], 'side': 'low'}, {'replacement': 4, 'remaining': [[1, 9], [2, 8], [6]], 'size': 5, 'singleton': True, 'survivor': 6, 'nodes': 3}), ({'intervals': [[1, 9], [2, 8], [4, 8]], 'side': 'low'}, {'replacement': 4, 'remaining': [[1, 9], [2, 8], [8]], 'size': 5, 'singleton': True, 'survivor': 8, 'nodes': 3})], [({'intervals': [], 'side': 'low'}, {'replacement': None, 'remaining': [], 'size': 0, 'singleton': False, 'survivor': None, 'nodes': 0}), ({'intervals': [[4]], 'side': 'high'}, {'replacement': 4, 'remaining': [], 'size': 0, 'singleton': False, 'survivor': None, 'nodes': 0}), ({'intervals': [[1, 9]], 'side': 'low'}, {'replacement': 1, 'remaining': [[9]], 'size': 1, 'singleton': True, 'survivor': 9, 'nodes': 1}), ({'intervals': [[1, 9], [3, 7]], 'side': 'high'}, {'replacement': 7, 'remaining': [[1, 9], [3]], 'size': 3, 'singleton': True, 'survivor': 3, 'nodes': 2}), ({'intervals': [[1, 9], [3]], 'side': 'low'}, {'replacement': 3, 'remaining': [[1, 9]], 'size': 2, 'singleton': False, 'survivor': None, 'nodes': 1}), ({'intervals': [[1, 9], [2, 8], [4, 6]], 'side': 'low'}, {'replacement': 4, 'remaining': [[1, 9], [2, 8], [6]], 'size': 5, 'singleton': True, 'survivor': 6, 'nodes': 3}), ({'intervals': [[1, 9], [2, 8], [4, 9]], 'side': 'low'}, {'replacement': 4, 'remaining': [[1, 9], [2, 8], [9]], 'size': 5, 'singleton': True, 'survivor': 9, 'nodes': 3})], [({'intervals': [], 'side': 'low'}, {'replacement': None, 'remaining': [], 'size': 0, 'singleton': False, 'survivor': None, 'nodes': 0}), ({'intervals': [[4]], 'side': 'high'}, {'replacement': 4, 'remaining': [], 'size': 0, 'singleton': False, 'survivor': None, 'nodes': 0}), ({'intervals': [[1, 9]], 'side': 'low'}, {'replacement': 1, 'remaining': [[9]], 'size': 1, 'singleton': True, 'survivor': 9, 'nodes': 1}), ({'intervals': [[1, 9], [3, 7]], 'side': 'high'}, {'replacement': 7, 'remaining': [[1, 9], [3]], 'size': 3, 'singleton': True, 'survivor': 3, 'nodes': 2}), ({'intervals': [[1, 9], [3]], 'side': 'low'}, {'replacement': 3, 'remaining': [[1, 9]], 'size': 2, 'singleton': False, 'survivor': None, 'nodes': 1}), ({'intervals': [[1, 9], [2, 8], [4, 6]], 'side': 'low'}, {'replacement': 4, 'remaining': [[1, 9], [2, 8], [6]], 'size': 5, 'singleton': True, 'survivor': 6, 'nodes': 3}), ({'intervals': [[1, 9], [2, 8], [4, 10]], 'side': 'low'}, {'replacement': 4, 'remaining': [[1, 9], [2, 8], [10]], 'size': 5, 'singleton': True, 'survivor': 10, 'nodes': 3})], [({'intervals': [], 'side': 'low'}, {'replacement': None, 'remaining': [], 'size': 0, 'singleton': False, 'survivor': None, 'nodes': 0}), ({'intervals': [[4]], 'side': 'high'}, {'replacement': 4, 'remaining': [], 'size': 0, 'singleton': False, 'survivor': None, 'nodes': 0}), ({'intervals': [[1, 9]], 'side': 'low'}, {'replacement': 1, 'remaining': [[9]], 'size': 1, 'singleton': True, 'survivor': 9, 'nodes': 1}), ({'intervals': [[1, 9], [3, 7]], 'side': 'high'}, {'replacement': 7, 'remaining': [[1, 9], [3]], 'size': 3, 'singleton': True, 'survivor': 3, 'nodes': 2}), ({'intervals': [[1, 9], [3]], 'side': 'low'}, {'replacement': 3, 'remaining': [[1, 9]], 'size': 2, 'singleton': False, 'survivor': None, 'nodes': 1}), ({'intervals': [[1, 9], [2, 8], [4, 6]], 'side': 'low'}, {'replacement': 4, 'remaining': [[1, 9], [2, 8], [6]], 'size': 5, 'singleton': True, 'survivor': 6, 'nodes': 3}), ({'intervals': [[1, 9], [2, 8], [4, 11]], 'side': 'low'}, {'replacement': 4, 'remaining': [[1, 9], [2, 8], [11]], 'size': 5, 'singleton': True, 'survivor': 11, 'nodes': 3})]][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-interval-pop-end-size","generated_at":"2026-09-29T14:43:34.419776+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 size using sum(map(len,out)) under the stated bounded certificate contract.","root_cause":"Interval delete counts one removed member even when the last node survives.","sha256":"08f346cf44a7eaf52e2108bb7785c3130f7ad15374c89765d5a5282a4db54058","title":"Interval delete counts one removed member even when the last node survives · 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":42.487,"exit_code":1,"observations":[{"actual":{"nodes":0,"remaining":[],"replacement":null,"singleton":false,"size":0,"survivor":null},"check":"regression certificate 1","expected":{"nodes":0,"remaining":[],"replacement":null,"singleton":false,"size":0,"survivor":null},"passed":true},{"actual":{"nodes":0,"remaining":[],"replacement":4,"singleton":false,"size":0,"survivor":null},"check":"regression certificate 2","expected":{"nodes":0,"remaining":[],"replacement":4,"singleton":false,"size":0,"survivor":null},"passed":true},{"actual":{"nodes":1,"remaining":[[9]],"replacement":1,"singleton":true,"size":2,"survivor":9},"check":"regression certificate 3","expected":{"nodes":1,"remaining":[[9]],"replacement":1,"singleton":true,"size":1,"survivor":9},"passed":false},{"actual":{"nodes":2,"remaining":[[1,9],[3]],"replacement":7,"singleton":true,"size":4,"survivor":3},"check":"regression certificate 4","expected":{"nodes":2,"remaining":[[1,9],[3]],"replacement":7,"singleton":true,"size":3,"survivor":3},"passed":false},{"actual":{"nodes":1,"remaining":[[1,9]],"replacement":3,"singleton":false,"size":2,"survivor":null},"check":"regression certificate 5","expected":{"nodes":1,"remaining":[[1,9]],"replacement":3,"singleton":false,"size":2,"survivor":null},"passed":true},{"actual":{"nodes":3,"remaining":[[1,9],[2,8],[6]],"replacement":4,"singleton":true,"size":6,"survivor":6},"check":"regression certificate 6","expected":{"nodes":3,"remaining":[[1,9],[2,8],[6]],"replacement":4,"singleton":true,"size":5,"survivor":6},"passed":false},{"actual":{"nodes":3,"remaining":[[1,9],[2,8],[7]],"replacement":4,"singleton":true,"size":6,"survivor":7},"check":"variant-dependent certificate","expected":{"nodes":3,"remaining":[[1,9],[2,8],[7]],"replacement":4,"singleton":true,"size":5,"survivor":7},"passed":false}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"regression certificate 1\", \"actual\": {\"replacement\": null, \"remaining\": [], \"size\": 0, \"singleton\": false, \"survivor\": null, \"nodes\": 0}, \"expected\": {\"replacement\": null, \"remaining\": [], \"size\": 0, \"singleton\": false, \"survivor\": null, \"nodes\": 0}, \"passed\": true}, {\"check\": \"regression certificate 2\", \"actual\": {\"replacement\": 4, \"remaining\": [], \"size\": 0, \"singleton\": false, \"survivor\": null, \"nodes\": 0}, \"expected\": {\"replacement\": 4, \"remaining\": [], \"size\": 0, \"singleton\": false, \"survivor\": null, \"nodes\": 0}, \"passed\": true}, {\"check\": \"regression certificate 3\", \"actual\": {\"replacement\": 1, \"remaining\": [[9]], \"size\": 2, \"singleton\": true, \"survivor\": 9, \"nodes\": 1}, \"expected\": {\"replacement\": 1, \"remaining\": [[9]], \"size\": 1, \"singleton\": true, \"survivor\": 9, \"nodes\": 1}, \"passed\": false}, {\"check\": \"regression certificate 4\", \"actual\": {\"replacement\": 7, \"remaining\": [[1, 9], [3]], \"size\": 4, \"singleton\": true, \"survivor\": 3, \"nodes\": 2}, \"expected\": {\"replacement\": 7, \"remaining\": [[1, 9], [3]], \"size\": 3, \"singleton\": true, \"survivor\": 3, \"nodes\": 2}, \"passed\": false}, {\"check\": \"regression certificate 5\", \"actual\": {\"replacement\": 3, \"remaining\": [[1, 9]], \"size\": 2, \"singleton\": false, \"survivor\": null, \"nodes\": 1}, \"expected\": {\"replacement\": 3, \"remaining\": [[1, 9]], \"size\": 2, \"singleton\": false, \"survivor\": null, \"nodes\": 1}, \"passed\": true}, {\"check\": \"regression certificate 6\", \"actual\": {\"replacement\": 4, \"remaining\": [[1, 9], [2, 8], [6]], \"size\": 6, \"singleton\": true, \"survivor\": 6, \"nodes\": 3}, \"expected\": {\"replacement\": 4, \"remaining\": [[1, 9], [2, 8], [6]], \"size\": 5, \"singleton\": true, \"survivor\": 6, \"nodes\": 3}, \"passed\": false}, {\"check\": \"variant-dependent certificate\", \"actual\": {\"replacement\": 4, \"remaining\": [[1, 9], [2, 8], [7]], \"size\": 6, \"singleton\": true, \"survivor\": 7, \"nodes\": 3}, \"expected\": {\"replacement\": 4, \"remaining\": [[1, 9], [2, 8], [7]], \"size\": 5, \"singleton\": true, \"survivor\": 7, \"nodes\": 3}, \"passed\": false}], \"passed\": false}\n"},"broken":{"elapsed_ms":43.555,"exit_code":1,"observations":[{"actual":{"nodes":0,"remaining":[],"replacement":null,"singleton":false,"size":0,"survivor":null},"check":"regression certificate 1","expected":{"nodes":0,"remaining":[],"replacement":null,"singleton":false,"size":0,"survivor":null},"passed":true},{"actual":{"nodes":0,"remaining":[],"replacement":4,"singleton":false,"size":-1,"survivor":null},"check":"regression certificate 2","expected":{"nodes":0,"remaining":[],"replacement":4,"singleton":false,"size":0,"survivor":null},"passed":false},{"actual":{"nodes":1,"remaining":[[9]],"replacement":1,"singleton":true,"size":0,"survivor":9},"check":"regression certificate 3","expected":{"nodes":1,"remaining":[[9]],"replacement":1,"singleton":true,"size":1,"survivor":9},"passed":false},{"actual":{"nodes":2,"remaining":[[1,9],[3]],"replacement":7,"singleton":true,"size":2,"survivor":3},"check":"regression certificate 4","expected":{"nodes":2,"remaining":[[1,9],[3]],"replacement":7,"singleton":true,"size":3,"survivor":3},"passed":false},{"actual":{"nodes":1,"remaining":[[1,9]],"replacement":3,"singleton":false,"size":1,"survivor":null},"check":"regression certificate 5","expected":{"nodes":1,"remaining":[[1,9]],"replacement":3,"singleton":false,"size":2,"survivor":null},"passed":false},{"actual":{"nodes":3,"remaining":[[1,9],[2,8],[6]],"replacement":4,"singleton":true,"size":4,"survivor":6},"check":"regression certificate 6","expected":{"nodes":3,"remaining":[[1,9],[2,8],[6]],"replacement":4,"singleton":true,"size":5,"survivor":6},"passed":false},{"actual":{"nodes":3,"remaining":[[1,9],[2,8],[7]],"replacement":4,"singleton":true,"size":4,"survivor":7},"check":"variant-dependent certificate","expected":{"nodes":3,"remaining":[[1,9],[2,8],[7]],"replacement":4,"singleton":true,"size":5,"survivor":7},"passed":false}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"regression certificate 1\", \"actual\": {\"replacement\": null, \"remaining\": [], \"size\": 0, \"singleton\": false, \"survivor\": null, \"nodes\": 0}, \"expected\": {\"replacement\": null, \"remaining\": [], \"size\": 0, \"singleton\": false, \"survivor\": null, \"nodes\": 0}, \"passed\": true}, {\"check\": \"regression certificate 2\", \"actual\": {\"replacement\": 4, \"remaining\": [], \"size\": -1, \"singleton\": false, \"survivor\": null, \"nodes\": 0}, \"expected\": {\"replacement\": 4, \"remaining\": [], \"size\": 0, \"singleton\": false, \"survivor\": null, \"nodes\": 0}, \"passed\": false}, {\"check\": \"regression certificate 3\", \"actual\": {\"replacement\": 1, \"remaining\": [[9]], \"size\": 0, \"singleton\": true, \"survivor\": 9, \"nodes\": 1}, \"expected\": {\"replacement\": 1, \"remaining\": [[9]], \"size\": 1, \"singleton\": true, \"survivor\": 9, \"nodes\": 1}, \"passed\": false}, {\"check\": \"regression certificate 4\", \"actual\": {\"replacement\": 7, \"remaining\": [[1, 9], [3]], \"size\": 2, \"singleton\": true, \"survivor\": 3, \"nodes\": 2}, \"expected\": {\"replacement\": 7, \"remaining\": [[1, 9], [3]], \"size\": 3, \"singleton\": true, \"survivor\": 3, \"nodes\": 2}, \"passed\": false}, {\"check\": \"regression certificate 5\", \"actual\": {\"replacement\": 3, \"remaining\": [[1, 9]], \"size\": 1, \"singleton\": false, \"survivor\": null, \"nodes\": 1}, \"expected\": {\"replacement\": 3, \"remaining\": [[1, 9]], \"size\": 2, \"singleton\": false, \"survivor\": null, \"nodes\": 1}, \"passed\": false}, {\"check\": \"regression certificate 6\", \"actual\": {\"replacement\": 4, \"remaining\": [[1, 9], [2, 8], [6]], \"size\": 4, \"singleton\": true, \"survivor\": 6, \"nodes\": 3}, \"expected\": {\"replacement\": 4, \"remaining\": [[1, 9], [2, 8], [6]], \"size\": 5, \"singleton\": true, \"survivor\": 6, \"nodes\": 3}, \"passed\": false}, {\"check\": \"variant-dependent certificate\", \"actual\": {\"replacement\": 4, \"remaining\": [[1, 9], [2, 8], [7]], \"size\": 4, \"singleton\": true, \"survivor\": 7, \"nodes\": 3}, \"expected\": {\"replacement\": 4, \"remaining\": [[1, 9], [2, 8], [7]], \"size\": 5, \"singleton\": true, \"survivor\": 7, \"nodes\": 3}, \"passed\": false}], \"passed\": false}\n"},"fixed":{"elapsed_ms":43.053,"exit_code":0,"observations":[{"actual":{"nodes":0,"remaining":[],"replacement":null,"singleton":false,"size":0,"survivor":null},"check":"regression certificate 1","expected":{"nodes":0,"remaining":[],"replacement":null,"singleton":false,"size":0,"survivor":null},"passed":true},{"actual":{"nodes":0,"remaining":[],"replacement":4,"singleton":false,"size":0,"survivor":null},"check":"regression certificate 2","expected":{"nodes":0,"remaining":[],"replacement":4,"singleton":false,"size":0,"survivor":null},"passed":true},{"actual":{"nodes":1,"remaining":[[9]],"replacement":1,"singleton":true,"size":1,"survivor":9},"check":"regression certificate 3","expected":{"nodes":1,"remaining":[[9]],"replacement":1,"singleton":true,"size":1,"survivor":9},"passed":true},{"actual":{"nodes":2,"remaining":[[1,9],[3]],"replacement":7,"singleton":true,"size":3,"survivor":3},"check":"regression certificate 4","expected":{"nodes":2,"remaining":[[1,9],[3]],"replacement":7,"singleton":true,"size":3,"survivor":3},"passed":true},{"actual":{"nodes":1,"remaining":[[1,9]],"replacement":3,"singleton":false,"size":2,"survivor":null},"check":"regression certificate 5","expected":{"nodes":1,"remaining":[[1,9]],"replacement":3,"singleton":false,"size":2,"survivor":null},"passed":true},{"actual":{"nodes":3,"remaining":[[1,9],[2,8],[6]],"replacement":4,"singleton":true,"size":5,"survivor":6},"check":"regression certificate 6","expected":{"nodes":3,"remaining":[[1,9],[2,8],[6]],"replacement":4,"singleton":true,"size":5,"survivor":6},"passed":true},{"actual":{"nodes":3,"remaining":[[1,9],[2,8],[7]],"replacement":4,"singleton":true,"size":5,"survivor":7},"check":"variant-dependent certificate","expected":{"nodes":3,"remaining":[[1,9],[2,8],[7]],"replacement":4,"singleton":true,"size":5,"survivor":7},"passed":true}],"passed":true,"stderr":"","stdout":"{\"observations\": [{\"check\": \"regression certificate 1\", \"actual\": {\"replacement\": null, \"remaining\": [], \"size\": 0, \"singleton\": false, \"survivor\": null, \"nodes\": 0}, \"expected\": {\"replacement\": null, \"remaining\": [], \"size\": 0, \"singleton\": false, \"survivor\": null, \"nodes\": 0}, \"passed\": true}, {\"check\": \"regression certificate 2\", \"actual\": {\"replacement\": 4, \"remaining\": [], \"size\": 0, \"singleton\": false, \"survivor\": null, \"nodes\": 0}, \"expected\": {\"replacement\": 4, \"remaining\": [], \"size\": 0, \"singleton\": false, \"survivor\": null, \"nodes\": 0}, \"passed\": true}, {\"check\": \"regression certificate 3\", \"actual\": {\"replacement\": 1, \"remaining\": [[9]], \"size\": 1, \"singleton\": true, \"survivor\": 9, \"nodes\": 1}, \"expected\": {\"replacement\": 1, \"remaining\": [[9]], \"size\": 1, \"singleton\": true, \"survivor\": 9, \"nodes\": 1}, \"passed\": true}, {\"check\": \"regression certificate 4\", \"actual\": {\"replacement\": 7, \"remaining\": [[1, 9], [3]], \"size\": 3, \"singleton\": true, \"survivor\": 3, \"nodes\": 2}, \"expected\": {\"replacement\": 7, \"remaining\": [[1, 9], [3]], \"size\": 3, \"singleton\": true, \"survivor\": 3, \"nodes\": 2}, \"passed\": true}, {\"check\": \"regression certificate 5\", \"actual\": {\"replacement\": 3, \"remaining\": [[1, 9]], \"size\": 2, \"singleton\": false, \"survivor\": null, \"nodes\": 1}, \"expected\": {\"replacement\": 3, \"remaining\": [[1, 9]], \"size\": 2, \"singleton\": false, \"survivor\": null, \"nodes\": 1}, \"passed\": true}, {\"check\": \"regression certificate 6\", \"actual\": {\"replacement\": 4, \"remaining\": [[1, 9], [2, 8], [6]], \"size\": 5, \"singleton\": true, \"survivor\": 6, \"nodes\": 3}, \"expected\": {\"replacement\": 4, \"remaining\": [[1, 9], [2, 8], [6]], \"size\": 5, \"singleton\": true, \"survivor\": 6, \"nodes\": 3}, \"passed\": true}, {\"check\": \"variant-dependent certificate\", \"actual\": {\"replacement\": 4, \"remaining\": [[1, 9], [2, 8], [7]], \"size\": 5, \"singleton\": true, \"survivor\": 7, \"nodes\": 3}, \"expected\": {\"replacement\": 4, \"remaining\": [[1, 9], [2, 8], [7]], \"size\": 5, \"singleton\": true, \"survivor\": 7, \"nodes\": 3}, \"passed\": true}], \"passed\": true}\n"}},"verified":true,"visibility":"public"}