Represent slices with native SMT sequences - #270
Conversation
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: a67b01145b
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| - run: curl -fsS "$PCSAT_URL" -o tests/thrust-pcsat-wrapper | ||
| env: | ||
| PCSAT_URL: https://thrust-ci-public.s3.ap-northeast-1.amazonaws.com/pcsat/thrust-pcsat-wrapper-873d558c6a |
There was a problem hiding this comment.
The test job downloads an executable from a mutable public S3 object and subsequently executes it through the UI tests without checking a digest or signature. This replaces the previously digest-pinned container image, so replacement or compromise of that object would provide direct code execution on every CI run; publish a checksum alongside the versioned artifact and verify it before cargo test.
Useful? React with 👍 / 👎.
| @@ -1,5 +1,6 @@ | |||
| //@check-pass | |||
| //@compile-flags: -C debug-assertions=off | |||
| //@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper | |||
There was a problem hiding this comment.
All sequence tests now override THRUST_SOLVER to use PCSat, but the application still defaults to Z3 (src/chc/solver.rs:117-126) while generated mutable-sequence constraints contain the non-Z3 seq.store operator. Consequently, users running Thrust normally on Vec or mutable-slice code receive a solver parse/error result even though CI passes; either select/provision PCSat by default or emit sequence updates in the default solver's supported dialect.
Useful? React with 👍 / 👎.
1 participant
using latest PCSat that supports Z3 Seq operations plus seq.store