From 396147851e9bfd039c29192e1fedfc9d07925ce2 Mon Sep 17 00:00:00 2001
From: "z3prover-ci-bot[bot]"
 <305651407+z3prover-ci-bot[bot]@users.noreply.github.com>
Date: Thu, 16 Jul 2026 11:33:30 -0700
Subject: [PATCH] =?UTF-8?q?[fixer-selftest]=20Fix=20typo=20in=20euf=5Fac?=
 =?UTF-8?q?=5Fplugin.cpp=20comment:=20"betwen"=20=E2=86=92=20"between"=20(?=
 =?UTF-8?q?#10141)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

## 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>
---
 src/ast/euf/euf_ac_plugin.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/ast/euf/euf_ac_plugin.cpp b/src/ast/euf/euf_ac_plugin.cpp
index 89d25b154..705e46bbe 100644
--- a/src/ast/euf/euf_ac_plugin.cpp
+++ b/src/ast/euf/euf_ac_plugin.cpp
@@ -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]);