Skip to content

Add implementation of setTimeout for CVC5#933

Merged
marcoeilers merged 3 commits into
viperproject:masterfrom
superaxander:cvc-timeout
Jun 27, 2025
Merged

Add implementation of setTimeout for CVC5#933
marcoeilers merged 3 commits into
viperproject:masterfrom
superaxander:cvc-timeout

Conversation

@superaxander

Copy link
Copy Markdown
Contributor

I'm not sure if there is a specific reason why timeouts are not set for the CVC5 prover? The comment says that cvc5 does not support setting the timeout after instantiation but in my testing it works fine. (although it can sometimes exceed the timeout because it's not very strict about keeping to it) I looked through the release notes but couldn't find mention of this being a new feature.

@marcoeilers

Copy link
Copy Markdown
Contributor

Thanks a lot! I have no idea why whoever wrote the code thought this wasn't supported, but it's clearly working now.

@marcoeilers

marcoeilers commented Jun 27, 2025

Copy link
Copy Markdown
Contributor

Ah, maybe this is it: With your change (and with CVC5 version 1.3.0), if I enable resource bounds, I get the following error from CVC5:
invalid call to 'setOption' for option 'rlimit-per', solver is already fully initialized
Maybe this used to also happen for tlimit?

@superaxander

Copy link
Copy Markdown
Contributor Author

There seems to be a very simple list of options that are allowed to be changed, I believe reproducible-resource-limit might equate to rlimit-per. https://github.com/cvc5/cvc5/blob/58cda4cdc96a9cdc0e267ba4f4ddd00bcd653a1f/src/api/cpp/cvc5.cpp#L8654-L8659

@superaxander

Copy link
Copy Markdown
Contributor Author

Yes just tested it, changing rlimit-per to reproducible-resource-limit works. Kind of a strange and undocumented thing.

@marcoeilers

Copy link
Copy Markdown
Contributor

How weird. Elsewhere that's just listed as an alias for rlimit-per. tlimit-per just doesn't seem to have an alias.
But okay, who cares, as long as it works. Thanks again for spotting and fixing this!

@marcoeilers marcoeilers enabled auto-merge (squash) June 27, 2025 15:02
@marcoeilers

Copy link
Copy Markdown
Contributor

Turns out there was actually a moment when tlimit-per was not on the list: cvc5/cvc5@53c2bc3

@marcoeilers marcoeilers merged commit 26cc85c into viperproject:master Jun 27, 2025
2 checks passed
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.

2 participants