Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Improve autotune for octagon #1450

Merged
merged 10 commits into from
May 23, 2024
Merged

Improve autotune for octagon #1450

merged 10 commits into from
May 23, 2024

Conversation

karoliineh
Copy link
Member

@karoliineh karoliineh commented May 9, 2024

I analyzed the SV-COMP NoOverflows tasks where Mopsa succeeded, but we failed, and uncovered some tasks where we succeeded when activating apron analysis but failed with autotune.

This PR proposes a fix that allows us to further succeed in 11 tasks (nla-digbench-scaling/sqrt1-.*) with autotune.

TODO:

  • Generalize the case handling operations inside LNot

@sim642 sim642 added the relational Relational analyses (Apron, affeq, lin2var) label May 9, 2024
@sim642 sim642 added this to the SV-COMP 2025 milestone May 9, 2024
src/autoTune.ml Outdated Show resolved Hide resolved
src/autoTune.ml Outdated Show resolved Hide resolved
Copy link
Collaborator

@DrMichaelPetter DrMichaelPetter left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM

@sim642 sim642 merged commit aae8d90 into master May 23, 2024
21 checks passed
@sim642 sim642 deleted the improve-autotune branch May 23, 2024 07:05
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
precision relational Relational analyses (Apron, affeq, lin2var) sv-comp
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

3 participants