FA-11491 / Static analysis soundness / Open access

Joining branch intervals discards a reachable endpoint · case 01

Joining branch intervals discards a reachable endpoint.

Verified by executionVariant 1 · 7 checks per implementationDownload source bundle ↓JSON ↗

ROOT CAUSE

The join intersects alternative outcomes instead of enclosing both.

VERIFIED REPAIR

Use the minimum lower bound and maximum upper bound, treating None as unreachable bottom.

Unsuccessful approach: Taking only the first reachable interval still discards values from the second branch.

Case contract

Join two integer closed intervals or None for unreachable; return a list enclosing their union, or None if both are unreachable.

Why this case matters

A deterministic offline analysis model exposing a specific soundness or precision boundary; it does not implement a complete language analyzer.

1 / The failure

Exit 1

"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(a, b):
    if a is None: return b
    if b is None: return a
    return [max(a[0],b[0]), min(a[1],b[1])]
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('disjoint branches',solve([0,N],[N+2,N+3]),[0,N+3])
check('nested second branch',solve([0,N+4],[1,N+2]),[0,N+4])
check('second expands lower bound',solve([0,N],[-N,0]),[-N,N])
check('left unreachable',solve(None,[N,N]),[N,N])
check('right unreachable',solve([N,N],None),[N,N])
check('both unreachable',solve(None,None),None)
check('identical singleton',solve([N,N],[N,N]),[N,N])
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)

Boundary fixture	Actual	Expected	Outcome
disjoint branches	`[3, 1]`	`[0, 4]`	Failed
nested second branch	`[1, 3]`	`[0, 5]`	Failed
second expands lower bound	`[0, 0]`	`[-1, 1]`	Failed
left unreachable	`[1, 1]`	`[1, 1]`	Passed
right unreachable	`[1, 1]`	`[1, 1]`	Passed
both unreachable	`None`	`None`	Passed
identical singleton	`[1, 1]`	`[1, 1]`	Passed

SHA-256 / 3171a6c2d70616d4445fab425bcdc1078a832bc1a6be299ee5f44bddd3a9e85d

2 / The unsuccessful fix

Exit 1

"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(a, b):
    return a if a is not None else b
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('disjoint branches',solve([0,N],[N+2,N+3]),[0,N+3])
check('nested second branch',solve([0,N+4],[1,N+2]),[0,N+4])
check('second expands lower bound',solve([0,N],[-N,0]),[-N,N])
check('left unreachable',solve(None,[N,N]),[N,N])
check('right unreachable',solve([N,N],None),[N,N])
check('both unreachable',solve(None,None),None)
check('identical singleton',solve([N,N],[N,N]),[N,N])
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)

Boundary fixture	Actual	Expected	Outcome
disjoint branches	`[0, 1]`	`[0, 4]`	Failed
nested second branch	`[0, 5]`	`[0, 5]`	Passed
second expands lower bound	`[0, 1]`	`[-1, 1]`	Failed
left unreachable	`[1, 1]`	`[1, 1]`	Passed
right unreachable	`[1, 1]`	`[1, 1]`	Passed
both unreachable	`None`	`None`	Passed
identical singleton	`[1, 1]`	`[1, 1]`	Passed

SHA-256 / a5c924dc1974cbf2b025d7571598c9c326eacdccecd3f1e6321d17d2c324caab

3 / The verified repair

Exit 0

"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(a, b):
    if a is None: return b
    if b is None: return a
    return [min(a[0],b[0]), max(a[1],b[1])]
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('disjoint branches',solve([0,N],[N+2,N+3]),[0,N+3])
check('nested second branch',solve([0,N+4],[1,N+2]),[0,N+4])
check('second expands lower bound',solve([0,N],[-N,0]),[-N,N])
check('left unreachable',solve(None,[N,N]),[N,N])
check('right unreachable',solve([N,N],None),[N,N])
check('both unreachable',solve(None,None),None)
check('identical singleton',solve([N,N],[N,N]),[N,N])
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)

Boundary fixture	Actual	Expected	Outcome
disjoint branches	`[0, 4]`	`[0, 4]`	Passed
nested second branch	`[0, 5]`	`[0, 5]`	Passed
second expands lower bound	`[-1, 1]`	`[-1, 1]`	Passed
left unreachable	`[1, 1]`	`[1, 1]`	Passed
right unreachable	`[1, 1]`	`[1, 1]`	Passed
both unreachable	`None`	`None`	Passed
identical singleton	`[1, 1]`	`[1, 1]`	Passed

SHA-256 / 580865f7f25fc2e04c7506f8a858642097c570c17c512bd9dd60cd558dd790d3

Verification & scope

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.

Observations recorded using Python 3.12.14 at 2026-09-29T14:38:48.438447+00:00.

Case digest / b7fe4e54e9c651150b256ea9b35bfc9c384d056a87cc180295abc2967affda05