Three `clang-analyzer-deadcode.DeadStores` warnings flagged by
clang-tidy: redundant bit-shifts in the log2 functions and an
unreachable assignment in `def::from_row()`.
## Changes
- **`src/util/util.cpp`** — `log2()` and `uint64_log2()`: Remove `v >>=
1` in the final `if (v & 0x2)` block. Only `r |= 1` matters; `v` is
never read after that point.
```cpp
// Before
if (v & 0x2) {
v >>= 1; // dead store
r |= 1;
}
// After
if (v & 0x2) {
r |= 1;
}
```
- **`src/math/simplex/model_based_opt.cpp`** — `def::from_row()`: Remove
`sign = true` assignment when `div < 0`. `sign` is only consumed earlier
in the function (`if (!sign)`) and is not read again after this point.
<!-- START COPILOT CODING AGENT SUFFIX -->
- Fixes#10333
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Memoize derivative_cofactors per regex in an owning cache so each regex's
cofactors are computed once per top-level solve. The cache is reset at the
start of solve()/solve_and() and freed in the destructor.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9
Per-variable extra constraints are now expressed as additional (var in R')
memberships passed to solve_and, so the var_extra parameter is dropped from
solve/solve_and and the internal decide_dnf. Tests updated to route extra
constraints through solve_and.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9
Extract the guard_set class (element-value set over derivative cofactor
guards) from the anonymous namespace in seq_monadic.cpp into a
self-contained guard_set.h / guard_set.cpp pair.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9
## Summary
Register the opt-in seq_monadic benchmark harness in test-z3.
The harness reads either Z3_SEQ_BENCH_FILE or all SMT2 files under
Z3_SEQ_BENCH_DIR, supports Brz and light-Ant modes through
Z3_SEQ_MONADIC_MODE, and reports per-file CSV timing and verdict
information.
The `agent` job in the Clang-Tidy Warning Fixer workflow was spending
most of its runtime waiting on a full clang-tidy build, then failing
before it could complete its safe-output path. This change narrows the
prompt so the agent can make a bounded decision from early diagnostics
instead of treating the full build as a prerequisite.
- **Prompt guardrail**
- Add a runtime-budget section to the compiled workflow prompt in
`build-warning-fixer.lock.yml`.
- Instruct the agent to stop after it has enough diagnostics for one
safe fix, or after 15 minutes.
- **Build scope reduction**
- Switch initial diagnostic collection to a `shell`-only build.
- Explicitly avoid waiting for a full `shell + test-z3` clang-tidy build
before deciding whether to act.
- **Fallback behavior**
- Direct the agent to emit `noop` when it cannot reach a safe, validated
fix within the time budget.
- Keep `test-z3` optional unless it is already available or cheap to
build within the remaining budget.
Example of the new prompt guidance:
```yaml
- Use `cmake --build build --target shell -- -k 0 2>&1 | tee /tmp/gh-aw/agent/clang-tidy-build.log` for initial diagnostic collection.
- Do not wait for the full `shell` build to finish before deciding what to do.
- Stop once you have enough diagnostics for one small, high-confidence fix, or after 15 minutes.
- If no safe fix is ready in that budget, call `noop`.
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
## Summary
Pin constant elements extracted while parsing sequence terms so they
remain alive throughout monadic decomposition.
Without these references, character ASTs could be reclaimed while still
stored as raw pointers in decomposition atoms, causing assertion
failures, fast-fail exits, and access violations during derivative
construction.
The fix eliminates 26 previously observed process failures in the regex
benchmark corpus. No stack-depth bailout is needed for these failures.
Emscripten worker threads spawned for long-running Z3 operations (e.g.
`solver.check()`) are never cleaned up, keeping the Node.js process
alive after Z3 is done.
The `killThreads` helper already existed internally in `jest.ts` but was
never part of the public package.
## Changes
- **`src/kill-threads.ts`** (new) — extracts `killThreads(em)` into a
standalone module; calls `em.PThread.terminateAllThreads()` then polls
until all workers are gone (5 s timeout)
- **`src/node.ts`** — re-exports `killThreads` so it is part of the
published `z3-solver` API
- **`src/jest.ts`** — simplified to re-export from `./kill-threads`
instead of duplicating ~45 lines
- **`src/kill-threads.test.ts`** (new) — unit tests for the exported
function
- **`PUBLISHED_README.md`** — documents the new API
## Usage
```typescript
import { init, killThreads } from 'z3-solver';
const api = await init();
// ... use Z3 ...
await killThreads(api.em);
```
<!-- START COPILOT CODING AGENT SUFFIX -->
- Fixes#7070
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Replace the TPTP and Z3_TPTP_DUMP_SMT2 environment variables in
tptp_frontend.cpp with a new 'tptp' configuration module (src/params/tptp.pyg)
exposing tptp.root and tptp.dump_smt2 parameters.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9
Light-weight Antimirov cofactors for seq_monadic
================================================
Overview
--------
The seq_monadic solver explores symbolic regex derivatives when
computing live
states and product transitions. Its original transition representation
used
Brzozowski cofactors.
This change adds a light-weight Antimirov representation. It first
computes the
existing Brzozowski cofactors and then decomposes targets whose outer
shape is
s1 | ... | sn
or
(s1 | ... | sn) . tail
into separate transitions. Concatenations are maintained in
right-associative
form, so a distributable union occurs as the head of the concatenation.
Targets are reconstructed with mk_regex_concat to preserve
normalization.
After decomposition, transitions with the same target are merged by
disjoining
their guards. The existing path-aware cofactor traversal and range
predicates
are therefore retained.
Example
-------
For
r = .* a .{k}
the Brzozowski cofactors have the shape
[a, r | .{k}]
[^a, r]
The light-weight Antimirov transformation produces
[., r]
[a, .{k}]
This preserves the language while avoiding the deterministic subset
states
that grow exponentially on this family.
Modes
-----
seq_monadic exposes two transition modes:
light_antimirov default
brzozowski retained as an explicit option
The implementation is seq_rewriter::light_ant_derivative_cofactors.
Correctness
-----------
The seq_monadic unit tests run in both modes. They cover character and
generic
element sequences, multiple and repeated variables, variable
constraints,
bounded loops, conjunctions of memberships, and witness construction. A
focused test checks the cofactor transformation above. The complete
94-test
unit suite used during evaluation passed. The benchmark harness is not
registered as a normal unit test; after detaching it, all 93 registered
tests
pass.
Benchmark evaluation
--------------------
The final optimized comparison used all 1,545 SMT2 files under
C:\git\bench\inputs\regexes. Each file was run in a separate process
with a
15-second timeout. There were 1,513 cases where both modes completed
without a
process failure or timeout.
Brzozowski Light-Ant
paired solver time 94.98 s 63.26 s
median solver time 1.734 ms 0.710 ms
derivative calls 5.70 M 3.39 M
cofactors 13.33 M 6.99 M
live states 2.74 M 0.44 M
product states 652.8 K 642.8 K
Light-Ant reduced paired solver time by 33.4%, derivative calls by
40.5%,
cofactors by 47.5%, and live states by 84.0%. It was faster on 1,091
cases;
Brzozowski was faster on 421 cases.
Light-Ant changed 131 Brzozowski undef results to sat. There were no
reverse
verdict changes and no mismatches against known sat/unsat statuses. Both
modes
had two timeouts. Process failures decreased from 30 to 27.
By corpus, paired solver time improved by 39.1% on ClemensRegex and by
11.9% on
MargusRegex.
Alternatives considered
-----------------------
Direct use of full Antimirov derivatives was also evaluated. It
introduced
large performance outliers, particularly around intersections, and
produced
additional undef results and timeouts. Disabling intersection-over-union
distribution improved some of these cases but remained slower and less
robust
than the light-weight transformation. The direct full-Ant mode was
therefore
removed from this change.
Copilot-Session: a2ce3573-4e15-4a4a-afb5-21e3cb04e4a2
This is another PR towards the goal of getting Z3 to compile cleanly
when included via FetchContents into clang-tidy, which uses a pretty
strict set of warnings. (Only 4 more warnings after this one!)
This PR adds -Wignored-qualifiers. It detects only one violation: a
function whose by-value return type (unsigned) has a const qualifier.
Here is the error message:
```
/Users/daviddetlefs/z3/src/math/lp/dioph_eq.cpp:1518:9: warning: 'const' type qualifier on return type has no effect [-Wignored-qualifiers]
1518 | const unsigned sub_index(unsigned k) const {
| ^~~~~
```
Seems worth fixing.
This updates the existing agentic workflow from generic build-warning
cleanup to a clang-tidy-based loop: compile Z3 with Clang, inspect
clang-tidy/compiler diagnostics, and open a PR only for small,
semantics-preserving fixes.
- **Workflow scope**
- Renames and repurposes `build-warning-fixer` as a clang-tidy warning
fixer.
- Keeps the existing agentic PR flow, but narrows it to clang/clang-tidy
findings from the current run.
- **Build/analyze path**
- Switches the authored workflow prompt to use the repo’s CMake + Ninja
build with `clang`/`clang++`.
- Enables `CMAKE_CXX_CLANG_TIDY=clang-tidy` and exports compile commands
for tool-driven analysis.
- Captures configure/build logs in the agent artifact directory for
post-run diagnosis.
- **Agent behavior**
- Instructs the agent to classify clang-tidy warnings, compiler
warnings, and build errors from the build log.
- Biases toward localized fixes only: e.g. `override`,
`[[maybe_unused]]`, `nullptr`, dead locals.
- Explicitly prefers `noop` over speculative edits when diagnostics are
broad, risky, or design-affecting.
- **Generated workflow**
- Regenerates the compiled lockfile to reflect the new prompt and
current auth/permission model used by other agentic workflows in this
repo.
```yaml
CC=clang CXX=clang++ cmake -GNinja -S . -B build \
-DCMAKE_BUILD_TYPE=Debug \
-DCMAKE_EXPORT_COMPILE_COMMANDS=ON \
-DCMAKE_CXX_CLANG_TIDY=clang-tidy \
2>&1 | tee /tmp/gh-aw/agent/clang-tidy-configure.log
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
## Summary
Adds a global configuration parameter **`suppress_platform_verbose`**
(bool, default `false`).
When set to `true`, memory and time information is suppressed from
verbose output — the same behavior as the `-V` flag proposed in #10301,
but driven by a global parameter instead of a dedicated command-line
switch. This yields deterministic, platform-independent verbose output
that is useful for testing and diffing.
Usage:
```
z3 -v:2 suppress_platform_verbose=true problem.smt2
```
## Approach
Instead of introducing a `-V` command-line flag (#10301), this registers
`suppress_platform_verbose` as a global parameter via `env_params`,
wired to a lightweight `get_suppress_platform_verbose()` flag in `util`.
Verbose output sites guard only their **memory** (`mem_stat`) and
**time** (`m_watch` / `:time` / `:before-memory` / `:after-memory`)
fields on this flag. Platform-independent counters (e.g. `:cost`,
`:threshold`, `:elim-vars`) are always emitted.
Affected sites:
- SAT: asymm-branch, probing, scc, simplifier (subsumer /
blocked-clauses / resolution), solver stats (`sat.stats`, `:memory`,
`mk_stat`)
- SMT: context stats (`smt.stats`)
- Tactic report (`:time`, `:before-memory`, `:after-memory`)
## Validation
- Release build succeeds.
- `suppress_platform_verbose` appears in `z3 -pd` with the correct
type/default, and is accepted on the command line.
- All 93 `test-z3 /a` unit tests pass.
Closes the need for the `-V` switch in #10301.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9
### What it does
Fixes an inverted precondition assertion in `grobner::pop_scope`
(`src/math/grobner/grobner.cpp`).
```cpp
void grobner::pop_scope(unsigned num_scopes) {
SASSERT(num_scopes >= get_scope_level()); // was reversed
unsigned new_lvl = get_scope_level() - num_scopes; // requires num_scopes <= level
...
m_scopes.shrink(new_lvl);
}
```
`get_scope_level()` returns `m_scopes.size()` (grobner.h). The body
computes
`new_lvl = get_scope_level() - num_scopes` and calls
`m_scopes.shrink(new_lvl)`,
which is only well-defined when `num_scopes <= get_scope_level()`. The
assertion
stated the opposite (`>=`), so in debug builds it would fire on any
valid partial
pop (e.g. popping one of several scopes) while failing to catch the
unsigned
underflow it was meant to guard against. Changed to `<=`.
### Evidence
- `get_scope_level() const { return m_scopes.size(); }`
(`src/math/grobner/grobner.h`).
- Compiled the translation unit with MSVC and `Z3DEBUG` defined (so the
`SASSERT`
is active): builds cleanly.
### What we did not verify
This is a debug-only (`SASSERT`) correctness fix and has no effect on
release
builds. No behavioral test was added.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: ad2c295d-7523-48cf-b786-b435b833e3af
https://github.com/Z3Prover/z3/pull/10284 changed the UNREACHABLE macro
in debug.h to use __builtin_unreachable() to indicate to the compiler
that the
code leading it should be considered unreachable.
In https://github.com/Z3Prover/z3/pull/10295 Copilot figured out that
this was wrong: the unreachable macro makes calls, which shouldn't be
elided, and whose arguments should be evaluated. It partially fixed the
problem by declaring invoke_exit_action to be `[[noreturn]]`. This
eliminated warnings in non-debug builds, but when Z3_DEBUG is enabled,
`UNREACHABLE` ends with an invocation of `INVOKE_DEBUGER()`. This can
call `invoke_debugger()`, which *can* actually return (so it can't be
given the `[[noreturn]]` attribute. So we still get warnings in debug
builds.
This PR fixes those, creating a Z3_unreachable_case macro, which is just
a combination of `UNREACHABLE()` and `Z3_fallthrough`. It uses that in
the places that give warnings.
It seemed better to me to still have these cases have a single macro,
rather than `UNREACHABLE` followed by an explicit `Z3_fallthrough`; this
seemed to me like it would confuse people -- "how can you fall through
if this code is unreachable?" But I'm open to alternative suggestions!
This addresses stale generated Agentic Workflow artifacts by recompiling
the workflow sources and updating the checked-in lock outputs. The
update brings lockfiles and shared action pin metadata back in sync with
the current compiler/runtime generation.
- **Scope of regeneration**
- Recompiled all Agentic Workflow markdown definitions in
`.github/workflows/*.md` into their corresponding `.lock.yml` outputs.
- Updated generated maintenance workflow output in
`.github/workflows/agentics-maintenance.yml`.
- **Pinned dependency/metadata refresh**
- Refreshed `.github/aw/actions-lock.json` and lockfile manifests
(actions, container digests, compiler metadata) to the latest generated
state.
- Resulting lock headers now reflect the current compiler/toolchain
metadata used for generation.
- **Auth/runtime shape in generated lockfiles**
- Regenerated lock outputs include current AW-generated runtime/env
wiring for Copilot execution paths and token handling where applicable.
```yaml
# Example (lockfile header after regeneration)
# gh-aw-metadata:
# compiler_version: "v0.83.4"
```
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Bumps [actions/cache/save](https://github.com/actions/cache) from 5.0.5
to 6.1.0.
<details>
<summary>Release notes</summary>
<p><em>Sourced from <a
href="https://github.com/actions/cache/releases">actions/cache/save's
releases</a>.</em></p>
<blockquote>
<h2>v6.1.0</h2>
<h2>What's Changed</h2>
<ul>
<li>Bump <code>@actions/cache</code> to v6.1.0 - handle read-only cache
access by <a
href="https://github.com/jasongin"><code>@jasongin</code></a> in <a
href="https://redirect.github.com/actions/cache/pull/1768">actions/cache#1768</a></li>
</ul>
<p><strong>Full Changelog</strong>: <a
href="https://github.com/actions/cache/compare/v6...v6.1.0">https://github.com/actions/cache/compare/v6...v6.1.0</a></p>
<h2>v6.0.0</h2>
<h2>What's Changed</h2>
<ul>
<li>Update packages, migrate to ESM by <a
href="https://github.com/Samirat"><code>@Samirat</code></a> in <a
href="https://redirect.github.com/actions/cache/pull/1760">actions/cache#1760</a></li>
</ul>
<p><strong>Full Changelog</strong>: <a
href="https://github.com/actions/cache/compare/v5...v6.0.0">https://github.com/actions/cache/compare/v5...v6.0.0</a></p>
<h2>v5.1.0</h2>
<h2>What's Changed</h2>
<ul>
<li>Bump <code>@actions/cache</code> to v5.1.0 - handle read-only cache
access by <a
href="https://github.com/jasongin"><code>@jasongin</code></a> in <a
href="https://redirect.github.com/actions/cache/pull/1775">actions/cache#1775</a></li>
</ul>
<p><strong>Full Changelog</strong>: <a
href="https://github.com/actions/cache/compare/v5...v5.1.0">https://github.com/actions/cache/compare/v5...v5.1.0</a></p>
</blockquote>
</details>
<details>
<summary>Changelog</summary>
<p><em>Sourced from <a
href="https://github.com/actions/cache/blob/main/RELEASES.md">actions/cache/save's
changelog</a>.</em></p>
<blockquote>
<h1>Releases</h1>
<h2>How to prepare a release</h2>
<blockquote>
<p>[!NOTE]
Relevant for maintainers with write access only.</p>
</blockquote>
<ol>
<li>Switch to a new branch from <code>main</code>.</li>
<li>Run <code>npm test</code> to ensure all tests are passing.</li>
<li>Update the version in <a
href="https://github.com/actions/cache/blob/main/package.json"><code>https://github.com/actions/cache/blob/main/package.json</code></a>.</li>
<li>Run <code>npm run build</code> to update the compiled files.</li>
<li>Update this <a
href="https://github.com/actions/cache/blob/main/RELEASES.md"><code>https://github.com/actions/cache/blob/main/RELEASES.md</code></a>
with the new version and changes in the <code>## Changelog</code>
section.</li>
<li>Run <code>licensed cache</code> to update the license report.</li>
<li>Run <code>licensed status</code> and resolve any warnings by
updating the <a
href="https://github.com/actions/cache/blob/main/.licensed.yml"><code>https://github.com/actions/cache/blob/main/.licensed.yml</code></a>
file with the exceptions.</li>
<li>Commit your changes and push your branch upstream.</li>
<li>Open a pull request against <code>main</code> and get it reviewed
and merged.</li>
<li>Draft a new release <a
href="https://github.com/actions/cache/releases">https://github.com/actions/cache/releases</a>
use the same version number used in <code>package.json</code>
<ol>
<li>Create a new tag with the version number.</li>
<li>Auto generate release notes and update them to match the changes you
made in <code>RELEASES.md</code>.</li>
<li>Toggle the set as the latest release option.</li>
<li>Publish the release.</li>
</ol>
</li>
<li>Navigate to <a
href="https://github.com/actions/cache/actions/workflows/release-new-action-version.yml">https://github.com/actions/cache/actions/workflows/release-new-action-version.yml</a>
<ol>
<li>There should be a workflow run queued with the same version
number.</li>
<li>Approve the run to publish the new version and update the major tags
for this action.</li>
</ol>
</li>
</ol>
<h2>Changelog</h2>
<h3>6.1.0</h3>
<ul>
<li>Bump <code>@actions/cache</code> to v6.1.0 to pick up <a
href="https://redirect.github.com/actions/toolkit/pull/2435">actions/toolkit#2435
Handle cache write error due to read-only token</a></li>
<li>Switch redundant "Cache save failed" warning to debug log
in save-only</li>
</ul>
<h3>6.0.0</h3>
<ul>
<li>Updated <code>@actions/cache</code> to ^6.0.1,
<code>@actions/core</code> to ^3.0.1, <code>@actions/exec</code> to
^3.0.0, <code>@actions/io</code> to ^3.0.2</li>
<li>Migrated to ESM module system</li>
<li>Upgraded Jest to v30 and test infrastructure to be ESM
compatible</li>
</ul>
<h3>5.0.4</h3>
<ul>
<li>Bump <code>minimatch</code> to v3.1.5 (fixes ReDoS via globstar
patterns)</li>
<li>Bump <code>undici</code> to v6.24.1 (WebSocket decompression bomb
protection, header validation fixes)</li>
<li>Bump <code>fast-xml-parser</code> to v5.5.6</li>
</ul>
<h3>5.0.3</h3>
<ul>
<li>Bump <code>@actions/cache</code> to v5.0.5 (Resolves: <a
href="https://github.com/actions/cache/security/dependabot/33">https://github.com/actions/cache/security/dependabot/33</a>)</li>
<li>Bump <code>@actions/core</code> to v2.0.3</li>
</ul>
<h3>5.0.2</h3>
<!-- raw HTML omitted -->
</blockquote>
<p>... (truncated)</p>
</details>
<details>
<summary>Commits</summary>
<ul>
<li><a
href="55cc834586"><code>55cc834</code></a>
Merge pull request <a
href="https://redirect.github.com/actions/cache/issues/1768">#1768</a>
from jasongin/readonly-cache</li>
<li><a
href="d8cd72f230"><code>d8cd72f</code></a>
Bump <code>@actions/cache</code> to v6.1.0 - handle cache write error
due to RO token</li>
<li><a
href="2c8a9bd745"><code>2c8a9bd</code></a>
Merge pull request <a
href="https://redirect.github.com/actions/cache/issues/1760">#1760</a>
from actions/samirat/esm_migration_and_package_update</li>
<li><a
href="e9b91fdc3f"><code>e9b91fd</code></a>
Prettier fixes</li>
<li><a
href="e4884b8ff7"><code>e4884b8</code></a>
Rebuild dist</li>
<li><a
href="10baf0191a"><code>10baf01</code></a>
Fixed licenses</li>
<li><a
href="e39b386c90"><code>e39b386</code></a>
Fix test mock return order</li>
<li><a
href="b692820337"><code>b692820</code></a>
PR feedback</li>
<li><a
href="60749128a4"><code>6074912</code></a>
Rebuild dist bundles as ESM to match type:module</li>
<li><a
href="5a912e8b4a"><code>5a912e8</code></a>
Fix lint and jest issues</li>
<li>Additional commits viewable in <a
href="27d5ce7f10...55cc834586">compare
view</a></li>
</ul>
</details>
<br />
[](https://docs.github.com/en/github/managing-security-vulnerabilities/about-dependabot-security-updates#about-compatibility-scores)
Dependabot will resolve any conflicts with this PR as long as you don't
alter it yourself. You can also trigger a rebase manually by commenting
`@dependabot rebase`.
[//]: # (dependabot-automerge-start)
[//]: # (dependabot-automerge-end)
---
<details>
<summary>Dependabot commands and options</summary>
<br />
You can trigger Dependabot actions by commenting on this PR:
- `@dependabot rebase` will rebase this PR
- `@dependabot recreate` will recreate this PR, overwriting any edits
that have been made to it
- `@dependabot show <dependency name> ignore conditions` will show all
of the ignore conditions of the specified dependency
- `@dependabot ignore this major version` will close this PR and stop
Dependabot creating any more for this major version (unless you reopen
the PR or upgrade to it yourself)
- `@dependabot ignore this minor version` will close this PR and stop
Dependabot creating any more for this minor version (unless you reopen
the PR or upgrade to it yourself)
- `@dependabot ignore this dependency` will close this PR and stop
Dependabot creating any more for this dependency (unless you reopen the
PR or upgrade to it yourself)
</details>
Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
For every row with only one non-fixed variable in nla_core.cpp,
core::propagate, fix this variable.
---------
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nikolaj@cs.stanford.edu>
Fixes#10303.
## Symptom
On the reported QF_NRA instance z3 answers `sat` for some values of
`smt.random_seed` and `unsat` for others, and every `sat` comes with a
model z3's own validator rejects. The correct answer is `unsat`.
`smt.arith.solver=2` is unaffected; `smt.arith.solver=6` (the default)
is not.
## Root cause
The simplex model is not rational — each column is a `numeric_pair<mpq>`
`(x, y)` denoting `x + δ·y`, where `δ` is a positive infinitesimal used
to represent *strict* bounds exactly (`v > 0` is stored as `(0, 1)`).
`δ` only becomes concrete at model-output time, in
`from_model_in_impq_to_mpq(v) = v.x + m_delta * v.y`.
But nla decides monomial consistency using **only the rational parts**:
```cpp
const rational& val(lpvar j) const { return lra.get_column_value(j).x; } // nla_core.h:165
r *= lra.get_column_value(j).x; // product_value
return product_value(m) == lra.get_column_value(m.var()).x; // check_monic
```
That is sound only on a δ-free model, and it cannot be repaired by also
tracking `y`: a **product** `(x₁+δy₁)(x₂+δy₂)` has a `δ²` term, which a
`numeric_pair` cannot represent. The delta encoding is inherently
linear, so nla structurally cannot reason on a δ-carrying model.
The code relies on this: `core::check()` calls
`lra.get_rid_of_inf_eps()` as its very first action to instantiate δ
before any monomial is inspected. The invariant is:
> `m_to_refine` must only ever be computed on a δ-free model.
`core::optimize_nl_bounds()` breaks it. It calls
`lra.find_feasible_solution()` in the middle of the nla check; the
simplex re-runs, parks columns back onto strict bounds and
**re-introduces non-zero `y`**. It then calls `init_to_refine()` on that
model — one full LP re-solve after the scrub in `core::check()`.
A wrong `m_to_refine` turns directly into a wrong answer:
```
find_feasible_solution() re-introduces δ
→ init_to_refine() mis-measures monomials (compares only .x)
→ m_to_refine wrongly empty
→ horner.cpp:117 set_nla_satisfied()
→ core::check() returns l_true
→ theory_lra FC_DONE → sat
→ model output instantiates δ (x + m_delta·y)
→ monomial equations violated → "an invalid model was generated"
```
Instrumenting model construction on the reported benchmark confirms it
exactly: `use_nra_model=0`, **87 columns still carrying infinitesimals,
44 monomials violated** once δ is instantiated — every one of them with
`to_refine = 0`.
## Fix
Enforce the invariant where it is actually depended upon, instead of
only at the entry to `core::check()`:
```cpp
void core::init_to_refine() {
if (lra.is_feasible())
lra.get_rid_of_inf_eps();
m_to_refine.reset();
...
}
```
Every caller — including the ones inside `optimize_nl_bounds()` that
follow an LP re-solve — now measures monomials on a δ-free model.
A second commit closes a related hole: the
`arith.nl.optimize_bounds_lp_max_vars` throttle exit returns *after*
`find_feasible_solution()` has already moved the model, and was the only
exit that never called `init_to_refine()` at all — leaving `m_to_refine`
stale rather than merely δ-contaminated.
## Validation
Reported benchmark, `tactic.default_tactic=smt` (deterministic — the
default QF_NRA portfolio uses wall-clock `try_for` budgets, so it is
timing-dependent): master fails on **9 of 20** seeds; with the fix
**20/20** answer `unsat`. Under the default configuration, seeds 1–10
all answer `unsat` (was `sat` + invalid model on 1, 3, 4, 10), matching
`smt.arith.solver=2`.
The bug was much broader than the single reported instance. On the
`QF_NRA_small` corpus (1147 instances, `-T:10`):
| | sat | unsat | unknown | invalid model |
|---|---|---|---|---|
| master | 460 | 597 | 77 | **13** |
| this PR | 466 | 602 | 79 | **0** |
**Zero sat/unsat conflicts.** Of the 13 instances where master emitted
an invalid model, **7 are genuinely `unsat`** — the same unsoundness as
the reported one.
## Performance
Net **faster**, on the 1054 instances answered identically before and
after:
| | total |
|---|---|
| master | 229.7 s |
| this PR | 146.4 s (**−36.3 %**) |
133 instances faster by >200 ms vs. 13 slower by >200 ms.
The added `get_rid_of_inf_eps()` is asymptotically free —
`init_to_refine()` already costs Θ(Σ|monic|) arbitrary-precision
*multiplications*, so adding Θ(#columns) `mpq::is_zero()` tests (which
early-exit when no deltas are present) does not change its complexity
class. The expensive path is also moved rather than added: deltas left
by `optimize_nl_bounds()` previously survived until the next
`core::check()`, which paid the full `find_delta_for_strict_bounds` +
rewrite cost anyway.
The speedup itself comes from correctness — a truthful `m_to_refine`
points grobner / basic_lemma / order / monotonicity / tangent / nra at
the monomials that are genuinely violated, instead of letting them chase
a model that was never consistent.
`test-z3 /a`: 93/93 pass.
---------
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This is another PR towards the goal of getting Z3 to compile cleanly
when included via FetchContents into clang-tidy, which uses a pretty
strict set of warnings.
I realized that in https://github.com/Z3Prover/z3/pull/10192, I had
intended to add "-Wextra-semi" to CLANG_ONLY_WARNINGS. I certainly did
in testing, and the PR fixes all the remaining warnings it provokes, but
for some reason I left it out of the final PR. This adds it back; I
tested by doing both the dbg and release builds.
The tptp5 example was removed, so drop its build/run steps from ci.yml,
coverage.yml, and the daily-test-improver coverage action. The z3 -tptp
front-end and the tptp-benchmark workflow are unaffected.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9
Remove the seq_split (regex sigma-splitting / factorization) module and all
code that uses it:
- delete src/ast/rewriter/seq_split.{h,cpp} and src/test/seq_split.cpp
- drop the m_split member, include, and split/simplify_split/split_membership
wrappers from seq_rewriter
- remove the regex factorization propagation block from seq_regex.cpp
- remove the seq.regex_factorization_enabled/threshold parameters and their
theory_seq_params fields
- drop the files from the rewriter/test CMake lists and the test registry
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9
## Summary
Adds `seq_monadic` (`src/ast/rewriter/seq_monadic.{h,cpp}`), a
self-contained,
rewriter-level decision procedure for regex membership of a term that is
a
concatenation of sequence variables and constant elements — e.g. `x·a·x
∈ R`,
including repeated and multiple variables. It uses a whole-language
*monadic
decomposition* plus automaton product-reachability; it is minterm-free
and does
**not** use Nielsen word-equation splitting or `seq_split`.
The component is **purely additive**: it is not wired into any solver
path, so
default behavior is unchanged. It ships with a unit test and an opt-in
benchmark
harness that is inert unless `Z3_SEQ_BENCH_DIR` is set.
## What it does
- `x·u ∈ R ⇔ ⋁_q ( x reaches q in A_R ∧ u ∈ q )` over the derivative
automaton; `reach(q)` is never materialized as a regex (avoids the
state-elimination blowup). A variable's constraint is decided by a lazy
product-reachability search over tuples of derivative states, with
transitions
= the product of `brz_derivative_cofactors` branches and
pairwise-conjoined
`seq::range_predicate` guards.
- **Generic in the element sort**: characters use the exact
`range_predicate`
algebra; any other element sort uses a candidate-basis over the element
values
the guards mention (sound and complete for the
`{true,false,=,<=,and,or,not}`
guard grammar the derivatives emit).
- **Concrete witnesses**: on sat it reconstructs a witness value (a
sequence of
concrete elements, not predicates) per variable from the accepting
product path.
- **Boolean combinations**: `solve_and` decides a conjunction of
memberships
jointly, so a variable shared across memberships is constrained
consistently.
This is the natural extension since `¬(t∈R) ≡ t∈~R`, `∨` = union of
DNFs, and
`∧` = product of DNFs.
Also de-duplicates the char-guard → `range_predicate` translator into a
single
public `seq::guard_to_range_predicate` in `seq_range_collapse` (it was
previously
duplicated there and in `seq_monadic`).
## Testing
- `tst_seq_monadic`: single / multiple / repeated variables, nested
complement,
bounded loops, per-variable constraints, a generic `(Seq Int)` section,
witness
verification (substitute the model back and re-decide membership), and
`solve_and` cases that are individually sat but jointly unsat.
- Full unit suite `test-z3 /a` passes (93/93).
## Evaluation (offline harness, not part of CI)
On a regex-membership benchmark corpus, restricted to files carrying a
genuine
`(set-info :status)`, the solver decides 318 and 316 are correct
(99.4%); the
only 2 disagreements are a length limitation (`|x|=2k`) that is outside
the
membership fragment.
## Known limitations / follow-ups
- Pathological deeply-nested, high-multiplicity regexes can overflow the
recursive derivative stack; a recursion-depth guard to degrade to
`unknown` is
a natural follow-up.
- Out-of-fragment constraints (word equations, length / Parikh) are not
handled,
by design — this decides regex membership only.
---------
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nikolaj@cs.stanford.edu>
Copilot-Session: 916db256-43c6-4067-b6f4-fa8d2cf2f37f
## Summary
Fixes a Spacer regression where a satisfiable HORN benchmark that
previously returned `sat` now returns `unknown` with `(:reason-unknown
"Stuck on a lemma")`.
- **Originating discussion:**
https://github.com/Z3Prover/bench/discussions/3420
- **Benchmark:** `iss-5561/bug-2.smt2` (`inputs/issues/iss-5561/` in
`Z3Prover/bench`)
- **Kind:** `diff` (semantic answer changed)
### Divergence
```diff
--- bug-2.expected.out (expected)
+++ produced (current z3)
@@ -1,2 +1,2 @@
-sat
-(:reason-unknown "")
+unknown
+(:reason-unknown "Stuck on a lemma")
```
## Root cause
`git bisect` (clean per-commit builds, `-T:20`) identifies the first bad
commit as **df8d23960** — *"qe2: fix nonlinear term introduced by
term_graph representative selection in MBP (#10186)"* — which modified
`term_graph::term_lt` in `src/qe/mbp/mbp_term_graph.cpp`.
That change made concrete model **values** win over non-eliminated
uninterpreted **constants** when electing equivalence-class
representatives (previously the documented invariant was *"prefer
uninterpreted constants over values"*). It was intended to keep `qe2`'s
one-shot output linear (avoiding e.g. `(* 2 x)` becoming `(* x1 x)`).
Spacer, however, shares this same term_graph machinery for model-based
projection when generalizing lemmas. Preferring the value makes a
non-eliminated state constant get substituted by its concrete model
value everywhere in the projected lemma. This **over-grounds** the lemma
to the specific model, so Spacer keeps regenerating an over-specialized
lemma at infinity level; each regeneration bumps it until
`old_lemma->get_bumped() >= 100`, at which point `add_lemma_core` throws
`default_exception("Stuck on a lemma")`
(`src/muz/spacer/spacer_context.cpp`), surfacing as `unknown`.
`qe2`'s projection and Spacer's lemma generalization both funnel through
the same `spacer_qel`/`mbp_qel`/`qel` term_graph paths, so there is no
clean, separately-validatable client seam at which to gate the new
behavior without threading a new context flag through several layers.
## Fix
Revert the `term_lt` value-preference block, restoring the long-standing
invariant *"prefer uninterpreted constants over values"* that Spacer's
projection relies on. The change is confined to `term_lt` and adds an
explanatory comment referencing this regression.
## Validation
Built the patched `./z3` checkout (mk_make + `make`) and re-ran the
benchmark with the snapshot capture options (`-T:20`):
```
$ z3 -T:20 inputs/issues/iss-5561/bug-2.smt2
sat
(:reason-unknown "")
```
This matches the recorded `bug-2.expected.out` oracle exactly. The
sibling benchmark `iss-5561/bug-1.smt2` and basic solving were also
spot-checked and unaffected.
## Caveat for reviewers
This is a straight revert of the `term_lt` portion of #10186, so that
PR's cosmetic improvement — keeping `apply qe2` output in linear
`QF_LIA` form (avoiding logically-equivalent nonlinear terms) — is
reintroduced. #10186 added no regression test, so that behavior could
not be re-validated here. A non-regressing reimplementation should make
the representative preference **client-controlled** (as the `XXX`
comment above `term_lt` already suggests): enable value-preference only
for one-shot QE tactics (`qe2`) while keeping symbolic representatives
for Spacer's MBP generalization. Opened as a **draft** for human review.
> [!WARNING]
> <details>
> <summary>Firewall blocked 1 domain</summary>
>
> The following domain was blocked by the firewall during workflow
execution:
>
> - `pypi.org`
>> To allow these domains, add them to the `network.allowed` list in
your workflow frontmatter:
>
> ```yaml
> network:
> allowed:
> - defaults
> - "pypi.org"
> ```
>
> See [Network
Configuration](https://github.github.com/gh-aw/reference/network/) for
more information.
>
> </details>
> Generated by [Fix a Z3 snapshot-regression
divergence](https://github.com/Z3Prover/bench/actions/runs/30191159770)
· 572.3 AIC · ⌖ 20.4 AIC · ⊞ 10.7K ·
[◷](https://github.com/search?q=repo%3AZ3Prover%2Fz3+%22gh-aw-workflow-id%3A+snapshot-regression-fixer%22&type=pullrequests)
<!-- gh-aw-agentic-workflow: Fix a Z3 snapshot-regression divergence,
engine: copilot, version: 1.0.65, model: claude-opus-4.8, id:
30191159770, workflow_id: snapshot-regression-fixer, run:
https://github.com/Z3Prover/bench/actions/runs/30191159770 -->
<!-- gh-aw-workflow-id: snapshot-regression-fixer -->
<!-- gh-aw-workflow-call-id: Z3Prover/bench/snapshot-regression-fixer
-->
---------
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>
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
## Summary
Fixes a **completeness regression** in `qe_mbp` uncovered by the
snapshot-regression corpus.
- Originating discussion:
https://github.com/Z3Prover/bench/discussions/3445
- Benchmark ref: `iss-5925/small.smt2` (`Z3Prover/bench`,
`inputs/issues/iss-5925/`)
### Divergence
```diff
--- small.expected.out (expected)
+++ produced (current z3)
@@ -1 +1 @@
-unsat
+unknown
```
The benchmark is `(check-sat-using qe2)` over a formula that eliminates
an array variable `r` used **directly** as a store index: `(store (store
a v true) r true)`.
### Root cause
Commit 5bd9e6a00 ("Fix #7259, #7036: unsound MBP array projection with
array var in select/store index") added `has_array_var_in_index`, which
routes `spacer_qel` to the classic model-based projection
(`spacer_qe_lite`) whenever an eliminated array variable occurs anywhere
in a select/store index position. That guard is **too broad**: it also
fires when the array variable is used *directly* as an index (e.g. `r`
in `(store base r val)`). For `iss-5925/small.smt2` the fallback path
cannot decide the goal and returns `unknown` instead of the correct
`unsat`.
Using an array variable *directly* as an index is sound under `mbp_qel`:
the index is exactly that variable, and its model value is substituted
soundly. The genuine unsoundness of #7259/#7036 arises only when the
variable is **nested inside a compound index term** that the
partial-array-equality class-merge can silently rewrite (e.g. `(select
va (= v va))` becoming `(select v true)`).
### Fix
Restrict `has_array_var_in_index` to the dangerous nested case by
skipping index arguments that are *exactly* the array variable (`v !=
idx && occurs(v, idx)`). This keeps the #7259/#7036 soundness fallback
intact while restoring `qe2` completeness for direct-index benchmarks.
### Validation
Built z3 from this checkout (`make -j`, Release) and re-ran with
`-T:20`:
- `inputs/issues/iss-5925/small.smt2`: `unknown` (before) -> **`unsat`**
(after), matching the recorded oracle.
- `inputs/issues/iss-5925/delta.smt2`: still `unknown`, matching its
oracle.
- Reconstructed #7259 case `(select va (= v va))` under `qe2`: still
**`unsat`** (fallback still triggers for the nested-index case) -
soundness preserved.
- Unit tests `test-z3 mbp_qel` and `test-z3 qe_arith`: **PASS**.
Opened as a draft for human review. Please double-check the soundness
argument against the exact #7036 reproducer, which was not available in
the checkout.
> [!WARNING]
> <details>
> <summary>Firewall blocked 1 domain</summary>
>
> The following domain was blocked by the firewall during workflow
execution:
>
> - `pypi.org`
>> To allow these domains, add them to the `network.allowed` list in
your workflow frontmatter:
>
> ```yaml
> network:
> allowed:
> - defaults
> - "pypi.org"
> ```
>
> See [Network
Configuration](https://github.github.com/gh-aw/reference/network/) for
more information.
>
> </details>
> Generated by [Fix a Z3 snapshot-regression
divergence](https://github.com/Z3Prover/bench/actions/runs/30425630832)
· 287.3 AIC · ⌖ 20.1 AIC · ⊞ 10.7K ·
[◷](https://github.com/search?q=repo%3AZ3Prover%2Fz3+%22gh-aw-workflow-id%3A+snapshot-regression-fixer%22&type=pullrequests)
<!-- gh-aw-agentic-workflow: Fix a Z3 snapshot-regression divergence,
engine: copilot, version: 1.0.65, model: claude-opus-4.8, id:
30425630832, workflow_id: snapshot-regression-fixer, run:
https://github.com/Z3Prover/bench/actions/runs/30425630832 -->
<!-- gh-aw-workflow-id: snapshot-regression-fixer -->
<!-- gh-aw-workflow-call-id: Z3Prover/bench/snapshot-regression-fixer
-->
---------
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>
Co-authored-by: Nikolaj Bjorner <nikolaj@cs.stanford.edu>
The generated Python bindings loaded `libz3.so` without a soversion,
which could bind to an ABI-incompatible shared library when multiple Z3
versions are present. This change makes Linux bindings prefer the
versioned soname while leaving other platforms on the existing lookup
path.
- **Python loader generation**
- Thread a `z3py_soversion` parameter through `scripts/update_api.py`.
- Generate `_lib_name` as `libz3.so.<major>.<minor>` on Linux, and keep
`libz3.<ext>` elsewhere.
- Reuse `_lib_name` consistently for directory probing, system fallback,
and error messages.
- **Build-system wiring**
- Pass the current `SOVERSION` from the CMake Python bindings build on
Linux.
- Pass the same value through the `mk_make`/`mk_util.py` generation path
so both build systems emit the same loader behavior.
- **In-tree Python bindings layout**
- Add the matching `libz3.so.<major>.<minor>` link in `build/python/` on
Linux so the generated bindings work directly from the build tree.
- **Regression coverage**
- Add a focused script-level test for the generated loader preamble to
check:
- Linux uses the versioned soname when provided.
- Non-versioned fallback remains available when no soversion is
supplied.
Example of the generated Linux loader behavior:
```python
_sover = '5.0'
_ext = 'so'
_lib_name = 'libz3.%s.%s' % (_ext, _sover) if sys.platform.startswith('linux') and _sover else 'libz3.%s' % _ext
_lib = ctypes.CDLL(_lib_name)
```
<!-- START COPILOT CODING AGENT SUFFIX -->
- Fixes#7518
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nikolaj@cs.stanford.edu>
Remove the examples/tptp project and its references in the CMake examples
build, mk_project.py, and the CMake examples CI script.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9
`scanner::scan()` was returning `EOF_TOKEN` when the underlying stream
had `badbit` set, making a failed read (EIO, ENOSPC, etc.)
indistinguishable from a clean end-of-file. Z3 would silently produce no
output with exit code 0.
## Root cause
`std::istream::gcount()` returns 0 for both normal EOF and I/O failure.
`read_char()` returned -1 in both cases, and `scan()`'s `-1` handler
unconditionally set `EOF_TOKEN`.
## Fix
### `src/parsers/util/scanner.cpp`
Check `m_stream.bad()` in the `-1` case; emit an error message and
`ERROR_TOKEN` on failure:
```cpp
case static_cast<char>(-1):
if (m_stream.bad()) {
m_err << "ERROR: I/O failure while reading input stream.\n";
m_state = ERROR_TOKEN;
} else {
m_state = EOF_TOKEN;
}
break;
```
### `src/test/scanner_io.cpp` (new)
Regression test (ported from the `io_test` branch) verifying:
1. A good stream scans to completion (`n > 0` tokens).
2. A stream with `badbit` pre-set produces `ERROR_TOKEN` or a non-empty
error message rather than silent EOF.
### `src/test/main.cpp` + `src/test/CMakeLists.txt`
Register `tst_scanner_io` in the `FOR_EACH_ALL_TEST` macro and add
`scanner_io.cpp` to the build.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nikolaj@cs.stanford.edu>
Commit d46fbad3 added `__builtin_unreachable()` to the `UNREACHABLE()`
macro in Clang builds to suppress `-Wimplicit-fallthrough` warnings. In
Release+Clang mode, this causes UB: Clang can legally eliminate the
`invoke_exit_action` call (since reaching `__builtin_unreachable()` is
UB, the compiler assumes the entire branch is dead), so when
`UNREACHABLE()` is actually hit, the function continues with
uninitialized state — producing the segfault observed in the FPA C
example.
## Changes
- **`src/util/debug.h`** — Declare `invoke_exit_action` as
`[[noreturn]]`. This is semantically accurate: the function always
terminates via `exit()` or `throw`, never returning normally. The
`[[noreturn]]` annotation naturally suppresses `-Wimplicit-fallthrough`
after `UNREACHABLE()` without any UB.
- **`src/util/debug.h`** — Remove `__compiler_unreachable` macro and its
use in `UNREACHABLE()`. With `[[noreturn]]` on `invoke_exit_action`, it
is redundant.
- **`src/util/debug.cpp`** — Add `[[noreturn]]` to the
`invoke_exit_action` definition to match.
```cpp
// Before (broken in Release+Clang: UB allows optimizer to eliminate invoke_exit_action)
# define UNREACHABLE() { notify_assertion_violation(...); invoke_exit_action(ERR_UNREACHABLE); }; __builtin_unreachable()
// After (invoke_exit_action is [[noreturn]], no UB)
# define UNREACHABLE() { notify_assertion_violation(...); invoke_exit_action(ERR_UNREACHABLE); } ((void) 0)
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
This refines the recently added `has_array_var_in_index` helper in
`src/qe/qe_mbp.cpp` to match the surrounding style without changing
behavior. The array-index guard remains identical; the implementation is
just expressed more consistently.
- **What changed**
- Replaced the nested `for`/`if` occurrence check with the local
`any_of(...)` pattern already used nearby in `has_unsupported_th`.
- Added the missing blank line before `operator()` to align with spacing
used between other methods in the class.
- **Behavior**
- No functional change intended.
- The helper still returns `true` as soon as any array variable occurs
in a `select`/`store` index position.
- **Example**
```c++
for (unsigned i = 1; i < last; ++i)
if (any_of(arr_vars, [&](app* v) { return occurs(v, a->get_arg(i)); }))
return true;
```
<!-- START COPILOT CODING AGENT SUFFIX -->
- Fixes#10282
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
This is another PR towards the goal of getting Z3 to compile cleanly
when included via FetchContents into clang-tidy, which uses a pretty
strict set of warnings.
This PR enable the "-Wimplicit-fallthrough" warning, then fix all the
warnings this gets
in the clang build, by:
* Augmenting UNREACHABLE to add __builtin_unreachable(), which
suppresses
warnings for fallthrough in that cse.
* Adding Z3_fallthrough in many cases, to make it clear that
fallthroughs are intentional.
* Adding [[noreturn]] to functions that throw, so the compiler knows
they don't fall through to the next case.
* In a couple of cases, there's a fall-through to a default case, which
does "break", or "return nullptr". In those cases, I duplicated the
action in the preceding case, to make it more self-contained, and robust
in the face of change.
In some cases, I am concerned about whether the warnings are identifying
real bugs. For example, the fall-throughs in these files seem at least a
little suspect:
nnf.cpp
seq_rewriter.cpp
lar_solver.cpp
while very probably correct, also seem at least a tiny bit suspect.
However, this PR does *not* attempt to change any behavior, only to
silence the warnings. It would be great if somebody with more knowledge
of the code could vet these cases. If vetted, the explicit presence of
the Z3_fallthrough would reassure future readers of the code that the
fall-through is intentional, not accidental.
Expose enum_tuples(sorts) which produces an iterator over vectors of
terms, one term per input sort, dovetailing the per-sort streams so all
combinations are enumerated even when individual streams are infinite.
Each sort is enumerated by a self-contained sort_stream owning its own
grammar and bottom_up_enumerator seeded from the user productions, so
array sorts (with their fresh select ops and bound vars) do not collide
across sorts.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: cb1e958b-f89b-4407-958d-8e7ecf172bbc
The array term-graph projection (mbp_qel) treats an array equality (= a b)
as an implicit partial array equality and eliminates it by merging the
array variable's congruence class. That rewrite is unsound when the array
variable being eliminated occurs inside a select/store index position,
because the index is a first-class term whose value must be preserved.
For example, (select va (= v va)) was rewritten to (select v true) after
merging va into v, turning a model-false literal into a model-true one and
triggering the qe_mbp validation assertions (qe_mbp.cpp:412 for #7259,
qe_mbp.cpp:622 for #7036), or a crash at qsat.cpp:579 in release builds.
Detect when an array variable to be eliminated occurs inside a select or
store index and fall back to the classic model-based projection
(spacer_qe_lite) for such formulas. Both reproducers now return the correct
unsat verdict with no assertion failure, and all unit tests pass.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9
Build FStar only type-checks the compiler and ulib. Running `make test`
afterwards exercises the tests/examples suite, which sends many more SMT
queries to the freshly built Z3 and produces more logged failing queries
for the existing .smt2 collection step.
The new step runs in the FStar clone with the same opam env, PATH to the
Z3 aliases and OTHERFLAGS as the build. It is gated on a new
fstar_run_tests input (default true) and on the build succeeding, and is
continue-on-error so a test failure does not hide the build result or
skip reporting. The discussion summary reports the test outcome and the
tail of the test log; the SMT2 preview budget is reduced accordingly to
stay below the discussion body size limit.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Adds visibility for the `fstar-master-build.yml` GitHub Actions workflow
in `README.md` alongside existing build/status ribbons so its health is
visible from the repository landing page.
- **Scope**
- Updated the **Scheduled Workflows** badge table in `README.md` to
include the F\* master workflow.
- **README updates**
- Added a new column header: `F* Master Build`.
- Added the corresponding badge/link pair pointing to:
-
`https://github.com/Z3Prover/z3/actions/workflows/fstar-master-build.yml`
```md
| ... | Cross Build | F* Master Build |
| ... | [](.../cross-build.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/fstar-master-build.yml) |
```
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
