vbpf / prevail / 22275933828

89%

push

github

Fix widening termination by removing constraint re-addition (#960)

TypeToNumDomain::widen called collect_type_dependent_constraints and
re-added intervals via set() after zone widening. This triggered eager
normalization (close_after_widen), which could create contradictions
producing bottom and causing infinite fixed-point iteration.

The fix removes the constraint re-addition from widen — this logic is
correct in join (where precision matters) but defeats widening's
termination guarantee. The separate known issue of eager normalization
in the zone domain constructor (split_dbm.hpp:145) is architectural
and remains deferred.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Signed-off-by: Elazar Gershuni <elazarg@gmail.com>

1 of 1 new or added line in 1 file covered. (100.0%)

13145 of 14848 relevant lines covered (88.53%)

4640721.39 hits per line