Skip to content

Making resource bounds the default instead of timeouts#949

Merged
marcoeilers merged 5 commits intomasterfrom
meilers_resource_bounds_default
Nov 26, 2025
Merged

Making resource bounds the default instead of timeouts#949
marcoeilers merged 5 commits intomasterfrom
meilers_resource_bounds_default

Conversation

@marcoeilers
Copy link
Copy Markdown
Contributor

@marcoeilers marcoeilers commented Nov 12, 2025

  • Making resource bounds the default instead of the current timeouts for checks. This removes the main source of non-determinism when using Silicon.
  • Replacing the old flag --proverEnableResourceBounds with a new flag --proverEnableTimeBounds, which can be used to get the old behavior.
  • Also doing some cleanup and removing old options whose names are Z3-specific (--z3X), which have been deprecated forever, and for which there are generic alternatives (--proverX).
  • For time to resource conversions, we add different options for Z3 and CVC5, because their resources work differently. I'm reasonably certain that the Z3 conversion rate is decent, I'm much less certain about the CVC5 one.

Tested with:

  • Nagini tests in CI and on my laptop
  • SCION router on my laptop
  • Viper tests in CI and on my laptop
  • Gobra tests on my laptop
  • Prusti tests on my laptop
    For all those, the change did not add spurious errors and only slightly changed overall verification time.

@marcoeilers marcoeilers enabled auto-merge (squash) November 26, 2025 12:49
@marcoeilers marcoeilers merged commit a8e5d1d into master Nov 26, 2025
4 checks passed
@marcoeilers marcoeilers deleted the meilers_resource_bounds_default branch November 26, 2025 13:02
AndreaKe pushed a commit that referenced this pull request Dec 2, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant