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

Yices invocation almost always fails #602

Closed
atomb opened this issue Dec 4, 2019 · 6 comments
Closed

Yices invocation almost always fails #602

atomb opened this issue Dec 4, 2019 · 6 comments

Comments

@atomb
Copy link
Contributor

atomb commented Dec 4, 2019

A recent change in What4 led to the Yices backend erroneously thinking that Yices didn't support bit vectors. This causes some of the saw-script tests to fail. It looks as though @robdockins has fixed the issue, though, so we just need to update the crucible submodule.

@brianhuffman
Copy link
Contributor

Do any of the integration tests in intTests use w4_unint_yices? If not, we should add one. I did run all the integration tests before I merged the last update-submodule-dependencies pull request.

@atomb
Copy link
Contributor Author

atomb commented Dec 4, 2019

Huh. Strange. Several of the intTests tests were failing on Jenkins overnight. I'll check locally.

@brianhuffman
Copy link
Contributor

I'll try it again too. It's possible that I accidentally had the wrong submodule version checked out when I ran the tests.

@brianhuffman
Copy link
Contributor

Yes, I'm seeing the failures now. I must have made some mistake yesterday when running the tests.

@brianhuffman
Copy link
Contributor

I think what happened is that I actually ran the right tests, looked at the end of the output, and didn't realize that there were any failures. I opened #603 in the hope that this won't be such an easy mistake to make in the future.

@brianhuffman
Copy link
Contributor

Fixed as of 4b0019b.

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

No branches or pull requests

2 participants