{"abstract":"A consuming split leaves the original whole-slice exclusive capability usable.","category":"Borrow checking","checks":21,"contract":"Validate static proof objects for splitting borrowed slices. Bounds are half-open; split point lies in 0..length; children exactly partition parent; exclusive children disjoint; every child retains parent owner and generation; dynamic indices need inequality proof; empty children confer no element access; strided loans include every enumerated element; reverse views retain original element addresses; consuming split removes parent exclusive capability. Input is a fully explicit descriptor of the stated toy IR. Return rule identifiers in declaration order; absent optional obligations use the provided neutral defaults. No rule is an assertion about a production language.","evaluation_group":"s3-borrow-checking-slice-borrow-proofs","failed_approach":"The partial repair uses if d['consuming'] and d['parent_unique_live'] and not d['parent']: errors.append('split-consumption'), which still violates the stipulated analysis contract.","family":"s3-borrow-checking-slice-borrow-proofs-split-consumption","id":"FA-43786","implementations":{"attempt":{"sha256":"3b61fff0f5830045bf7169afef6c6f50bcb1cd519de8d884b5819791772d696a","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(d):\n    errors=[]\n    if d['split']<0 or d['split']>d['length']: errors.append('split-boundary')\n    if set(d['left'])|set(d['right'])!=set(d['parent']): errors.append('partition-completeness')\n    if bool(set(d['exclusive_a'])&set(d['exclusive_b'])): errors.append('exclusive-disjoint')\n    if any(x!=d['owner'] for x in d['child_owners']): errors.append('owner-preservation')\n    if any(x!=d['generation'] for x in d['child_generations']): errors.append('generation-preservation')\n    if d['dynamic_pair'] and not d['inequality_proven']: errors.append('dynamic-disjoint-proof')\n    if bool(d['empty_access']): errors.append('empty-access')\n    if set(d['stride_indices'])!=set(d['enumerated']): errors.append('strided-footprint')\n    if d['reverse_actual']!=d['reverse_expected']: errors.append('reverse-addresses')\n    if d['consuming'] and d['parent_unique_live'] and not d['parent']: errors.append('split-consumption')\n    return errors\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\nbase={'length': 0, 'split': 0, 'left': [], 'right': [], 'parent': [], 'exclusive_a': [], 'exclusive_b': [], 'child_owners': [], 'owner': None, 'child_generations': [], 'generation': 0, 'dynamic_pair': False, 'inequality_proven': True, 'empty_access': [], 'stride_indices': [], 'enumerated': [], 'reverse_expected': [], 'reverse_actual': [], 'consuming': False, 'parent_unique_live': False}\ncheck('well formed empty obligations',solve(base),[])\ncheck('split-boundary regression 0', solve(dict(base, **({'length':N,'split':N+1}))), ['split-boundary'])\ncheck('split-boundary regression 1', solve(dict(base, **({'length':N+1,'split':N+2}))), ['split-boundary'])\ncheck('partition-completeness regression 0', solve(dict(base, **({'parent':list(range(N+1)),'left':[0]}))), ['partition-completeness'])\ncheck('partition-completeness regression 1', solve(dict(base, **({'parent':[N,N+1],'right':[N]}))), ['partition-completeness'])\ncheck('exclusive-disjoint regression 0', solve(dict(base, **({'exclusive_a':[N,N+1],'exclusive_b':[N+1]}))), ['exclusive-disjoint'])\ncheck('exclusive-disjoint regression 1', solve(dict(base, **({'exclusive_a':[N],'exclusive_b':[N,N+1]}))), ['exclusive-disjoint'])\ncheck('owner-preservation regression 0', solve(dict(base, **({'owner':'r','child_owners':['r','s']}))), ['owner-preservation'])\ncheck('owner-preservation regression 1', solve(dict(base, **({'owner':N,'child_owners':[N,N+1]}))), ['owner-preservation'])\ncheck('generation-preservation regression 0', solve(dict(base, **({'generation':N+1,'child_generations':[N]}))), ['generation-preservation'])\ncheck('generation-preservation regression 1', solve(dict(base, **({'generation':N+2,'child_generations':[N+1]}))), ['generation-preservation'])\ncheck('dynamic-disjoint-proof regression 0', solve(dict(base, **({'dynamic_pair':True,'inequality_proven':False,'length':N}))), ['dynamic-disjoint-proof'])\ncheck('dynamic-disjoint-proof regression 1', solve(dict(base, **({'dynamic_pair':True,'inequality_proven':False,'length':N+1}))), ['dynamic-disjoint-proof'])\ncheck('empty-access regression 0', solve(dict(base, **({'empty_access':[N]}))), ['empty-access'])\ncheck('empty-access regression 1', solve(dict(base, **({'empty_access':[N+1]}))), ['empty-access'])\ncheck('strided-footprint regression 0', solve(dict(base, **({'stride_indices':[N,N+2],'enumerated':[N,N+1]}))), ['strided-footprint'])\ncheck('strided-footprint regression 1', solve(dict(base, **({'stride_indices':[N,N+3],'enumerated':[N,N+2]}))), ['strided-footprint'])\ncheck('reverse-addresses regression 0', solve(dict(base, **({'reverse_actual':[N,N+1],'reverse_expected':[N+1,N]}))), ['reverse-addresses'])\ncheck('reverse-addresses regression 1', solve(dict(base, **({'reverse_actual':[N,N+1,N+2],'reverse_expected':[N+2,N+1,N]}))), ['reverse-addresses'])\ncheck('split-consumption regression 0', solve(dict(base, **({'consuming':True,'parent_unique_live':True,'parent':[N],'left':[N]}))), ['split-consumption'])\ncheck('split-consumption regression 1', solve(dict(base, **({'consuming':True,'parent_unique_live':True,'parent':[N+1],'right':[N+1]}))), ['split-consumption'])\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":"dfe2fcc4802af3cc6ec3b70222fc82a8e9d99b36bed173370c67481016d943cc","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(d):\n    errors=[]\n    if d['split']<0 or d['split']>d['length']: errors.append('split-boundary')\n    if set(d['left'])|set(d['right'])!=set(d['parent']): errors.append('partition-completeness')\n    if bool(set(d['exclusive_a'])&set(d['exclusive_b'])): errors.append('exclusive-disjoint')\n    if any(x!=d['owner'] for x in d['child_owners']): errors.append('owner-preservation')\n    if any(x!=d['generation'] for x in d['child_generations']): errors.append('generation-preservation')\n    if d['dynamic_pair'] and not d['inequality_proven']: errors.append('dynamic-disjoint-proof')\n    if bool(d['empty_access']): errors.append('empty-access')\n    if set(d['stride_indices'])!=set(d['enumerated']): errors.append('strided-footprint')\n    if d['reverse_actual']!=d['reverse_expected']: errors.append('reverse-addresses')\n    if False: errors.append('split-consumption')\n    return errors\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\nbase={'length': 0, 'split': 0, 'left': [], 'right': [], 'parent': [], 'exclusive_a': [], 'exclusive_b': [], 'child_owners': [], 'owner': None, 'child_generations': [], 'generation': 0, 'dynamic_pair': False, 'inequality_proven': True, 'empty_access': [], 'stride_indices': [], 'enumerated': [], 'reverse_expected': [], 'reverse_actual': [], 'consuming': False, 'parent_unique_live': False}\ncheck('well formed empty obligations',solve(base),[])\ncheck('split-boundary regression 0', solve(dict(base, **({'length':N,'split':N+1}))), ['split-boundary'])\ncheck('split-boundary regression 1', solve(dict(base, **({'length':N+1,'split':N+2}))), ['split-boundary'])\ncheck('partition-completeness regression 0', solve(dict(base, **({'parent':list(range(N+1)),'left':[0]}))), ['partition-completeness'])\ncheck('partition-completeness regression 1', solve(dict(base, **({'parent':[N,N+1],'right':[N]}))), ['partition-completeness'])\ncheck('exclusive-disjoint regression 0', solve(dict(base, **({'exclusive_a':[N,N+1],'exclusive_b':[N+1]}))), ['exclusive-disjoint'])\ncheck('exclusive-disjoint regression 1', solve(dict(base, **({'exclusive_a':[N],'exclusive_b':[N,N+1]}))), ['exclusive-disjoint'])\ncheck('owner-preservation regression 0', solve(dict(base, **({'owner':'r','child_owners':['r','s']}))), ['owner-preservation'])\ncheck('owner-preservation regression 1', solve(dict(base, **({'owner':N,'child_owners':[N,N+1]}))), ['owner-preservation'])\ncheck('generation-preservation regression 0', solve(dict(base, **({'generation':N+1,'child_generations':[N]}))), ['generation-preservation'])\ncheck('generation-preservation regression 1', solve(dict(base, **({'generation':N+2,'child_generations':[N+1]}))), ['generation-preservation'])\ncheck('dynamic-disjoint-proof regression 0', solve(dict(base, **({'dynamic_pair':True,'inequality_proven':False,'length':N}))), ['dynamic-disjoint-proof'])\ncheck('dynamic-disjoint-proof regression 1', solve(dict(base, **({'dynamic_pair':True,'inequality_proven':False,'length':N+1}))), ['dynamic-disjoint-proof'])\ncheck('empty-access regression 0', solve(dict(base, **({'empty_access':[N]}))), ['empty-access'])\ncheck('empty-access regression 1', solve(dict(base, **({'empty_access':[N+1]}))), ['empty-access'])\ncheck('strided-footprint regression 0', solve(dict(base, **({'stride_indices':[N,N+2],'enumerated':[N,N+1]}))), ['strided-footprint'])\ncheck('strided-footprint regression 1', solve(dict(base, **({'stride_indices':[N,N+3],'enumerated':[N,N+2]}))), ['strided-footprint'])\ncheck('reverse-addresses regression 0', solve(dict(base, **({'reverse_actual':[N,N+1],'reverse_expected':[N+1,N]}))), ['reverse-addresses'])\ncheck('reverse-addresses regression 1', solve(dict(base, **({'reverse_actual':[N,N+1,N+2],'reverse_expected':[N+2,N+1,N]}))), ['reverse-addresses'])\ncheck('split-consumption regression 0', solve(dict(base, **({'consuming':True,'parent_unique_live':True,'parent':[N],'left':[N]}))), ['split-consumption'])\ncheck('split-consumption regression 1', solve(dict(base, **({'consuming':True,'parent_unique_live':True,'parent':[N+1],'right':[N+1]}))), ['split-consumption'])\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":"a27a0cdd3aa8345549d6b4891eb8008c1ca87ebf35df567260dba4b119bc4c87","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(d):\n    errors=[]\n    if d['split']<0 or d['split']>d['length']: errors.append('split-boundary')\n    if set(d['left'])|set(d['right'])!=set(d['parent']): errors.append('partition-completeness')\n    if bool(set(d['exclusive_a'])&set(d['exclusive_b'])): errors.append('exclusive-disjoint')\n    if any(x!=d['owner'] for x in d['child_owners']): errors.append('owner-preservation')\n    if any(x!=d['generation'] for x in d['child_generations']): errors.append('generation-preservation')\n    if d['dynamic_pair'] and not d['inequality_proven']: errors.append('dynamic-disjoint-proof')\n    if bool(d['empty_access']): errors.append('empty-access')\n    if set(d['stride_indices'])!=set(d['enumerated']): errors.append('strided-footprint')\n    if d['reverse_actual']!=d['reverse_expected']: errors.append('reverse-addresses')\n    if d['consuming'] and d['parent_unique_live']: errors.append('split-consumption')\n    return errors\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\nbase={'length': 0, 'split': 0, 'left': [], 'right': [], 'parent': [], 'exclusive_a': [], 'exclusive_b': [], 'child_owners': [], 'owner': None, 'child_generations': [], 'generation': 0, 'dynamic_pair': False, 'inequality_proven': True, 'empty_access': [], 'stride_indices': [], 'enumerated': [], 'reverse_expected': [], 'reverse_actual': [], 'consuming': False, 'parent_unique_live': False}\ncheck('well formed empty obligations',solve(base),[])\ncheck('split-boundary regression 0', solve(dict(base, **({'length':N,'split':N+1}))), ['split-boundary'])\ncheck('split-boundary regression 1', solve(dict(base, **({'length':N+1,'split':N+2}))), ['split-boundary'])\ncheck('partition-completeness regression 0', solve(dict(base, **({'parent':list(range(N+1)),'left':[0]}))), ['partition-completeness'])\ncheck('partition-completeness regression 1', solve(dict(base, **({'parent':[N,N+1],'right':[N]}))), ['partition-completeness'])\ncheck('exclusive-disjoint regression 0', solve(dict(base, **({'exclusive_a':[N,N+1],'exclusive_b':[N+1]}))), ['exclusive-disjoint'])\ncheck('exclusive-disjoint regression 1', solve(dict(base, **({'exclusive_a':[N],'exclusive_b':[N,N+1]}))), ['exclusive-disjoint'])\ncheck('owner-preservation regression 0', solve(dict(base, **({'owner':'r','child_owners':['r','s']}))), ['owner-preservation'])\ncheck('owner-preservation regression 1', solve(dict(base, **({'owner':N,'child_owners':[N,N+1]}))), ['owner-preservation'])\ncheck('generation-preservation regression 0', solve(dict(base, **({'generation':N+1,'child_generations':[N]}))), ['generation-preservation'])\ncheck('generation-preservation regression 1', solve(dict(base, **({'generation':N+2,'child_generations':[N+1]}))), ['generation-preservation'])\ncheck('dynamic-disjoint-proof regression 0', solve(dict(base, **({'dynamic_pair':True,'inequality_proven':False,'length':N}))), ['dynamic-disjoint-proof'])\ncheck('dynamic-disjoint-proof regression 1', solve(dict(base, **({'dynamic_pair':True,'inequality_proven':False,'length':N+1}))), ['dynamic-disjoint-proof'])\ncheck('empty-access regression 0', solve(dict(base, **({'empty_access':[N]}))), ['empty-access'])\ncheck('empty-access regression 1', solve(dict(base, **({'empty_access':[N+1]}))), ['empty-access'])\ncheck('strided-footprint regression 0', solve(dict(base, **({'stride_indices':[N,N+2],'enumerated':[N,N+1]}))), ['strided-footprint'])\ncheck('strided-footprint regression 1', solve(dict(base, **({'stride_indices':[N,N+3],'enumerated':[N,N+2]}))), ['strided-footprint'])\ncheck('reverse-addresses regression 0', solve(dict(base, **({'reverse_actual':[N,N+1],'reverse_expected':[N+1,N]}))), ['reverse-addresses'])\ncheck('reverse-addresses regression 1', solve(dict(base, **({'reverse_actual':[N,N+1,N+2],'reverse_expected':[N+2,N+1,N]}))), ['reverse-addresses'])\ncheck('split-consumption regression 0', solve(dict(base, **({'consuming':True,'parent_unique_live':True,'parent':[N],'left':[N]}))), ['split-consumption'])\ncheck('split-consumption regression 1', solve(dict(base, **({'consuming':True,'parent_unique_live':True,'parent':[N+1],'right':[N+1]}))), ['split-consumption'])\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":"The explicitly stated toy language is the complete scope; this is not a production compiler or a claim about Rust semantics. 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-borrow-checking-slice-borrow-proofs-split-consumption","generated_at":"2026-09-29T14:44:05.615049+00:00","license":"CC0-1.0","python":"3.12.14","seed":1,"split":"open-access"},"relevance":"A finite offline static-analysis model of ownership and borrowing; it does not execute the analyzed program.","repair":"Apply the specified transfer or inference rule at this site: if d['consuming'] and d['parent_unique_live']: errors.append('split-consumption').","root_cause":"The static analyzer mishandles split consumption: a consuming split leaves the original whole-slice exclusive capability usable.","sha256":"d5250c31c7a07d2f04cf3034f50adc4725dcf82055e479993c5da4143eac6296","title":"A consuming split leaves the original whole-slice exclusive capability usable · case 01","variant":1,"variant_policy":"Five numbered records share a model and may reuse boundary fixtures.","verification":{"attempt":{"elapsed_ms":48.45,"exit_code":1,"observations":[{"actual":[],"check":"well formed empty obligations","expected":[],"passed":true},{"actual":["split-boundary"],"check":"split-boundary regression 0","expected":["split-boundary"],"passed":true},{"actual":["split-boundary"],"check":"split-boundary regression 1","expected":["split-boundary"],"passed":true},{"actual":["partition-completeness"],"check":"partition-completeness regression 0","expected":["partition-completeness"],"passed":true},{"actual":["partition-completeness"],"check":"partition-completeness regression 1","expected":["partition-completeness"],"passed":true},{"actual":["exclusive-disjoint"],"check":"exclusive-disjoint regression 0","expected":["exclusive-disjoint"],"passed":true},{"actual":["exclusive-disjoint"],"check":"exclusive-disjoint regression 1","expected":["exclusive-disjoint"],"passed":true},{"actual":["owner-preservation"],"check":"owner-preservation regression 0","expected":["owner-preservation"],"passed":true},{"actual":["owner-preservation"],"check":"owner-preservation regression 1","expected":["owner-preservation"],"passed":true},{"actual":["generation-preservation"],"check":"generation-preservation regression 0","expected":["generation-preservation"],"passed":true},{"actual":["generation-preservation"],"check":"generation-preservation regression 1","expected":["generation-preservation"],"passed":true},{"actual":["dynamic-disjoint-proof"],"check":"dynamic-disjoint-proof regression 0","expected":["dynamic-disjoint-proof"],"passed":true},{"actual":["dynamic-disjoint-proof"],"check":"dynamic-disjoint-proof regression 1","expected":["dynamic-disjoint-proof"],"passed":true},{"actual":["empty-access"],"check":"empty-access regression 0","expected":["empty-access"],"passed":true},{"actual":["empty-access"],"check":"empty-access regression 1","expected":["empty-access"],"passed":true},{"actual":["strided-footprint"],"check":"strided-footprint regression 0","expected":["strided-footprint"],"passed":true},{"actual":["strided-footprint"],"check":"strided-footprint regression 1","expected":["strided-footprint"],"passed":true},{"actual":["reverse-addresses"],"check":"reverse-addresses regression 0","expected":["reverse-addresses"],"passed":true},{"actual":["reverse-addresses"],"check":"reverse-addresses regression 1","expected":["reverse-addresses"],"passed":true},{"actual":[],"check":"split-consumption regression 0","expected":["split-consumption"],"passed":false},{"actual":[],"check":"split-consumption regression 1","expected":["split-consumption"],"passed":false}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"well formed empty obligations\", \"actual\": [], \"expected\": [], \"passed\": true}, {\"check\": \"split-boundary regression 0\", \"actual\": [\"split-boundary\"], \"expected\": [\"split-boundary\"], \"passed\": true}, {\"check\": \"split-boundary regression 1\", \"actual\": [\"split-boundary\"], \"expected\": [\"split-boundary\"], \"passed\": true}, {\"check\": \"partition-completeness regression 0\", \"actual\": [\"partition-completeness\"], \"expected\": [\"partition-completeness\"], \"passed\": true}, {\"check\": \"partition-completeness regression 1\", \"actual\": [\"partition-completeness\"], \"expected\": [\"partition-completeness\"], \"passed\": true}, {\"check\": \"exclusive-disjoint regression 0\", \"actual\": [\"exclusive-disjoint\"], \"expected\": [\"exclusive-disjoint\"], \"passed\": true}, {\"check\": \"exclusive-disjoint regression 1\", \"actual\": [\"exclusive-disjoint\"], \"expected\": [\"exclusive-disjoint\"], \"passed\": true}, {\"check\": \"owner-preservation regression 0\", \"actual\": [\"owner-preservation\"], \"expected\": [\"owner-preservation\"], \"passed\": true}, {\"check\": \"owner-preservation regression 1\", \"actual\": [\"owner-preservation\"], \"expected\": [\"owner-preservation\"], \"passed\": true}, {\"check\": \"generation-preservation regression 0\", \"actual\": [\"generation-preservation\"], \"expected\": [\"generation-preservation\"], \"passed\": true}, {\"check\": \"generation-preservation regression 1\", \"actual\": [\"generation-preservation\"], \"expected\": [\"generation-preservation\"], \"passed\": true}, {\"check\": \"dynamic-disjoint-proof regression 0\", \"actual\": [\"dynamic-disjoint-proof\"], \"expected\": [\"dynamic-disjoint-proof\"], \"passed\": true}, {\"check\": \"dynamic-disjoint-proof regression 1\", \"actual\": [\"dynamic-disjoint-proof\"], \"expected\": [\"dynamic-disjoint-proof\"], \"passed\": true}, {\"check\": \"empty-access regression 0\", \"actual\": [\"empty-access\"], \"expected\": [\"empty-access\"], \"passed\": true}, {\"check\": \"empty-access regression 1\", \"actual\": [\"empty-access\"], \"expected\": [\"empty-access\"], \"passed\": true}, {\"check\": \"strided-footprint regression 0\", \"actual\": [\"strided-footprint\"], \"expected\": [\"strided-footprint\"], \"passed\": true}, {\"check\": \"strided-footprint regression 1\", \"actual\": [\"strided-footprint\"], \"expected\": [\"strided-footprint\"], \"passed\": true}, {\"check\": \"reverse-addresses regression 0\", \"actual\": [\"reverse-addresses\"], \"expected\": [\"reverse-addresses\"], \"passed\": true}, {\"check\": \"reverse-addresses regression 1\", \"actual\": [\"reverse-addresses\"], \"expected\": [\"reverse-addresses\"], \"passed\": true}, {\"check\": \"split-consumption regression 0\", \"actual\": [], \"expected\": [\"split-consumption\"], \"passed\": false}, {\"check\": \"split-consumption regression 1\", \"actual\": [], \"expected\": [\"split-consumption\"], \"passed\": false}], \"passed\": false}\n"},"broken":{"elapsed_ms":44.504,"exit_code":1,"observations":[{"actual":[],"check":"well formed empty obligations","expected":[],"passed":true},{"actual":["split-boundary"],"check":"split-boundary regression 0","expected":["split-boundary"],"passed":true},{"actual":["split-boundary"],"check":"split-boundary regression 1","expected":["split-boundary"],"passed":true},{"actual":["partition-completeness"],"check":"partition-completeness regression 0","expected":["partition-completeness"],"passed":true},{"actual":["partition-completeness"],"check":"partition-completeness regression 1","expected":["partition-completeness"],"passed":true},{"actual":["exclusive-disjoint"],"check":"exclusive-disjoint regression 0","expected":["exclusive-disjoint"],"passed":true},{"actual":["exclusive-disjoint"],"check":"exclusive-disjoint regression 1","expected":["exclusive-disjoint"],"passed":true},{"actual":["owner-preservation"],"check":"owner-preservation regression 0","expected":["owner-preservation"],"passed":true},{"actual":["owner-preservation"],"check":"owner-preservation regression 1","expected":["owner-preservation"],"passed":true},{"actual":["generation-preservation"],"check":"generation-preservation regression 0","expected":["generation-preservation"],"passed":true},{"actual":["generation-preservation"],"check":"generation-preservation regression 1","expected":["generation-preservation"],"passed":true},{"actual":["dynamic-disjoint-proof"],"check":"dynamic-disjoint-proof regression 0","expected":["dynamic-disjoint-proof"],"passed":true},{"actual":["dynamic-disjoint-proof"],"check":"dynamic-disjoint-proof regression 1","expected":["dynamic-disjoint-proof"],"passed":true},{"actual":["empty-access"],"check":"empty-access regression 0","expected":["empty-access"],"passed":true},{"actual":["empty-access"],"check":"empty-access regression 1","expected":["empty-access"],"passed":true},{"actual":["strided-footprint"],"check":"strided-footprint regression 0","expected":["strided-footprint"],"passed":true},{"actual":["strided-footprint"],"check":"strided-footprint regression 1","expected":["strided-footprint"],"passed":true},{"actual":["reverse-addresses"],"check":"reverse-addresses regression 0","expected":["reverse-addresses"],"passed":true},{"actual":["reverse-addresses"],"check":"reverse-addresses regression 1","expected":["reverse-addresses"],"passed":true},{"actual":[],"check":"split-consumption regression 0","expected":["split-consumption"],"passed":false},{"actual":[],"check":"split-consumption regression 1","expected":["split-consumption"],"passed":false}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"well formed empty obligations\", \"actual\": [], \"expected\": [], \"passed\": true}, {\"check\": \"split-boundary regression 0\", \"actual\": [\"split-boundary\"], \"expected\": [\"split-boundary\"], \"passed\": true}, {\"check\": \"split-boundary regression 1\", \"actual\": [\"split-boundary\"], \"expected\": [\"split-boundary\"], \"passed\": true}, {\"check\": \"partition-completeness regression 0\", \"actual\": [\"partition-completeness\"], \"expected\": [\"partition-completeness\"], \"passed\": true}, {\"check\": \"partition-completeness regression 1\", \"actual\": [\"partition-completeness\"], \"expected\": [\"partition-completeness\"], \"passed\": true}, {\"check\": \"exclusive-disjoint regression 0\", \"actual\": [\"exclusive-disjoint\"], \"expected\": [\"exclusive-disjoint\"], \"passed\": true}, {\"check\": \"exclusive-disjoint regression 1\", \"actual\": [\"exclusive-disjoint\"], \"expected\": [\"exclusive-disjoint\"], \"passed\": true}, {\"check\": \"owner-preservation regression 0\", \"actual\": [\"owner-preservation\"], \"expected\": [\"owner-preservation\"], \"passed\": true}, {\"check\": \"owner-preservation regression 1\", \"actual\": [\"owner-preservation\"], \"expected\": [\"owner-preservation\"], \"passed\": true}, {\"check\": \"generation-preservation regression 0\", \"actual\": [\"generation-preservation\"], \"expected\": [\"generation-preservation\"], \"passed\": true}, {\"check\": \"generation-preservation regression 1\", \"actual\": [\"generation-preservation\"], \"expected\": [\"generation-preservation\"], \"passed\": true}, {\"check\": \"dynamic-disjoint-proof regression 0\", \"actual\": [\"dynamic-disjoint-proof\"], \"expected\": [\"dynamic-disjoint-proof\"], \"passed\": true}, {\"check\": \"dynamic-disjoint-proof regression 1\", \"actual\": [\"dynamic-disjoint-proof\"], \"expected\": [\"dynamic-disjoint-proof\"], \"passed\": true}, {\"check\": \"empty-access regression 0\", \"actual\": [\"empty-access\"], \"expected\": [\"empty-access\"], \"passed\": true}, {\"check\": \"empty-access regression 1\", \"actual\": [\"empty-access\"], \"expected\": [\"empty-access\"], \"passed\": true}, {\"check\": \"strided-footprint regression 0\", \"actual\": [\"strided-footprint\"], \"expected\": [\"strided-footprint\"], \"passed\": true}, {\"check\": \"strided-footprint regression 1\", \"actual\": [\"strided-footprint\"], \"expected\": [\"strided-footprint\"], \"passed\": true}, {\"check\": \"reverse-addresses regression 0\", \"actual\": [\"reverse-addresses\"], \"expected\": [\"reverse-addresses\"], \"passed\": true}, {\"check\": \"reverse-addresses regression 1\", \"actual\": [\"reverse-addresses\"], \"expected\": [\"reverse-addresses\"], \"passed\": true}, {\"check\": \"split-consumption regression 0\", \"actual\": [], \"expected\": [\"split-consumption\"], \"passed\": false}, {\"check\": \"split-consumption regression 1\", \"actual\": [], \"expected\": [\"split-consumption\"], \"passed\": false}], \"passed\": false}\n"},"fixed":{"elapsed_ms":46.787,"exit_code":0,"observations":[{"actual":[],"check":"well formed empty obligations","expected":[],"passed":true},{"actual":["split-boundary"],"check":"split-boundary regression 0","expected":["split-boundary"],"passed":true},{"actual":["split-boundary"],"check":"split-boundary regression 1","expected":["split-boundary"],"passed":true},{"actual":["partition-completeness"],"check":"partition-completeness regression 0","expected":["partition-completeness"],"passed":true},{"actual":["partition-completeness"],"check":"partition-completeness regression 1","expected":["partition-completeness"],"passed":true},{"actual":["exclusive-disjoint"],"check":"exclusive-disjoint regression 0","expected":["exclusive-disjoint"],"passed":true},{"actual":["exclusive-disjoint"],"check":"exclusive-disjoint regression 1","expected":["exclusive-disjoint"],"passed":true},{"actual":["owner-preservation"],"check":"owner-preservation regression 0","expected":["owner-preservation"],"passed":true},{"actual":["owner-preservation"],"check":"owner-preservation regression 1","expected":["owner-preservation"],"passed":true},{"actual":["generation-preservation"],"check":"generation-preservation regression 0","expected":["generation-preservation"],"passed":true},{"actual":["generation-preservation"],"check":"generation-preservation regression 1","expected":["generation-preservation"],"passed":true},{"actual":["dynamic-disjoint-proof"],"check":"dynamic-disjoint-proof regression 0","expected":["dynamic-disjoint-proof"],"passed":true},{"actual":["dynamic-disjoint-proof"],"check":"dynamic-disjoint-proof regression 1","expected":["dynamic-disjoint-proof"],"passed":true},{"actual":["empty-access"],"check":"empty-access regression 0","expected":["empty-access"],"passed":true},{"actual":["empty-access"],"check":"empty-access regression 1","expected":["empty-access"],"passed":true},{"actual":["strided-footprint"],"check":"strided-footprint regression 0","expected":["strided-footprint"],"passed":true},{"actual":["strided-footprint"],"check":"strided-footprint regression 1","expected":["strided-footprint"],"passed":true},{"actual":["reverse-addresses"],"check":"reverse-addresses regression 0","expected":["reverse-addresses"],"passed":true},{"actual":["reverse-addresses"],"check":"reverse-addresses regression 1","expected":["reverse-addresses"],"passed":true},{"actual":["split-consumption"],"check":"split-consumption regression 0","expected":["split-consumption"],"passed":true},{"actual":["split-consumption"],"check":"split-consumption regression 1","expected":["split-consumption"],"passed":true}],"passed":true,"stderr":"","stdout":"{\"observations\": [{\"check\": \"well formed empty obligations\", \"actual\": [], \"expected\": [], \"passed\": true}, {\"check\": \"split-boundary regression 0\", \"actual\": [\"split-boundary\"], \"expected\": [\"split-boundary\"], \"passed\": true}, {\"check\": \"split-boundary regression 1\", \"actual\": [\"split-boundary\"], \"expected\": [\"split-boundary\"], \"passed\": true}, {\"check\": \"partition-completeness regression 0\", \"actual\": [\"partition-completeness\"], \"expected\": [\"partition-completeness\"], \"passed\": true}, {\"check\": \"partition-completeness regression 1\", \"actual\": [\"partition-completeness\"], \"expected\": [\"partition-completeness\"], \"passed\": true}, {\"check\": \"exclusive-disjoint regression 0\", \"actual\": [\"exclusive-disjoint\"], \"expected\": [\"exclusive-disjoint\"], \"passed\": true}, {\"check\": \"exclusive-disjoint regression 1\", \"actual\": [\"exclusive-disjoint\"], \"expected\": [\"exclusive-disjoint\"], \"passed\": true}, {\"check\": \"owner-preservation regression 0\", \"actual\": [\"owner-preservation\"], \"expected\": [\"owner-preservation\"], \"passed\": true}, {\"check\": \"owner-preservation regression 1\", \"actual\": [\"owner-preservation\"], \"expected\": [\"owner-preservation\"], \"passed\": true}, {\"check\": \"generation-preservation regression 0\", \"actual\": [\"generation-preservation\"], \"expected\": [\"generation-preservation\"], \"passed\": true}, {\"check\": \"generation-preservation regression 1\", \"actual\": [\"generation-preservation\"], \"expected\": [\"generation-preservation\"], \"passed\": true}, {\"check\": \"dynamic-disjoint-proof regression 0\", \"actual\": [\"dynamic-disjoint-proof\"], \"expected\": [\"dynamic-disjoint-proof\"], \"passed\": true}, {\"check\": \"dynamic-disjoint-proof regression 1\", \"actual\": [\"dynamic-disjoint-proof\"], \"expected\": [\"dynamic-disjoint-proof\"], \"passed\": true}, {\"check\": \"empty-access regression 0\", \"actual\": [\"empty-access\"], \"expected\": [\"empty-access\"], \"passed\": true}, {\"check\": \"empty-access regression 1\", \"actual\": [\"empty-access\"], \"expected\": [\"empty-access\"], \"passed\": true}, {\"check\": \"strided-footprint regression 0\", \"actual\": [\"strided-footprint\"], \"expected\": [\"strided-footprint\"], \"passed\": true}, {\"check\": \"strided-footprint regression 1\", \"actual\": [\"strided-footprint\"], \"expected\": [\"strided-footprint\"], \"passed\": true}, {\"check\": \"reverse-addresses regression 0\", \"actual\": [\"reverse-addresses\"], \"expected\": [\"reverse-addresses\"], \"passed\": true}, {\"check\": \"reverse-addresses regression 1\", \"actual\": [\"reverse-addresses\"], \"expected\": [\"reverse-addresses\"], \"passed\": true}, {\"check\": \"split-consumption regression 0\", \"actual\": [\"split-consumption\"], \"expected\": [\"split-consumption\"], \"passed\": true}, {\"check\": \"split-consumption regression 1\", \"actual\": [\"split-consumption\"], \"expected\": [\"split-consumption\"], \"passed\": true}], \"passed\": true}\n"}},"verified":true,"visibility":"public"}