Severity: CRITICAL
Location: scripts/interpretation/interpretation.py:1631
Description:
In _update_edge(), when updating an IPL complement predicate in the if p2 == l: block, the code updates p1's bounds but incorrectly appends p2's bounds to the updated_bnds list used for convergence tracking.
# Lines 1617-1633 in _update_edge
if p2 == l:
if p1 not in world.world:
world.world[p1] = interval.closed(0, 1)
# ... predicate_map update
if atom_trace:
_update_rule_trace(rule_trace_atoms, ..., world.world[p1], ...)
# Update P1's bounds
lower = max(world.world[p1].lower, 1 - world.world[p2].upper)
upper = min(world.world[p1].upper, 1 - world.world[p2].lower)
world.world[p1].set_lower_upper(lower, upper)
world.world[p1].set_static(static)
ip_update_cnt += 1
# BUG: Appending P2 instead of P1!
updated_bnds.append(world.world[p2]) # ← Line 1631: WRONG!
# Should be: updated_bnds.append(world.world[p1])
if store_interpretation_changes:
rule_trace.append((numba.types.uint16(t_cnt), numba.types.uint16(fp_cnt), comp, p1, interval.closed(lower, upper)))
Comparison with _update_node (CORRECT):
# Lines 1511-1527 in _update_node
if p2 == l:
# ... same setup code ...
lower = max(world.world[p1].lower, 1 - world.world[p2].upper)
upper = min(world.world[p1].upper, 1 - world.world[p2].lower)
world.world[p1].set_lower_upper(lower, upper)
world.world[p1].set_static(static)
ip_update_cnt += 1
updated_bnds.append(world.world[p1]) # ← Line 1525: CORRECT!
Impact:
- Convergence detection broken: The convergence delta calculation (lines 1643-1647) iterates through
updated_bnds to compute max delta. Using p2's bound (which wasn't actually updated) instead of p1's bound (which was updated) produces incorrect deltas.
- Only affects edges with IPL constraints: Nodes are unaffected since _update_node has correct code.
- Silent failure: No error raised, convergence just doesn't work correctly.
Fix:
updated_bnds.append(world.world[p1])
Severity: CRITICAL
Location:
scripts/interpretation/interpretation.py:1631Description:
In
_update_edge(), when updating an IPL complement predicate in theif p2 == l:block, the code updatesp1's bounds but incorrectly appendsp2's bounds to theupdated_bndslist used for convergence tracking.Comparison with _update_node (CORRECT):
Impact:
updated_bndsto compute max delta. Using p2's bound (which wasn't actually updated) instead of p1's bound (which was updated) produces incorrect deltas.Fix: