3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-25 01:50:33 +00:00

[fixer-selftest] Fix comment typo in elim_unconstrained.cpp (accomodate → accommodate) (#9925)

This is an **automated workflow self-test** of the `fixer-selftest` /
`snapshot-regression-fixer` pipeline running on the self-hosted
**`rise-runner-1`** runner pool. Its sole purpose is to prove the
end-to-end agentic pipeline works: Copilot inference runs, and the
`create-pull-request` safe output can open a real **draft** pull request
on `Z3Prover/z3` using the configured PAT. It is intentionally
build-free.

### Change
- **File:** `src/ast/simplifiers/elim_unconstrained.cpp` (module-header
`/*++ ... */` comment)
- **Before:** `   - it does not accomodate side constraints.`
- **After:** `   - it does not accommodate side constraints.`

A plain spelling correction in a comment: `accomodate` → `accommodate`.
The diff is a single line.

### Why this is safe
The change is **comment-only** — it touches no code, identifiers, string
literals, build files, or tests, and therefore **cannot affect z3's
behaviour or output**. Because of that, no compilation or testing was
performed and **no rebuild is needed** to be confident it is correct.

### For maintainers
This is a genuine, correct fix, so you are welcome to **merge** it.
Equally, you may simply **close** it — the success of this self-test
does not depend on the PR being merged.




> Generated by [Self-test the agentic PR pipeline with a tiny z3 comment
fix](https://github.com/Z3Prover/bench/actions/runs/27987685681) · 299.1
AIC · ⌖ 53.6 AIC · ⊞ 35.5K ·
[◷](https://github.com/search?q=repo%3AZ3Prover%2Fz3+%22gh-aw-workflow-id%3A+fixer-selftest%22&type=pullrequests)

<!-- gh-aw-agentic-workflow: Self-test the agentic PR pipeline with a
tiny z3 comment fix, engine: copilot, version: 1.0.60, model:
claude-opus-4.8, id: 27987685681, workflow_id: fixer-selftest, run:
https://github.com/Z3Prover/bench/actions/runs/27987685681 -->

<!-- gh-aw-workflow-id: fixer-selftest -->
<!-- gh-aw-workflow-call-id: Z3Prover/bench/fixer-selftest -->

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Lev Nachmanson 2026-06-22 15:51:26 -07:00 committed by GitHub
parent 2067a227ef
commit 5bba757131
No known key found for this signature in database
GPG key ID: B5690EEEBB952194

View file

@ -16,7 +16,7 @@ Abstract:
All variables x, y, z, .. can eventually be eliminated, but the tactic requires a global
analysis between each elimination. We address this by using reference counts and maintaining
a heap of reference counts.
- it does not accomodate side constraints. The more general invertibility reduction methods, such
- it does not accommodate side constraints. The more general invertibility reduction methods, such
as those introduced for bit-vectors use side constraints.
- it is not modular: we detach the expression invertion routines to self-contained code.