Skip to content

Conversation

@karoliineh
Copy link
Member

@karoliineh karoliineh commented May 21, 2024

  • Makes sure that if the next widen threshold is bigger than max_ik (or smaller than man_ik), max_ik (or min_ik) is picked instead. (solves Interval sets are unsound due to larger-than-type ranges #1473)
  • Refactors the duplicate code of widen.upper_threshold and widen.lower_threshold of IntervalFunctor and IntervalSetFunctor to IntervalArith module, and uses this function for both.

@karoliineh karoliineh added cleanup Refactoring, clean-up bug unsound sv-comp SV-COMP (analyses, results), witnesses labels May 21, 2024
@karoliineh karoliineh added this to the SV-COMP 2025 milestone May 21, 2024
@karoliineh karoliineh requested a review from sim642 May 21, 2024 09:36
@sim642 sim642 linked an issue May 21, 2024 that may be closed by this pull request
@sim642
Copy link
Member

sim642 commented May 21, 2024

It would be nice to have tests for this. Instead of trying to construct programs with complex autotuning configurations, adding unit tests into intDomainTest.ml would be a nice way.

@sim642 sim642 merged commit 4f648ee into master May 22, 2024
@sim642 sim642 deleted the interval-widen-thresholds branch May 22, 2024 06:55
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

bug cleanup Refactoring, clean-up sv-comp SV-COMP (analyses, results), witnesses unsound

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Interval sets are unsound due to larger-than-type ranges

4 participants