mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-22 15:05:51 +00:00
Code Activity

[fixer-selftest] Fix typo in euf_ac_plugin.cpp comment: "betwen" → "between" (#10141)

Browse source 
## Automated workflow self-test

This PR is an **automated workflow self-test** of the `fixer-selftest` /
`snapshot-regression-fixer` pipeline running on the self-hosted
`rise-runner-1` pool. Its purpose is to verify that Copilot inference
runs and that the `create-pull-request` safe output can open a real
**draft** pull request on `Z3Prover/z3`.

### The fix

- **File:** `src/ast/euf/euf_ac_plugin.cpp` (line 995)
- **Before:** `// add difference betwen dst.l and src.l to both src.l,
src.r`
- **After:** `// add difference between dst.l and src.l to both src.l,
src.r`

A single spelling mistake (`betwen` → `between`) in a `//` code comment.

### Why no rebuild is needed

The change is **comment-only** — no code, string literals, identifiers,
or build files were touched — so it cannot affect z3's behaviour and
requires no compilation or testing.

### For maintainers

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




> Generated by [Self-test the agentic PR pipeline with a tiny z3 comment
fix](https://github.com/Z3Prover/bench/actions/runs/29523479037) · 54.5
AIC · ⌖ 18.9 AIC · ⊞ 8K ·
[◷](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.65, model:
claude-opus-4.8, id: 29523479037, workflow_id: fixer-selftest, run:
https://github.com/Z3Prover/bench/actions/runs/29523479037 -->

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

Co-authored-by: z3prover-ci-bot[bot] <305651407+z3prover-ci-bot[bot]@users.noreply.github.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
z3prover-ci-bot[bot] 2026-07-16 11:33:30 -07:00 • committed by GitHub
parent 436237bfbb
commit 396147851e
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/euf/euf_ac_plugin.cpp
View file

@ -992,7 +992,7 @@ namespace euf {
SASSERT(is_correct_ref_count(monomial(src.r), m_src_r_counts));
SASSERT(is_correct_ref_count(monomial(dst.l), m_dst_l_counts));
SASSERT(is_correct_ref_count(monomial(dst.r), m_dst_r_counts));
// add difference betwen dst.l and src.l to both src.l, src.r
// add difference between dst.l and src.l to both src.l, src.r
for (auto n : monomial(dst.l)) {
unsigned id = n->id();
SASSERT(m_dst_l_counts[id] >= m_src_l_counts[id]);