Run CI for install z3 in CI + z3 SMT struct fix [DO NOT REVIEW] #5949
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
7 tasks
Codecov Report
@@ Coverage Diff @@
## develop #5949 +/- ##
===========================================
+ Coverage 75.04% 75.14% +0.10%
===========================================
Files 1433 1435 +2
Lines 155817 156303 +486
===========================================
+ Hits 116932 117455 +523
+ Misses 38885 38848 -37
Continue to review full report at Codecov.
|
|
@thomasspriggs Looks like the z3 version on Windows (from chocolatey) and Ubuntu 18.04 are too old and do not handle datatypes. I think instead of using package manager version, we should be grabbing binaries from https://github.com/Z3Prover/z3/releases/tag/z3-4.8.10. |
|
The Ubuntu 18 job is just missing z3. I still need to investigate the Windows jobs. |
|
It could be that they support datatype to some extent, but the version in the Ubuntu 18.04 repo for Z3 is 4.4.1 (tagged 5 years ago) and the version in Chocolatey repo is 4.3.2 (tagged 6 years ago). The latest z3 version is 4.8.10. I think having different solver versions on different platforms is problematic. |
4 tasks
thomasspriggs
force-pushed
the
tas/smt_struct_fix_ci_test
branch
from
d8e422d to
e17e8c8
Compare
thomasspriggs
force-pushed
the
tas/smt_struct_fix_ci_test
branch
7 times, most recently
from
76672da to
7b582be
Compare
This was previously missing, which would cause any tests which needed Z3 to fail this job.
Because the `choco` installation of `z3` seems to be broken/outdated. Using `Invoke-WebRequest` instead of `choco` allows us to pin the version installed and to get a version which includes the `z3.exe`, not just `z3.dll`. Using `nuget` was also considered, so that we were still using a package manager. But the up to date `nuget` package was missing the `.exe` file. `wget` is supposed to be aliased to `Invoke-WebRequest` in powershell. However `Invoke-WebRequest` is used rather than `wget` as `wget` does not seem to work for windows github actions jobs.
This was previously missing, which would cause any tests which needed Z3 to fail this job.
For confirmation of version and that installation is successfull. This supports easier debugging for both the github actions `.yaml` and for future test failures. As a bonus we get fast failing CI jobs if the dependency isn't installed properly, because it fails at this step rather than during testing. This z3 version check is done as a separate step because adding to `$env:GITHUB_PATH` doesn't take effect the path until the next step.
thomasspriggs
force-pushed
the
tas/smt_struct_fix_ci_test
branch
from
7b582be to
bcf08be
Compare
This confirms that Z3 is present and working in CI, as well as that cbmc's support for Z3 is not entirely broken.
This commit fixes a `key not found` exception in `convert_type` during SMT2 encoding of structs using data types. Although structs were being mapped to SMT2 datatypes (in `datatype_map`) struct_tags were not.
This prevents auto upgrade of z3, in order to keep it inline with the version used on Windows. Note that the version currently being installed on Mac is already 4.8.10.
thomasspriggs
force-pushed
the
tas/smt_struct_fix_ci_test
branch
from
bcf08be to
cd88b8f
Compare
|
The work we wanted from this PR is merged. So the PR itself is no longer needed. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Run CI for install z3 in CI + z3 SMT struct fix [DO NOT REVIEW]