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

CVC 1.8 timeout tests failing in CI #278

Open
langston-barrett opened this issue Feb 4, 2025 · 1 comment
Open

CVC 1.8 timeout tests failing in CI #278

langston-barrett opened this issue Feb 4, 2025 · 1 comment
Labels
bug Something isn't working CI Issues related to continuous integration performance Issues related to compile-time or runtime performance

Comments

@langston-barrett
Copy link
Contributor

langston-barrett commented Feb 4, 2025

https://github.com/GaloisInc/what4/actions/runs/13142662183

  Timeout Tests
    valid test timeout:                            OK
    Z3
      Test itself is valid and completes (2.27 s): OK (5.09s)
      Test runs past timeout:                      OK (1.41s)
      Test with goal timeout (0.25 s):             OK (0.43s)
    CVC4
      Test itself is valid and completes (7.5 s):  OK (9.19s)
      Test runs past timeout:                      FAIL (2.87s)
        test/OnlineSolverTest.hs:463:
        Solver check query not interruptible (2.8689650130000004 s > expected 1.4 s)
        Use -p '/CVC4.Test runs past timeout/' to rerun this test only.
      Test with goal timeout (0.25 s):             AsyncCancelled
FAIL (1.66s)
        test/OnlineSolverTest.hs:485:
        solver goal timeout didn't occur
        Use -p '/CVC4.Test with goal timeout (0.25 s)/' to rerun this test only.
@RyanGlScott
Copy link
Contributor

It is strange that this failure only surfaced recently. What's more, I am able to reproduce the errors locally on my machine.

A wild shot in the dark: perhaps the performance characteristics of the CI runners were once such that these CVC4-related tests would take long enough that the timeout could reliably kick in, but the performance characteristics of the CI runners are now such that this no longer occurs. (I don't have any evidence for this claim, but I'm not sure what else might be causing this.) Either way, we should redesign these tests so that they aren't quite so sensitive to the performance characteristics of individual machines.

@RyanGlScott RyanGlScott added bug Something isn't working CI Issues related to continuous integration performance Issues related to compile-time or runtime performance labels Feb 4, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working CI Issues related to continuous integration performance Issues related to compile-time or runtime performance
Projects
None yet
Development

No branches or pull requests

2 participants