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

cvc5 is too fast for challenge problem in timeout test #210

Open
arjunvish opened this issue Jul 1, 2022 · 0 comments
Open

cvc5 is too fast for challenge problem in timeout test #210

arjunvish opened this issue Jul 1, 2022 · 0 comments
Labels
bug Something isn't working

Comments

@arjunvish
Copy link
Collaborator

arjunvish commented Jul 1, 2022

The challenge problem used to test solver timeouts is solved too quickly by cvc5:

CVC5
      Test itself is valid and completes (0.4 s):  OK (0.41s)
      Test runs past timeout:                      IGNORED
        solver runs test faster than reasonable timing threshold; skipping
      Test with goal timeout (0.25 s):             OK (0.42s)

We'll need to come up with a new challenge problem that takes cvc5 at least a couple of seconds longer (and is also challenging for the other solvers)

@arjunvish arjunvish added the bug Something isn't working label Jul 1, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working
Projects
None yet
Development

No branches or pull requests

1 participant