Skip to content

Incremental SMT back-end occasionally fails regression tests #7549

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.

Sign up for GitHub

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

Jump to bottom
Open
tautschnig opened this issue Feb 16, 2023 · 2 comments
Open

Incremental SMT back-end occasionally fails regression tests #7549

tautschnig opened this issue Feb 16, 2023 · 2 comments
Labels
CI SMT Backend Interface

Comments

@tautschnig
Copy link
Collaborator

I have seen this more than once before, and the latest instance is https://github.com/diffblue/cbmc/actions/runs/4196248319/jobs/7276954029:

Running incremental SMT2 solving via "z3 --smt2 -in"
Invalid SMT response "cbmc"
Invalid SMT response received from solver.

I don't recall whether it is always the same test that is failing (on this occasion: array-cell-sensitivity3/test_execution.desc), but all failures I have observed were in the "codecov-coverage-report" CI job. I have not managed to reproduce this failure locally.
@tautschnig
Copy link
Collaborator Author

https://github.com/diffblue/cbmc/actions/runs/4197648661/jobs/7280244383 is another example, and it happens to be the same regression test.

@tautschnig
Copy link
Collaborator Author

Adding one more: https://github.com/diffblue/cbmc/actions/runs/4222195921/jobs/7330414616.

tautschnig added a commit to tautschnig/cbmc that referenced this issue Feb 22, 2023
@tautschnig
Disable array-cell-sensitivity3 with new SMT back-end
be28f1e 
See diffblue#7549: this test appears to fail when building with coverage
annotation enabled (but succeeds otherwise).
@tautschnig tautschnig mentioned this issue Feb 22, 2023
Merged
3 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
CI SMT Backend Interface
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@tautschnig