mirror of
https://github.com/Z3Prover/z3
synced 2026-07-27 01:12:40 +00:00
22550 commits
| Author | SHA1 | Message | Date | |
|---|---|---|---|---|
Copilot
|
18b4a86740
|
ci: add MinGW build/test job to Windows.yml (#10211)
MinGW silently ignores `#pragma comment(lib, ...)` (MSVC-only), so linker errors like missing `dbghelp` symbols go undetected until a downstream user hits them. No CI coverage existed for MinGW on Windows. ## Changes - **`.github/workflows/Windows.yml`**: New `mingw-build` job using MSYS2 UCRT64 (`mingw-w64-ucrt-x86_64-gcc`) that builds Z3 via `cmake -G Ninja` and runs `test-z3 /a`, exercising the full link step under MinGW on every push/PR to master. --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> |
||
z3prover-ci-bot[bot]
|
19781df2bc
|
[coz3-deepperf-fix] Avoid full-column rescan on each delta halving in lar_solver::init_model (#10217)
## Summary `lp::lar_solver::init_model()` (`src/math/lp/lar_solver.cpp`) picks an infinitesimal `delta` that maps every distinct rational-pair column value `(x, y)` to a *distinct* scalar `x + delta*y`, halving `delta` whenever a collision is detected. The previous implementation rebuilt **both** the set of distinct pairs and the set of scalars from a full O(n) pass over all columns on *every* halving, and the pair set is entirely independent of `delta`. ## Change - Build the delta-invariant set of distinct column pairs (`m_set_of_different_pairs`) **once**, before the halving loop. - On each halving, only rebuild the scalar set by iterating over the **distinct pairs** rather than rescanning all `n` columns (including duplicates). The collision test and the selected `delta` are unchanged: the loop still halves `delta` whenever the number of distinct scalars is less than the number of distinct pairs, and terminates when the scalar map is injective. The early-`break` versus end-of-pass check produce the same `delta` sequence because a size discrepancy on a full pass is exactly the injectivity-failure condition. ## Cost argument Let `n` = column count and `D` = number of *distinct* column pairs (`D ≤ n`), and `H` = number of halvings. - Before: `O(H · n · log D)` — every halving re-inserts all `n` columns into both sets. - After: `O(n · log D + H · D · log D)` — the pair set is built once; each halving touches only the `D` distinct pairs. This removes the repeated full rescan from the halving loop and skips redundant work for duplicate columns, turning a per-halving O(n) rebuild into a one-time cost plus O(D) per halving. ## Evidence Profiled under callgrind (deterministic instruction counts), differential correctness preserved, static-analysis hygiene clean: - Target function self-instructions: **2,695,433,533 → 2,084,074,808** (−22.7%). - Total program instructions ratio: **0.904** (−9.6%). - Wall-time speedup: **~6.1%**. - Differential correctness: identical results (no mismatches). Logic class exercised: **QF_LRA / linear real arithmetic** model construction. <!-- gh-aw-workflow-id: coz3-deepperf-fix --> <!-- gh-aw-workflow-call-id: Z3Prover/bench/coz3-deepperf-fix --> --------- 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> |
||
|
Copilot
|
c15ef957eb
|
Fix NameError: EXECUTABLE_FILE_FALLBACKS undefined on win32/darwin in setup.py (#10219)
`EXECUTABLE_FILE_FALLBACKS` was referenced on all platforms in
`_copy_bins()` but only defined in the `emscripten` and `else` (Linux)
branches — causing a `NameError` crash on Windows and macOS wheel
builds.
## Change
Add `EXECUTABLE_FILE_FALLBACKS = []` to the missing platform branches in
`src/api/python/setup.py`:
```python
if BUILD_PLATFORM in ('sequoia','darwin', 'osx'):
LIBRARY_FILE = "libz3.dylib"
EXECUTABLE_FILE = "z3"
EXECUTABLE_FILE_FALLBACKS = [] # added
elif BUILD_PLATFORM in ('win32', 'cygwin', 'win'):
LIBRARY_FILE = "libz3.dll"
EXECUTABLE_FILE = "z3.exe"
EXECUTABLE_FILE_FALLBACKS = [] # added
elif BUILD_PLATFORM in ('emscripten',):
...
EXECUTABLE_FILE_FALLBACKS = ["z3.js.wasm", "z3"]
else:
...
EXECUTABLE_FILE_FALLBACKS = []
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nikolaj@cs.stanford.edu>
|
||
|
Copilot
|
74b616c2f3
|
Stabilize max_reg in Ubuntu MT debug CI by normalizing nonlinear term construction (#10212)
The `Ubuntu build - python make - MT` job was failing in unit test
`max_reg` under debug configuration due to a shape-sensitive internal
NLA assertion. This PR updates the test’s nonlinear expressions to an
equivalent construction that avoids the failing path.
- **Root issue in CI path**
- `test_max_reg` built BNH objective/constraints with subtraction forms
that triggered a debug-only monic-check assertion in NLA internals.
- **Targeted test-only normalization**
- In `src/test/api.cpp` (`test_max_reg`), rewrote squared-difference
terms to constant-first subtraction forms (mathematically equivalent).
- Updated:
- `f2` construction
- circle/offset constraints in `mk_max_reg()`
- **No solver behavior change**
- This is a unit-test expression-shape change only; production solver
code is untouched.
```cpp
// before
Z3_ast f2 = mk_add(mk_sq(mk_sub(x1, mk_real(5))), mk_sq(mk_sub(x2, mk_real(5))));
Z3_optimize_assert(ctx, opt, Z3_mk_le(ctx,
mk_add(mk_sq(mk_sub(x1, mk_real(5))), mk_sq(x2)), mk_real(25)));
// after
Z3_ast f2 = mk_add(mk_sq(mk_sub(mk_real(5), x2)), mk_sq(mk_sub(mk_real(5), x1)));
Z3_optimize_assert(ctx, opt, Z3_mk_le(ctx,
mk_add(mk_sq(mk_sub(mk_real(5), x1)), mk_sq(x2)), mk_real(25)));
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
|
||
Nikolaj Bjorner
|
d60d6a0665 | add incremental propagate for nla to retain some propagation lemmas | ||
dependabot[bot]
|
7055366050
|
Bump actions/checkout from 7.0.0 to 7.0.1 (#10208)
Bumps [actions/checkout](https://github.com/actions/checkout) from 7.0.0 to 7.0.1. <details> <summary>Release notes</summary> <p><em>Sourced from <a href="https://github.com/actions/checkout/releases">actions/checkout's releases</a>.</em></p> <blockquote> <h2>v7.0.1</h2> <h2>What's Changed</h2> <ul> <li>skip running unsafe pr check if input is default by <a href="https://github.com/aiqiaoy"><code>@aiqiaoy</code></a> in <a href="https://redirect.github.com/actions/checkout/pull/2518">actions/checkout#2518</a></li> <li>trim only ascii whitespace for branch by <a href="https://github.com/aiqiaoy"><code>@aiqiaoy</code></a> in <a href="https://redirect.github.com/actions/checkout/pull/2521">actions/checkout#2521</a></li> <li>escape values passed to --unset by <a href="https://github.com/aiqiaoy"><code>@aiqiaoy</code></a> in <a href="https://redirect.github.com/actions/checkout/pull/2530">actions/checkout#2530</a></li> <li>Various dependency updates</li> </ul> <p><strong>Full Changelog</strong>: <a href="https://github.com/actions/checkout/compare/v7...v7.0.1">https://github.com/actions/checkout/compare/v7...v7.0.1</a></p> </blockquote> </details> <details> <summary>Commits</summary> <ul> <li>See full diff in <a href="https://github.com/actions/checkout/compare/v7...v7.0.1">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> |
||
|
dependabot[bot]
|
4611ea3f19
|
Bump actions/setup-python from 6 to 7 (#10209)
Bumps [actions/setup-python](https://github.com/actions/setup-python) from 6 to 7. <details> <summary>Release notes</summary> <p><em>Sourced from <a href="https://github.com/actions/setup-python/releases">actions/setup-python's releases</a>.</em></p> <blockquote> <h2>v7.0.0</h2> <h2>What's Changed</h2> <h3>Enhancements</h3> <ul> <li>Migrate to ESM and upgrade dependencies by <a href="https://github.com/priyagupta108"><code>@priyagupta108</code></a> in <a href="https://redirect.github.com/actions/setup-python/pull/1330">actions/setup-python#1330</a></li> <li>Pin SHA commits and update docs with latest versions by <a href="https://github.com/HarithaVattikuti"><code>@HarithaVattikuti</code></a> in <a href="https://redirect.github.com/actions/setup-python/pull/1338">actions/setup-python#1338</a></li> <li>Remove the pip-install input by <a href="https://github.com/gowridurgad"><code>@gowridurgad</code></a> in <a href="https://redirect.github.com/actions/setup-python/pull/1336">actions/setup-python#1336</a></li> </ul> <h3>Bug Fix</h3> <ul> <li>Fix to Classify stderr warning messages as warnings instead of errors in annotations by <a href="https://github.com/lmvysakh"><code>@lmvysakh</code></a> in <a href="https://redirect.github.com/actions/setup-python/pull/1335">actions/setup-python#1335</a></li> <li>Validate and retry manifest fetch to prevent silent failures by <a href="https://github.com/priyagupta108"><code>@priyagupta108</code></a> in <a href="https://redirect.github.com/actions/setup-python/pull/1332">actions/setup-python#1332</a></li> </ul> <h3>Dependency Upgrade</h3> <ul> <li>Bump certifi from 2020.6.20 to 2024.7.4 in /<strong>tests</strong>/data by <a href="https://github.com/dependabot"><code>@dependabot</code></a> in <a href="https://redirect.github.com/actions/setup-python/pull/1328">actions/setup-python#1328</a></li> <li>Remove EOL Python versions and Bumps numpy text fixture by <a href="https://github.com/priya-kinthali"><code>@priya-kinthali</code></a> in <a href="https://redirect.github.com/actions/setup-python/pull/1333">actions/setup-python#1333</a></li> <li>Upgrade <code>@actions/cache</code> to 6.2.0 by <a href="https://github.com/philip-gai"><code>@philip-gai</code></a> in <a href="https://redirect.github.com/actions/setup-python/pull/1337">actions/setup-python#1337</a></li> </ul> <h2>New Contributors</h2> <ul> <li><a href="https://github.com/lmvysakh"><code>@lmvysakh</code></a> made their first contribution in <a href="https://redirect.github.com/actions/setup-python/pull/1335">actions/setup-python#1335</a></li> <li><a href="https://github.com/philip-gai"><code>@philip-gai</code></a> made their first contribution in <a href="https://redirect.github.com/actions/setup-python/pull/1337">actions/setup-python#1337</a></li> </ul> <p><strong>Full Changelog</strong>: <a href="https://github.com/actions/setup-python/compare/v6...v7.0.0">https://github.com/actions/setup-python/compare/v6...v7.0.0</a></p> <h2>v6.3.0</h2> <h2>What's Changed</h2> <h3>Enhancement</h3> <ul> <li>Add RHEL support and include Linux distro in cache keys by <a href="https://github.com/priyagupta108"><code>@priyagupta108</code></a> in <a href="https://redirect.github.com/actions/setup-python/pull/1323">actions/setup-python#1323</a></li> <li>Fix pip cache error handling on Windows by <a href="https://github.com/priyagupta108"><code>@priyagupta108</code></a> in <a href="https://redirect.github.com/actions/setup-python/pull/1040">actions/setup-python#1040</a></li> </ul> <h3>Dependency update</h3> <ul> <li>Upgrade minimatch from 3.1.2 to 3.1.5 by <a href="https://github.com/dependabot"><code>@dependabot</code></a> in <a href="https://redirect.github.com/actions/setup-python/pull/1281">actions/setup-python#1281</a></li> <li>Upgrade actions dependencies by <a href="https://github.com/gowridurgad"><code>@gowridurgad</code></a> with <a href="https://github.com/Copilot"><code>@Copilot</code></a> in <a href="https://redirect.github.com/actions/setup-python/pull/1303">actions/setup-python#1303</a></li> <li>Upgrade <code>@actions/cache</code> to 5.1.0, log cache write denied by <a href="https://github.com/jasongin"><code>@jasongin</code></a> in <a href="https://redirect.github.com/actions/setup-python/pull/1324">actions/setup-python#1324</a></li> <li>Upgrade dependency versions and test workflow configuration by <a href="https://github.com/HarithaVattikuti"><code>@HarithaVattikuti</code></a> in <a href="https://redirect.github.com/actions/setup-python/pull/1322">actions/setup-python#1322</a></li> </ul> <h3>Documentation</h3> <ul> <li>Update advanced-usage.md by <a href="https://github.com/Dunky-Z"><code>@Dunky-Z</code></a> in <a href="https://redirect.github.com/actions/setup-python/pull/811">actions/setup-python#811</a></li> </ul> <h2>New Contributors</h2> <ul> <li><a href="https://github.com/gowridurgad"><code>@gowridurgad</code></a> with <a href="https://github.com/Copilot"><code>@Copilot</code></a> made their first contribution in <a href="https://redirect.github.com/actions/setup-python/pull/1303">actions/setup-python#1303</a></li> <li><a href="https://github.com/jasongin"><code>@jasongin</code></a> made their first contribution in <a href="https://redirect.github.com/actions/setup-python/pull/1324">actions/setup-python#1324</a></li> <li><a href="https://github.com/Dunky-Z"><code>@Dunky-Z</code></a> made their first contribution in <a href="https://redirect.github.com/actions/setup-python/pull/811">actions/setup-python#811</a></li> </ul> <p><strong>Full Changelog</strong>: <a href="https://github.com/actions/setup-python/compare/v6.2.0...v6.3.0">https://github.com/actions/setup-python/compare/v6.2.0...v6.3.0</a></p> <h2>v6.2.0</h2> <h2>What's Changed</h2> <h3>Dependency Upgrades</h3> <ul> <li>Upgrade dependencies to Node 24 compatible versions by <a href="https://github.com/salmanmkc"><code>@salmanmkc</code></a> in <a href="https://redirect.github.com/actions/setup-python/pull/1259">actions/setup-python#1259</a></li> </ul> <!-- raw HTML omitted --> </blockquote> <p>... (truncated)</p> </details> <details> <summary>Commits</summary> <ul> <li><a href=" |
||
|
Nikolaj Bjorner
|
e3cc338fc9 |
nla: restore eager propagate_nla during theory_lra propagation
PR #10180 moved nonlinear bound propagation to final_check only, removing the eager propagate_nla() from the search-time propagation path. This left E-matching without nla-implied bound facts during search, causing an instantiation blowup on number-theory goals (e.g. FStar.Math.Euclid), which exhausted rlimit and returned unknown on queries previously proved. Re-run propagate_nla() before propagate_bounds_with_lp_solver() in the l_true case of propagate_core so tightened nonlinear bounds are surfaced to the SMT core during search. Recovers FStar.Math.Euclid-1/-2. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 96a14756-2ffe-4cc3-87e7-49fda1b6113a |
||
Nikolaj Bjorner
|
e268a72eb9
|
Update fstar-master-build.yml | ||
|
Copilot
|
a3c7dc9433
|
fix: smtlib2_compliant mode turns unsat to unknown due to Int/Real sort mismatch in coeffs2app (#10204)
With `(set-option :smtlib2_compliant true)`, Z3 disables implicit Int→Real coercions. When the LP solver generates Gomory cuts/bounds over expressions that mix Int and Real LP variables (as happens when `to_real(n)` is internalized — both `to_real(n)` as Real and `n` as Int are registered as LP vars), `coeffs2app` was constructing `mk_mul(Real_numeral, Int_expr)`. Without implicit coercions, `check_args` throws an `ast_exception` that bubbles up through `cmd_context::check_sat()` as `l_undef`, producing a spurious `unknown` instead of `unsat`. ## Changes - **`src/smt/theory_lra.cpp` — `coeffs2app`**: Before building each product term, coerce `o` to Real via `a.mk_to_real(o)` when `!is_int && a.is_int(o)`. This makes the sort explicit rather than relying on implicit coercions. - **`src/test/smt2print_parse.cpp`**: Regression test for the exact formula from the issue — verifies the result is `unsat` (not `unknown`) when `smtlib2_compliant` is set. ```smt2 (set-option :smtlib2_compliant true) (set-logic ALL) (declare-datatype SBVRational ((SBV.Rational (sbv.rat.numerator Int) (sbv.rat.denominator Int)))) ; ... mixed Int/Real via to_real ... (check-sat) ; was: unknown (:reason-unknown "Sort mismatch at argument #2 for function * (Real Real) Real supplied sort is Int") ; now: unsat ``` <!-- START COPILOT CODING AGENT SUFFIX --> - Fixes #10166 --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> |
||
|
Nikolaj Bjorner
|
caeaaa7d07 |
qe2: eliminate fresh undeclared constant leak (#10172)
spacer_qel could report a bound variable as eliminated (removing it from vars) while do_qel/qel_project simplifications still left an occurrence of it in the formula. The variable then surfaced in the qe2 result as a fresh, undeclared constant (e.g. X!0), so asserting the result failed with "unknown constant". After qel_project, scan the formula for any originally-to-eliminate variable that was dropped from vars yet still occurs in fml, and route it through other_vars so the existing model-based projection/substitution replaces it with its model value. The result is logically equivalent and mentions only declared symbols. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 96a14756-2ffe-4cc3-87e7-49fda1b6113a |
||
|
Nikolaj Bjorner
|
48f1676f2b |
Fix drain_backtrack to pop trail scopes and compile
The drain_backtrack destructor added in
|
||
|
Copilot
|
44c221b690
|
Fix MinGW linker errors: explicitly link dbghelp on Windows (#10203)
Building Z3 on Windows with MinGW (`mingw-w64-ucrt-x86_64-gcc`) fails with undefined references to `SymSetOptions`, `SymInitialize`, `SymFromAddr`, and `SymGetLineFromAddr64` from the DbgHelp library used in `src/util/debug.cpp` for stack backtraces. The existing `#pragma comment(lib, "dbghelp.lib")` in `debug.cpp` is an MSVC-only extension — MinGW silently ignores it, so `dbghelp` is never passed to the linker. ## Changes - **`CMakeLists.txt`**: Append `dbghelp` to `Z3_DEPENDENT_LIBS` in the `WIN32` platform block. This feeds the library to both the `libz3` and `shell` link steps regardless of compiler. - **`src/util/debug.cpp`**: Guard the `#pragma comment` with `#ifdef _MSC_VER` to make the MSVC-only intent explicit. <!-- START COPILOT CODING AGENT SUFFIX --> - Fixes #10171 --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> |
||
|
Nikolaj Bjorner
|
d247df72a2 |
drain backtrack trail using scoped guarantees
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> |
||
|
Nikolaj Bjorner
|
c9d3dc959d |
Fix trail-scope leak in ho_matcher on early exit (#10196)
The higher-order matcher shares the solver's trail stack. On early-exit paths (resource/rlimit reached via m.inc(), or search budget exhausted) work items were left on m_backtrack with their pushed scopes never popped, leaking a trail scope. This desynchronized the trail scope count from the solver scope level and later tripped SASSERT(ilvl <= m_scope_lvl) / unsound backtracking in smt::context::reinit_clauses. Restore the trail before exit on every path using an RAII guard (scoped_trail_level) and drain the backtrack stack after the main search loop so m_backtrack is left empty for the next call. This avoids wrapping large blocks in try/catch (which would mask underlying bugs such as creating non-well-sorted expressions) while still guaranteeing the trail is restored on both normal and exceptional exits. The sort-mismatch check and UNREACHABLE() in refine_ho_match are preserved so ill-sorted terms remain surfaced rather than silently discarded. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 96a14756-2ffe-4cc3-87e7-49fda1b6113a |
||
|
Nikolaj Bjorner
|
e0f978f7cd | omit adding rows for affine relations if it is true in the current model | ||
|
Nikolaj Bjorner
|
1d83ecb9de |
Move SMTLIB2 verdict unit tests to z3test regressions
These tests fed a fixed SMTLIB2 string to Z3_eval_smtlib2_string and checked a sat/unsat verdict. They are now data-driven regression files under z3test regressions/smt2 (with .expected.out ground truth), so remove them from the C++ test suite: - fpa.cpp: removed entirely (all tests transferred) - seq_rewriter.cpp: removed the two seq.foldl model-validation tests - simplifier.cpp: removed the sat.smt QF_UFBV predicate model-validation test - mod_factor.cpp: removed the const-array store-chain unsat test The API-constructed mod/idiv internalization-order tests remain in mod_factor.cpp. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 96a14756-2ffe-4cc3-87e7-49fda1b6113a |
||
l46kok
|
8a9beaf882
|
Fix ASAN memory leak by removing unused m_fixed_val in undo_fixed_column (#10199)
Remove unused m_fixed_val member variable from undo_fixed_column. undo_fixed_column is allocated in a region/trail allocator where C++ destructors are not invoked when objects are popped/reclaimed. Storing an mpq instance (which can allocate heap memory for multi-precision numbers) inside a region-allocated object causes a memory leak that is flagged by ASAN. m_fixed_val was never used in undo() or elsewhere in the struct. Removing it completely eliminates the ASAN finding, avoids unnecessary mpq copies, and is entirely safe. |
||
|
Nikolaj Bjorner
|
aba41d026f
|
nla: add LP-based nonlinear bound optimization for cross-nested confl… (#10180)
…icts Add core::optimize_nl_bounds() (gated by arith.nl.optimize_bounds) which runs LP max/min over monomial leaf variables inside core::propagate(), analogous to solver=2's max_min_nl_vars, so nla (arith.solver=6) can detect cross-nested conflicts previously missed. Collect improved bounds first, then apply them and re-establish feasibility once; reconcile the core solver via find_feasible_solution before the raw maximize solves to preserve inf_heap_is_correct(). Skip null witnesses in get_dependencies_of_maximum for implied/unconditional bounds. On FStar-UInt128-divergence solver=6 this yields unsat in 2 final-checks, seed-insensitive (seeds 1-10). Copilot-Session: ac36bb84-de91-4e6c-86df-6008c7396ceb --------- Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: ac36bb84-de91-4e6c-86df-6008c7396ceb Copilot-Session: 96a14756-2ffe-4cc3-87e7-49fda1b6113a |
||
1sgtpepper
|
53fa8f9cc4
|
Fix unsigned BV-to-FP exponent narrowing (#10189)
## Summary Include the equal-width case in symbolic unsigned BV-to-FP exponent saturation, preventing positive exponents from being interpreted as negative by the rounder. Adds regression coverage for overflow and in-range values. Fixes #7135. ## Testing - `./build-review/test-z3 fpa` - `./build-review/test-z3 /a` (92 passed) - Symbolic-versus-numeral differential matrix (50 cases across five width boundaries and all rounding modes) - Exact-head fork `CI` and `OCaml Binding CI` workflows (passed) |
||
|
Copilot
|
df8d23960e
|
qe2: fix nonlinear term introduced by term_graph representative selection in MBP (#10186)
`qe2` could produce a nonlinear term (e.g. `(* x x1)`) when eliminating quantifiers from a purely linear LIA formula. The result was logically equivalent but broke downstream consumers expecting QF_LIA output. **Root cause** In `term_graph::term_lt`, numeric values were unconditionally ranked *lower* than uninterpreted constants when selecting equivalence class representatives. During model-based projection, ITE processing adds the model literal `(= x1 2)` to the term graph, merging `x1` and `2` into one equivalence class with `x1` elected as representative. Any expression containing the coefficient `2` — e.g. `(* 2 x)` from `x + x` — then gets rewritten as `(* x1 x)`, a nonlinear product of two free variables. **Fix** (`src/qe/mbp/mbp_term_graph.cpp` — `term_lt`) When both terms are 0-argument and differ in value-ness, prefer the *value* as class representative **unless** the non-value is a variable slated for elimination (where `refine_repr_class` will later replace it with a value anyway). This prevents free variables from displacing numeric coefficients. ```smt2 ; Before fix (apply qe2) ; => (or (not (= x1 2)) (not (= (+ y (* (- 1) x x1)) 0)) (not (= y 0))) ; ^^^^^^^^^^^ nonlinear ; After fix ; => (or (not (= x1 2)) (not (= x 0)) (not (= y 0))) ; fully linear ``` --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: Nikolaj Bjorner <nikolaj@cs.stanford.edu> |
||
davedets
|
35b0b42d2e
|
Use macros to disable semi-colon warnings for blocks of macros. (#10192)
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 completes the job started by https://github.com/Z3Prover/z3/pull/10169. It adds `-Wextra-semi` to the set of CLANG_ONLY_WARNINGS, and adds ``` START_DISABLE_EXTRA_SEMI_WARNING; ...macro invocations with trailing semis... END_DISABLE_WARNING; ``` around all the blocks of macro invocations that provoked warnings. (Additionally, in realclosure.h, there was one block of macro invocations that did *not* follow the trailing-semi pattern; changed that to look like all the others). |
||
|
dependabot[bot]
|
f8f763bdf1
|
Bump shell-quote from 1.8.4 to 1.10.0 in /src/api/js (#10193)
Bumps [shell-quote](https://github.com/ljharb/shell-quote) from 1.8.4 to 1.10.0. <details> <summary>Changelog</summary> <p><em>Sourced from <a href="https://github.com/ljharb/shell-quote/blob/main/CHANGELOG.md">shell-quote's changelog</a>.</em></p> <blockquote> <h2><a href="https://github.com/ljharb/shell-quote/compare/v1.9.0...v1.10.0">v1.10.0</a> - 2026-07-10</h2> <h3>Merged</h3> <ul> <li>[New] <code>parse</code>: add opt-in <code>splitUnquoted</code> option for shell field-splitting of unquoted expansions <a href="https://redirect.github.com/ljharb/shell-quote/pull/1"><code>[#1](https://github.com/ljharb/shell-quote/issues/1)</code></a></li> </ul> <h3>Commits</h3> <ul> <li>[Fix] <code>parse</code>: match nested <code>${...}</code> braces so nested parameter expansion is consumed as one substitution <a href=" |
||
|
dependabot[bot]
|
5055183037
|
Bump linkify-it from 5.0.1 to 5.0.2 in /src/api/js (#10194)
Bumps [linkify-it](https://github.com/markdown-it/linkify-it) from 5.0.1 to 5.0.2. <details> <summary>Changelog</summary> <p><em>Sourced from <a href="https://github.com/markdown-it/linkify-it/blob/master/CHANGELOG.md">linkify-it's changelog</a>.</em></p> <blockquote> <h2>5.0.2 / 2026-07-02</h2> <ul> <li>Fixed DoS in <code>mailto:</code> links (restrict user name to 64 chars).</li> <li>Restricted user/pass part length in links.</li> </ul> </blockquote> </details> <details> <summary>Commits</summary> <ul> <li><a href=" |
||
Daniel Tang
|
d91bb5b5fa
|
Fix some lost Solver.solutions(t) (#10195)
z3-rs correctly used Or. I accidentally forgot that enclosing function
call, and had what resulted in And.
Test case:
```python
s = Solver()
x, y, z = Ints("x y z")
s.add(x >= 0, x <= 2, y >= 0, y <= 2, z >= 0, z <= 2, x + y + z == 2)
# I didn't test multivariable constraints last time fearing nondeterminism
# Sorting avoids that
print(sorted(map(lambda x: list(map(lambda x: x.as_long(), x)), s.solutions([x, y, z]))))
```
**Before**: `[[0, 1, 1], [2, 0, 0]]`
**After**: `[[0, 0, 2], [0, 1, 1], [0, 2, 0], [1, 0, 1], [1, 1, 0], [2,
0, 0]]`
Fixes: #8633
---------
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
||
|
Copilot
|
0f2bc0c36b
|
Removing nuget-build workflow and updating README (#10191)
Pull request created by AI Agent Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> |
||
|
Copilot
|
847ee63b2d
|
Fix invalid model from int_to_bv missing modular reduction in bv2int_translator (#10185)
With `smt.bv.solver=2`, `int_to_bv(x)` was translated to the raw integer
`x` without normalizing it to `[0, 2^N)`. Bitwise operations like
`bvxor(A, B)` are translated as `A + B - 2·band(A, B)`, which is only
valid when both operands are in `[0, 2^N)`. When `x` was negative or ≥
2^N, the LP solver could assign a band value inconsistent with bit
semantics, producing a model that fails validation.
## Changes
- **`OP_INT2BV` translation** (`translate_bv`): Apply `umod(e, 0)`
instead of passing the raw integer argument through. This normalizes the
value to `[0, 2^N)` before it participates in any bitwise arithmetic.
```cpp
// Before
case OP_INT2BV:
r = arg(0); // raw integer, may be negative or ≥ 2^N
// After
case OP_INT2BV:
r = umod(e, 0); // normalized to [0, 2^N)
```
- **`amod` shortcut**: Add a fast-path for `mod(t, N)` when the divisor
already equals `N` — the result is already in `[0, N)`, so wrapping it
again with another `mod(_, N)` is unnecessary and avoids expression
bloat.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
|
||
|
Copilot
|
9ac438b199
|
Fix nested symbolic re.range under re.++ ignoring solver timeout (#10181)
Symbolic `re.range` nested under `re.++` caused Z3 to loop indefinitely,
ignoring timeouts. Direct symbolic range membership was fixed
previously, but the nested case reaches a different code path — the
Brzozowski derivative engine in `derive_range`.
## Root cause
`derive_range` in `seq_derive.cpp` only handled concrete unit-string
bounds. For symbolic bounds it returned a stuck `re.derivative(ele,
re.range(lo, hi))` term. When nested under concatenation, this stuck
term cycled infinitely:
1. `is_nullable` of the stuck term → `is_nullable_symbolic_regex` →
emits `re.in_re("", re.derivative(...))`
2. That `in_re` triggers `propagate_in_re` → new `accept` predicate
3. New `accept` computes another derivative → another stuck term →
repeat
## Fix
Replace the stuck fallback with a proper symbolic ITE. By SMT-LIB
semantics, `re.range(lo, hi)` accepts character `c` iff both bounds are
single-character strings and `lo[0] ≤ c ≤ hi[0]`. The derivative with
respect to `ele` becomes:
```
ite(len(lo)=1 ∧ len(hi)=1 ∧ lo[0] ≤ ele ∧ ele ≤ hi[0], ε, ∅)
```
Length conditions are omitted for bounds already known to be concrete
single-character strings.
```smt2
(set-logic ALL)
(declare-const s String)
(assert (str.in_re "a" (re.++ re.all (re.range s "c"))))
(check-sat)
; Previously hung indefinitely; now returns sat in ~10ms
```
## Changes
- **`src/ast/rewriter/seq_derive.cpp`** — `derive_range`: replace stuck
`re.derivative` fallback with symbolic ITE using `str.nth_i` and length
guards for non-concrete bounds
- **`src/test/seq_rewriter.cpp`** — add solver-level regression test
(case 21) for nested symbolic `re.range` under `re.++`
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
|
||
|
davedets
|
e2df18faaf
|
Test PR for disabling semicolon warnings (#10169)
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. https://github.com/Z3Prover/z3/pull/10020 deleted a number of unnecessary (and, by a strict interpretation, illegal) semicolons. These were detected by adding -Wextra-semi to CLANG_ONLY_WARNINGS during testing. The PR did not eliminate all such unnecessary/illegal semi-colons; Nikolaj Bjorner argued that some IDEs would be confused by doing so for macro invocations, which otherwise look like function calls. So it left those, and did not include adding -Wextra-semi to CLANG_ONLY_WARNINGS in the PR. I'm worried that not having -Wextra-semi will allow instances of the semis we'd like to eliminate to creep back in. This PR introduces a mechanism to disable the warnings for regions with such macro invocations, and uses that mechanism for one file. If accepted, a subsequent PR would use this mechanism in all the remaining places, so that there is a clean clang build with -Wextra-semi. I verified that: * It compiles cleanly for if the enable/disable macros have null definitions, as they would for non-clang compilations. * It compiles cleanly for a clang build without -Wextra-semis. * It compiles successfully, albeit with *many* warnings, for a clang build with-Wextra-semis -- but none of those errors are for the regions in ast.h where the warning is disabled. |
||
|
Copilot
|
ae190b8b88
|
fix: parallel mode exits unknown immediately for QF_BV due to reason-string mismatch (#10183)
Under `parallel.enable=true`, QF_BV workers that exhaust their per-cube
conflict budget (1000) are misclassified as unrecoverably incomplete,
causing the portfolio to return `unknown` in ~1 second instead of
escalating the budget and continuing.
## Root cause
`parallel_tactical.cpp` only recognizes `"max-conflicts-reached"` (the
`smt::context` spelling) as a signal to escalate the conflict budget.
SAT-core-backed solvers — which QF_BV workers use — report the same
condition as `"sat.max.conflicts"` (from
`sat_solver::reached_max_conflicts()`). The mismatch causes every QF_BV
cube attempt to fall through to `b.set_unknown()` instead of
`update_max_thread_conflicts()`.
## Fix
```diff
- if (reason != "max-conflicts-reached") {
+ if (reason != "max-conflicts-reached" && reason != "sat.max.conflicts") {
```
Both spellings now correctly route to the budget-escalation path. The
parallel `smt_parallel.cpp` path is unaffected — it owns `smt::context`
workers, which can only produce `"max-conflicts-reached"`.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
|
||
|
Copilot
|
35f6b0869a
|
parallel solver: suppress bare reason_unknown on stderr at default verbosity (#10182)
`IF_VERBOSE(0, ...)` in the parallel tactic's `l_undef` handler caused the raw reason string (e.g. `sat.max.conflicts`) to be written unconditionally to stderr, polluting output for any application embedding libz3 that hits the conflict-budget give-up path. ## Change - **`src/solver/parallel_tactical.cpp:2186`** — raise verbosity threshold from `0` to `1`: ```cpp // Before: fires at default verbosity, writes bare string to stderr IF_VERBOSE(0, verbose_stream() << reason << "\n"); // After: only fires under -v:1 IF_VERBOSE(1, verbose_stream() << reason << "\n"); ``` The reason string remains fully accessible via `(get-info :reason-unknown)` and `set_reason_unknown` regardless of verbosity. --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> |
||
|
1sgtpepper
|
479ff3476e
|
Fix polymorphic application arity validation (#10179)
## Summary Validate a polymorphic declaration's arity before matching argument sorts. This prevents `Z3_mk_app` from reading past the declaration domain and makes both too-few and too-many arguments return `Z3_INVALID_ARG`. Adds C API regression coverage for valid, too-few, and too-many applications. Fixes #10177. ## Testing - `./build-release/test-z3 api` - `./build-release/test-z3 /a` (92 passed) - Standalone #10177 reproducer against the patched shared library |
||
Michael Tautschnig
|
0105b220fd
|
Make string_hash independent of char signedness (#10163)
`string_hash`'s tail-byte handling reads bytes through plain `char`, whose signedness is implementation-defined. On signed-char platforms (x86_64 Linux, macOS) bytes ≥ `0x80` are sign-extended before entering the hash state (e.g. `c+=((unsigned)data[10]<<24);` becomes `c += 0xFF80xxxx` instead of `c += 0x0080xxxx`); on unsigned-char platforms (Linux aarch64) they are not. Hashes of byte strings containing such bytes therefore differ across platforms. This is not just cosmetic: `mpz_manager::hash` feeds the digit arrays of large numerals through `string_hash`, so AST hashes of bit-vector constants like `(_ bv36028797018963968 64)` (= 2^55, whose digit bytes include `0x80`) differ between architectures. AST hashes determine hash table layouts throughout the solver, so preprocessing and search take platform-dependent paths for byte-identical input. Observed impact (Z3 4.15.3 release binaries as well as local gcc-13 builds, identical `.smt2` input generated by CBMC from the [mldsa-native](https://github.com/pq-code-package/mldsa-native) verification suite — quantifiers + arrays + bit-vectors, ~120k lines): | instance | x86_64 | aarch64 | |---|---|---| | instance A | 643 s | 11.7 s | | instance B | 22.8 s | 1578 s | Tracing AST construction on both hosts showed the first divergence at the registration of the numeral `2^55`, whose node hash was `2587296535` on x86_64 vs `808470355` on aarch64, with identical mpz digit arrays; from that point on, hash table iteration orders (and consequently `ctx-simplify` steps, quantifier instantiation order, and case-split order) diverge. With this patch, instance A solves in ~21 s on x86_64 (down from 643 s), matching the aarch64 behaviour class. The fix casts the tail bytes to `unsigned char`, matching the 4-byte-chunk path (which is already signedness-independent via `memcpy` into `unsigned`). Note that hash values on signed-char platforms change for inputs containing bytes ≥ `0x80` (pure-ASCII symbol names are unaffected). (Found while investigating cross-platform proof-time instability reported in diffblue/cbmc#8991.) Co-authored-by: Kiro <kiro-agent@users.noreply.github.com> |
||
|
Michael Tautschnig
|
09aaadf963
|
Sequence AST-creating arguments in rewriters for cross-compiler determinism (#10165)
### Problem
The order of evaluation of function arguments is unspecified in C++
(arguments are indeterminately sequenced since C++17). Compilers use
this freedom differently:
```c++
static int f(int i) { printf("%d ", i); return i; }
static void g(int, int, int) { printf("\n"); }
int main() { g(f(1), f(2), f(3)); }
```
| compiler/target | output |
|---|---|
| gcc 13, x86_64 | `3 2 1` |
| gcc 13, aarch64 | `1 2 3` |
| clang 18, x86_64 | `1 2 3` |
Z3 has many call sites where **two or more arguments each create AST
nodes**, e.g. (before this PR, `bv_rewriter.cpp:876`):
```c++
result = m.mk_ite(c, m_mk_extract(high, low, t), m_mk_extract(high, low, e));
```
The two extract nodes are hash-consed and receive their AST ids in
evaluation order, so the id assignment differs between
compilers/targets. AST ids feed heuristic tie-breaking throughout the
solver (`bool_rewriter`'s `m_order_eq` equality-operand ordering,
id-based sorts in `array_rewriter`, case-split ordering, ...), so
**byte-identical input takes different solver paths depending on the
compiler and architecture z3 was built with**.
### Evidence
Investigated while chasing cross-platform proof-time instability in
CBMC/mldsa-native CI (diffblue/cbmc#8991), on byte-identical ~12 MB SMT2
instances (bit-vectors + arrays + quantifiers), with the `string_hash`
fix from #10163 applied to isolate this effect. Z3 4.15.3, gcc 13 on
x86_64 Linux and aarch64 Linux (Graviton):
* one instance: **17 s on x86_64 vs 1633 s on aarch64** (both `unsat`; a
sibling instance shows the reverse direction). Run-to-run within one
host: ±1 %.
* Instrumenting `ast_manager::register_node_core` with an order
fingerprint (running hash over `(node hash, node id)`) shows both
architectures construct **identical AST sequences up to registration
#41,789**, where x86_64 creates `(extract[0:0] #xFFFFFFFF)` before
`(extract[0:0] #xFFFFFFFE)` and aarch64 the other way around — from
identical call stacks at the `mk_ite`-over-two-`mk_extract` site quoted
above. All divergence between the two hosts flows from such events
(pointer/ASLR effects experimentally excluded: fingerprints are
invariant under `setarch -R` and across repeated runs).
* Sequencing that one site by hand moved the first divergence to
#248,118 — the analogous `mk_ite(c, mk_select(...), mk_select(...))`
site in `array_rewriter.cpp`. Sequencing that one, too, moved it to
#248,411, inside `nnf:👿:process_iff_xor` — i.e. the next layer of
the same onion.
* With the whole `ast/rewriter` layer swept (this PR), the instrumented
builds produce **identical AST construction traces on both architectures
throughout the entire rewriter phase** of this 546k-line industrial
instance; the first divergence left is the NNF one.
### Fix
Following the precedent of
|
||
|
z3prover-ci-bot[bot]
|
7f7f8ae59b
|
[snapshot-regression-fix] fpa: fp.to_bv of large-exponent values should be unspecified, not unknown (#10174)
## Summary
Fixes a completeness regression where a **satisfiable** floating-point
problem is answered `unknown`.
- **Originating discussion:**
https://github.com/Z3Prover/bench/discussions/3232
- **Benchmark:** `iss-3199/bug-1.smt2` (from
https://github.com/Z3Prover/z3/issues/3199)
### Divergence
```diff
--- bug-1.expected.out (expected)
+++ produced (current z3)
@@ -1 +1 @@
-sat
+unknown
```
The benchmark:
```smt2
(declare-fun x () (_ FloatingPoint 40 60))
(declare-fun y () (_ BitVec 8))
(assert (= ((_ fp.to_ubv 8) RTP x) y #x00))
(check-sat)
```
`(get-info :reason-unknown)` reports `"exponents over 31 bits are not
supported"`.
### Root cause
The problem is clearly `sat` (e.g. `x = 0.0`, `y = #x00`; and for any
out-of-range `x`, `fp.to_ubv` is unspecified so `= #x00` is
satisfiable). z3 bit-blasts and finds a model that assigns `x` a value
with a very large binary exponent (the `FloatingPoint 40 60` sort has a
40-bit exponent field). During model reconstruction,
`fpa_util::is_considered_uninterpreted` performs a range check by
calling `mpf_manager::to_sbv_mpq`, which **throws** `"exponents over 31
bits are not supported"` when the unpacked exponent does not fit into an
`int` (guard added in `
|
||
|
Nikolaj Bjorner
|
c9a4a5907d |
tptp: set weight 1 on parsed quantifiers
Route all forall/exists creation in the TPTP frontend through a with_weight1() helper so quantifiers use weight 1 instead of the default 0. Improves smt.ho_matching on higher-order TPTP problems (+26 net solved, fewer timeouts over the ^ benchmark set). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 96a14756-2ffe-4cc3-87e7-49fda1b6113a |
||
|
Copilot
|
1f306e1e29
|
Fix Pyodide wheel packaging for emscripten executable name variants (#10158)
`build-pyodide` failed because Python packaging assumed the wasm shell
artifact is always emitted as `build/z3.wasm`. In the failing run, the
expected file was absent, causing wheel build to abort during binary
copy.
- **Root cause handling in `setup.py`**
- In the emscripten path, add executable fallbacks (`z3.js.wasm`, `z3`)
alongside the canonical `z3.wasm`.
- During packaging, probe known output names in order and copy the first
match.
- **Stable wheel layout**
- Keep packaged artifact name stable as `bin/z3.wasm` regardless of
which build output variant exists.
- **Failure diagnostics**
- If no candidate exists, raise a `FileNotFoundError` listing all
attempted paths to make CI failures immediately actionable.
```python
executable_names = (EXECUTABLE_FILE,) + tuple(EXECUTABLE_FILE_FALLBACKS)
for executable_name in executable_names:
candidate = os.path.join(BUILD_DIR, executable_name)
if os.path.exists(candidate):
shutil.copy(candidate, os.path.join(BINS_DIR, EXECUTABLE_FILE))
break
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
|
||
|
Nikolaj Bjorner
|
225cf6dd9b
|
Revert "Allow OTP input for WebAssembly npm publish workflow" (#10157)
Reverts Z3Prover/z3#10156 |
||
|
Copilot
|
5a03a73685
|
Allow OTP input for WebAssembly npm publish workflow (#10156)
The `WebAssembly Publish` Actions job failed at `npm publish` with
`EOTP` because the workflow had no path to supply npm one-time passwords
for OTP-protected accounts. This change adds secure OTP input wiring for
manual publish runs while preserving the existing token-based flow.
- **Workflow dispatch input**
- Added optional `workflow_dispatch` input `npm_otp` in
`.github/workflows/wasm-release.yml`.
- **Secure OTP handling**
- Added a dedicated masking step so provided OTP values are redacted in
logs.
- Routed OTP to npm via `NPM_CONFIG_OTP` in the publish step
environment.
- **Publish step behavior**
- Kept publish command as `npm publish`; npm now consumes OTP
automatically when provided through env.
```yaml
on:
workflow_dispatch:
inputs:
npm_otp:
description: "One-time password for npm publish (optional)"
required: false
type: string
# ...
- name: Mask npm OTP
if: ${{ github.event.inputs.npm_otp != '' }}
run: echo "::add-mask::${{ github.event.inputs.npm_otp }}"
- name: Publish
run: npm publish
env:
NODE_AUTH_TOKEN: ${{ secrets.NPM_TOKEN }}
NPM_CONFIG_OTP: ${{ github.event.inputs.npm_otp }}
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
|
||
|
Copilot
|
0d7376c733
|
Fix WebAssembly Publish job by using the release environment (#10155)
The `WebAssembly Publish` workflow was failing in the `Publish` step
after a successful build/test pass. The failure was isolated to npm
publication, indicating the job was not running with the intended
release-scoped publish configuration.
- **Workflow wiring**
- Attach the `publish` job in `.github/workflows/wasm-release.yml` to
the existing `release` environment.
- Align the wasm npm publish path with the repository’s other release
publishing jobs that already rely on environment-scoped release
configuration.
- **Effect**
- Ensures the final `npm publish` step executes in the same release
context as other artifact publication jobs.
- Avoids publishing with default job context when release-specific
configuration is required.
```yaml
jobs:
publish:
name: Publish
runs-on: ubuntu-latest
environment: release
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
|
||
|
Copilot
|
8e3402b215
|
wasm: pin Node.js to v22 instead of lts/* to avoid manifest fetch failures (#10151)
`actions/setup-node` with `node-version: "lts/*"` requires fetching a version manifest from GitHub's servers to resolve the alias. This manifest request was returning a GitHub 500 error, causing the `Check` job to fail at setup. ## Changes - **`wasm.yml`, `wasm-release.yml`**: Replace `node-version: "lts/*"` with `node-version: "22"` (current Active LTS), eliminating the remote manifest lookup entirely. --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> |
||
|
Nikolaj Bjorner
|
d722fb1708 |
update release notes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> |
||
|
Nikolaj Bjorner
|
7ba8861784 |
update version
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> |
||
|
dependabot[bot]
|
3751bfa8c4
|
Bump actions/cache/save from 5.0.5 to 6.1.0 (#10149)
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=" |
||
|
dependabot[bot]
|
b39692a643
|
Bump actions/setup-dotnet from 5 to 6 (#10147)
Bumps [actions/setup-dotnet](https://github.com/actions/setup-dotnet) from 5 to 6. <details> <summary>Release notes</summary> <p><em>Sourced from <a href="https://github.com/actions/setup-dotnet/releases">actions/setup-dotnet's releases</a>.</em></p> <blockquote> <h2>v6.0.0</h2> <h2>What's Changed</h2> <ul> <li>Migrate to ESM and upgrade dependencies by <a href="https://github.com/priyagupta108"><code>@priyagupta108</code></a> in <a href="https://redirect.github.com/actions/setup-dotnet/pull/752">actions/setup-dotnet#752</a></li> <li>Bump actions/checkout from 6.0.3 to 7.0.0 by <a href="https://github.com/dependabot"><code>@dependabot</code></a>[bot] in <a href="https://redirect.github.com/actions/setup-dotnet/pull/751">actions/setup-dotnet#751</a></li> <li>chore(deps): bump <code>@actions/cache</code> to 6.2.0 by <a href="https://github.com/philip-gai"><code>@philip-gai</code></a> in <a href="https://redirect.github.com/actions/setup-dotnet/pull/756">actions/setup-dotnet#756</a></li> </ul> <h2>New Contributors</h2> <ul> <li><a href="https://github.com/philip-gai"><code>@philip-gai</code></a> made their first contribution in <a href="https://redirect.github.com/actions/setup-dotnet/pull/756">actions/setup-dotnet#756</a></li> </ul> <p><strong>Full Changelog</strong>: <a href="https://github.com/actions/setup-dotnet/compare/v5...v6.0.0">https://github.com/actions/setup-dotnet/compare/v5...v6.0.0</a></p> <h2>v5.4.0</h2> <h2>What's Changed</h2> <h3>Enhancements</h3> <ul> <li>Improve global.json SDK version validation for rollForward by <a href="https://github.com/priyagupta108"><code>@priyagupta108</code></a> in <a href="https://redirect.github.com/actions/setup-dotnet/pull/742">actions/setup-dotnet#742</a></li> <li>Pin actions to commit SHAs in workflows by <a href="https://github.com/priya-kinthali"><code>@priya-kinthali</code></a> in <a href="https://redirect.github.com/actions/setup-dotnet/pull/744">actions/setup-dotnet#744</a></li> <li>Expand the CSC problem matcher to light up more errors on GitHub. by <a href="https://github.com/StephenCleary"><code>@StephenCleary</code></a> in <a href="https://redirect.github.com/actions/setup-dotnet/pull/717">actions/setup-dotnet#717</a></li> </ul> <h3>Documentation</h3> <ul> <li>Docs(action): Explicitly mark all optional inputs with required: false by <a href="https://github.com/kranthipoturaju"><code>@kranthipoturaju</code></a> in <a href="https://redirect.github.com/actions/setup-dotnet/pull/737">actions/setup-dotnet#737</a></li> </ul> <h3>Bug Fixes</h3> <ul> <li>Fix global.json creation command by <a href="https://github.com/michal2612"><code>@michal2612</code></a> in <a href="https://redirect.github.com/actions/setup-dotnet/pull/694">actions/setup-dotnet#694</a></li> </ul> <h3>Dependency Updates</h3> <ul> <li>Upgrade <code>@actions/cache</code> to 5.1.0, log cache write denied by <a href="https://github.com/jasongin"><code>@jasongin</code></a> in <a href="https://redirect.github.com/actions/setup-dotnet/pull/746">actions/setup-dotnet#746</a></li> </ul> <h2>New Contributors</h2> <ul> <li><a href="https://github.com/jasongin"><code>@jasongin</code></a> made their first contribution in <a href="https://redirect.github.com/actions/setup-dotnet/pull/746">actions/setup-dotnet#746</a></li> <li><a href="https://github.com/michal2612"><code>@michal2612</code></a> made their first contribution in <a href="https://redirect.github.com/actions/setup-dotnet/pull/694">actions/setup-dotnet#694</a></li> <li><a href="https://github.com/kranthipoturaju"><code>@kranthipoturaju</code></a> made their first contribution in <a href="https://redirect.github.com/actions/setup-dotnet/pull/737">actions/setup-dotnet#737</a></li> <li><a href="https://github.com/StephenCleary"><code>@StephenCleary</code></a> made their first contribution in <a href="https://redirect.github.com/actions/setup-dotnet/pull/717">actions/setup-dotnet#717</a></li> </ul> <p><strong>Full Changelog</strong>: <a href="https://github.com/actions/setup-dotnet/compare/v5...v5.4.0">https://github.com/actions/setup-dotnet/compare/v5...v5.4.0</a></p> <h2>v5.3.0</h2> <h2>What's Changed</h2> <h3>Enhancements</h3> <ul> <li>Add dotnet-version: latest support with dotnet-channel input by <a href="https://github.com/mahabaleshwars"><code>@mahabaleshwars</code></a> in <a href="https://redirect.github.com/actions/setup-dotnet/pull/730">actions/setup-dotnet#730</a></li> <li>Support global.json's rollForward latest* variants by <a href="https://github.com/js6pak"><code>@js6pak</code></a> in <a href="https://redirect.github.com/actions/setup-dotnet/pull/538">actions/setup-dotnet#538</a></li> <li>Improve version resolution by <a href="https://github.com/akoeplinger"><code>@akoeplinger</code></a> in <a href="https://redirect.github.com/actions/setup-dotnet/pull/560">actions/setup-dotnet#560</a></li> </ul> <h3>Dependency Updates</h3> <!-- raw HTML omitted --> </blockquote> <p>... (truncated)</p> </details> <details> <summary>Commits</summary> <ul> <li><a href=" |
||
|
dependabot[bot]
|
0739cd2347
|
Bump actions/checkout from 6.0.2 to 7.0.0 (#10146)
Bumps [actions/checkout](https://github.com/actions/checkout) from 6.0.2 to 7.0.0. <details> <summary>Release notes</summary> <p><em>Sourced from <a href="https://github.com/actions/checkout/releases">actions/checkout's releases</a>.</em></p> <blockquote> <h2>v7.0.0</h2> <h2>What's Changed</h2> <ul> <li>block checking out fork pr for pull_request_target and workflow_run by <a href="https://github.com/aiqiaoy"><code>@aiqiaoy</code></a> in <a href="https://redirect.github.com/actions/checkout/pull/2454">actions/checkout#2454</a></li> <li>Bump actions/publish-immutable-action from 0.0.3 to 0.0.4 in the minor-actions-dependencies group across 1 directory by <a href="https://github.com/dependabot"><code>@dependabot</code></a>[bot] in <a href="https://redirect.github.com/actions/checkout/pull/2458">actions/checkout#2458</a></li> <li>Bump flatted from 3.3.1 to 3.4.2 by <a href="https://github.com/dependabot"><code>@dependabot</code></a>[bot] in <a href="https://redirect.github.com/actions/checkout/pull/2460">actions/checkout#2460</a></li> <li>Bump js-yaml from 4.1.0 to 4.2.0 by <a href="https://github.com/dependabot"><code>@dependabot</code></a>[bot] in <a href="https://redirect.github.com/actions/checkout/pull/2461">actions/checkout#2461</a></li> <li>Bump <code>@actions/core</code> and <code>@actions/tool-cache</code> and Remove uuid by <a href="https://github.com/dependabot"><code>@dependabot</code></a>[bot] in <a href="https://redirect.github.com/actions/checkout/pull/2459">actions/checkout#2459</a></li> <li>upgrade module to esm and update dependencies by <a href="https://github.com/aiqiaoy"><code>@aiqiaoy</code></a> in <a href="https://redirect.github.com/actions/checkout/pull/2463">actions/checkout#2463</a></li> <li>Bump the minor-npm-dependencies group across 1 directory with 3 updates by <a href="https://github.com/dependabot"><code>@dependabot</code></a>[bot] in <a href="https://redirect.github.com/actions/checkout/pull/2462">actions/checkout#2462</a></li> <li>getting ready for checkout v7 release by <a href="https://github.com/aiqiaoy"><code>@aiqiaoy</code></a> in <a href="https://redirect.github.com/actions/checkout/pull/2464">actions/checkout#2464</a></li> <li>update error wording by <a href="https://github.com/aiqiaoy"><code>@aiqiaoy</code></a> in <a href="https://redirect.github.com/actions/checkout/pull/2467">actions/checkout#2467</a></li> </ul> <h2>New Contributors</h2> <ul> <li><a href="https://github.com/aiqiaoy"><code>@aiqiaoy</code></a> made their first contribution in <a href="https://redirect.github.com/actions/checkout/pull/2454">actions/checkout#2454</a></li> </ul> <p><strong>Full Changelog</strong>: <a href="https://github.com/actions/checkout/compare/v6.0.3...v7.0.0">https://github.com/actions/checkout/compare/v6.0.3...v7.0.0</a></p> <h2>v6.0.3</h2> <h2>What's Changed</h2> <ul> <li>Update changelog by <a href="https://github.com/ericsciple"><code>@ericsciple</code></a> in <a href="https://redirect.github.com/actions/checkout/pull/2357">actions/checkout#2357</a></li> <li>fix: expand merge commit SHA regex and add SHA-256 test cases by <a href="https://github.com/yaananth"><code>@yaananth</code></a> in <a href="https://redirect.github.com/actions/checkout/pull/2414">actions/checkout#2414</a></li> <li>Fix checkout init for SHA-256 repositories by <a href="https://github.com/yaananth"><code>@yaananth</code></a> in <a href="https://redirect.github.com/actions/checkout/pull/2439">actions/checkout#2439</a></li> <li>Update changelog for v6.0.3 by <a href="https://github.com/yaananth"><code>@yaananth</code></a> in <a href="https://redirect.github.com/actions/checkout/pull/2446">actions/checkout#2446</a></li> </ul> <h2>New Contributors</h2> <ul> <li><a href="https://github.com/yaananth"><code>@yaananth</code></a> made their first contribution in <a href="https://redirect.github.com/actions/checkout/pull/2414">actions/checkout#2414</a></li> </ul> <p><strong>Full Changelog</strong>: <a href="https://github.com/actions/checkout/compare/v6...v6.0.3">https://github.com/actions/checkout/compare/v6...v6.0.3</a></p> </blockquote> </details> <details> <summary>Commits</summary> <ul> <li><a href=" |
||
|
dependabot[bot]
|
bb9dc5e5a4
|
Bump actions/setup-node from 6 to 7 (#10148)
Bumps [actions/setup-node](https://github.com/actions/setup-node) from 6 to 7. <details> <summary>Release notes</summary> <p><em>Sourced from <a href="https://github.com/actions/setup-node/releases">actions/setup-node's releases</a>.</em></p> <blockquote> <h2>v7.0.0</h2> <h2>What's Changed</h2> <h3>Enhancements:</h3> <ul> <li>Add cache-primary-key and cache-matched-key as outputs by <a href="https://github.com/gowridurgad"><code>@gowridurgad</code></a> in <a href="https://redirect.github.com/actions/setup-node/pull/1577">actions/setup-node#1577</a></li> <li>Migrate to ESM and upgrade dependencies by <a href="https://github.com/gowridurgad"><code>@gowridurgad</code></a> in <a href="https://redirect.github.com/actions/setup-node/pull/1574">actions/setup-node#1574</a></li> </ul> <h3>Bug fixes:</h3> <ul> <li>Remove dummy NODE_AUTH_TOKEN export by <a href="https://github.com/gowridurgad"><code>@gowridurgad</code></a> in <a href="https://redirect.github.com/actions/setup-node/pull/1558">actions/setup-node#1558</a></li> <li>Only use <code>mirrorToken</code> in <code>getManifest</code> if it's provided by <a href="https://github.com/deiga"><code>@deiga</code></a> in <a href="https://redirect.github.com/actions/setup-node/pull/1548">actions/setup-node#1548</a></li> </ul> <h3>Documentation updates:</h3> <ul> <li>Add documentation for publishing to npm with Trusted Publisher (OIDC) by <a href="https://github.com/chiranjib-swain"><code>@chiranjib-swain</code></a> in <a href="https://redirect.github.com/actions/setup-node/pull/1536">actions/setup-node#1536</a></li> <li>docs: Update restore-only cache documentation by <a href="https://github.com/priya-kinthali"><code>@priya-kinthali</code></a> in <a href="https://redirect.github.com/actions/setup-node/pull/1550">actions/setup-node#1550</a></li> <li>docs: Update caching recommendations to mitigate cache poisoning risks by <a href="https://github.com/chiranjib-swain"><code>@chiranjib-swain</code></a> in <a href="https://redirect.github.com/actions/setup-node/pull/1567">actions/setup-node#1567</a></li> </ul> <h3>Dependency update:</h3> <ul> <li>Upgrade <code>@actions/cache</code> to 5.1.0, log cache write denied by <a href="https://github.com/jasongin"><code>@jasongin</code></a> in <a href="https://redirect.github.com/actions/setup-node/pull/1569">actions/setup-node#1569</a></li> </ul> <h2>New Contributors</h2> <ul> <li><a href="https://github.com/chiranjib-swain"><code>@chiranjib-swain</code></a> made their first contribution in <a href="https://redirect.github.com/actions/setup-node/pull/1536">actions/setup-node#1536</a></li> <li><a href="https://github.com/deiga"><code>@deiga</code></a> made their first contribution in <a href="https://redirect.github.com/actions/setup-node/pull/1548">actions/setup-node#1548</a></li> <li><a href="https://github.com/jasongin"><code>@jasongin</code></a> made their first contribution in <a href="https://redirect.github.com/actions/setup-node/pull/1569">actions/setup-node#1569</a></li> </ul> <p><strong>Full Changelog</strong>: <a href="https://github.com/actions/setup-node/compare/v6...v7.0.0">https://github.com/actions/setup-node/compare/v6...v7.0.0</a></p> <h2>v6.5.0</h2> <h2>What's Changed</h2> <ul> <li>Update <code>@actions/cache</code> to 5.1.0 and add security overrides for undici and fast-xml-parser by <a href="https://github.com/HarithaVattikuti"><code>@HarithaVattikuti</code></a> in <a href="https://redirect.github.com/actions/setup-node/pull/1579">actions/setup-node#1579</a></li> </ul> <p><strong>Full Changelog</strong>: <a href="https://github.com/actions/setup-node/compare/v6.4.0...v6.5.0">https://github.com/actions/setup-node/compare/v6.4.0...v6.5.0</a></p> <h2>v6.4.0</h2> <h2>What's Changed</h2> <h3>Dependency updates:</h3> <ul> <li>Upgrade <a href="https://github.com/actions"><code>@actions</code></a> dependencies by <a href="https://github.com/Copilot"><code>@Copilot</code></a> in <a href="https://redirect.github.com/actions/setup-node/pull/1525">actions/setup-node#1525</a></li> <li>Update Node.js versions in versions.yml and bump package to v6.4.0 by <a href="https://github.com/priya-kinthali"><code>@priya-kinthali</code></a> in <a href="https://redirect.github.com/actions/setup-node/pull/1533">actions/setup-node#1533</a></li> </ul> <h2>New Contributors</h2> <ul> <li><a href="https://github.com/Copilot"><code>@Copilot</code></a> made their first contribution in <a href="https://redirect.github.com/actions/setup-node/pull/1525">actions/setup-node#1525</a></li> </ul> <p><strong>Full Changelog</strong>: <a href="https://github.com/actions/setup-node/compare/v6...v6.4.0">https://github.com/actions/setup-node/compare/v6...v6.4.0</a></p> <h2>v6.3.0</h2> <h2>What's Changed</h2> <h3>Enhancements:</h3> <ul> <li>Support parsing <code>devEngines</code> field by <a href="https://github.com/susnux"><code>@susnux</code></a> in <a href="https://redirect.github.com/actions/setup-node/pull/1283">actions/setup-node#1283</a></li> </ul> <!-- raw HTML omitted --> </blockquote> <p>... (truncated)</p> </details> <details> <summary>Commits</summary> <ul> <li><a href=" |
||
|
dependabot[bot]
|
7e29ea76d6
|
Bump actions/setup-go from 6 to 7 (#10150)
Bumps [actions/setup-go](https://github.com/actions/setup-go) from 6 to 7. <details> <summary>Release notes</summary> <p><em>Sourced from <a href="https://github.com/actions/setup-go/releases">actions/setup-go's releases</a>.</em></p> <blockquote> <h2>v7.0.0</h2> <h2>What's Changed</h2> <ul> <li>Migrate to ESM and upgrade dependencies by <a href="https://github.com/priyagupta108"><code>@priyagupta108</code></a> in <a href="https://redirect.github.com/actions/setup-go/pull/763">actions/setup-go#763</a></li> <li>chore(deps): bump <code>@actions/cache</code> to 6.2.0 by <a href="https://github.com/philip-gai"><code>@philip-gai</code></a> in <a href="https://redirect.github.com/actions/setup-go/pull/771">actions/setup-go#771</a></li> </ul> <h2>New Contributors</h2> <ul> <li><a href="https://github.com/philip-gai"><code>@philip-gai</code></a> made their first contribution in <a href="https://redirect.github.com/actions/setup-go/pull/771">actions/setup-go#771</a></li> </ul> <p><strong>Full Changelog</strong>: <a href="https://github.com/actions/setup-go/compare/v6...v7.0.0">https://github.com/actions/setup-go/compare/v6...v7.0.0</a></p> <h2>v6.5.0</h2> <h2>What's Changed</h2> <h3>Dependency update</h3> <ul> <li>Upgrade actions dependencies by <a href="https://github.com/priyagupta108"><code>@priyagupta108</code></a> with <a href="https://github.com/Copilot"><code>@Copilot</code></a> in <a href="https://redirect.github.com/actions/setup-go/pull/744">actions/setup-go#744</a></li> <li>Upgrade <code>@types/node</code> and typescript-eslint dependencies to resolve npm audit findings by <a href="https://github.com/HarithaVattikuti"><code>@HarithaVattikuti</code></a> in <a href="https://redirect.github.com/actions/setup-go/pull/755">actions/setup-go#755</a></li> <li>Upgrade <code>@actions/cache</code> to 5.1.0, log cache write denied by <a href="https://github.com/jasongin"><code>@jasongin</code></a> in <a href="https://redirect.github.com/actions/setup-go/pull/758">actions/setup-go#758</a></li> <li>Upgrade version to 6.5.0 in package.json and package-lock.json by <a href="https://github.com/HarithaVattikuti"><code>@HarithaVattikuti</code></a> in <a href="https://redirect.github.com/actions/setup-go/pull/762">actions/setup-go#762</a></li> </ul> <h2>New Contributors</h2> <ul> <li><a href="https://github.com/priyagupta108"><code>@priyagupta108</code></a> with <a href="https://github.com/Copilot"><code>@Copilot</code></a> made their first contribution in <a href="https://redirect.github.com/actions/setup-go/pull/744">actions/setup-go#744</a></li> <li><a href="https://github.com/jasongin"><code>@jasongin</code></a> made their first contribution in <a href="https://redirect.github.com/actions/setup-go/pull/758">actions/setup-go#758</a></li> </ul> <p><strong>Full Changelog</strong>: <a href="https://github.com/actions/setup-go/compare/v6...v6.5.0">https://github.com/actions/setup-go/compare/v6...v6.5.0</a></p> <h2>v6.4.0</h2> <h2>What's Changed</h2> <h3>Enhancement</h3> <ul> <li>Add go-download-base-url input for custom Go distributions by <a href="https://github.com/gdams"><code>@gdams</code></a> in <a href="https://redirect.github.com/actions/setup-go/pull/721">actions/setup-go#721</a></li> </ul> <h3>Dependency update</h3> <ul> <li>Upgrade minimatch from 3.1.2 to 3.1.5 by <a href="https://github.com/dependabot"><code>@dependabot</code></a> in <a href="https://redirect.github.com/actions/setup-go/pull/727">actions/setup-go#727</a></li> </ul> <h3>Documentation update</h3> <ul> <li>Rearrange README.md, add advanced-usage.md by <a href="https://github.com/priyagupta108"><code>@priyagupta108</code></a> in <a href="https://redirect.github.com/actions/setup-go/pull/724">actions/setup-go#724</a></li> <li>Fix Microsoft build of Go link by <a href="https://github.com/gdams"><code>@gdams</code></a> in <a href="https://redirect.github.com/actions/setup-go/pull/734">actions/setup-go#734</a></li> </ul> <h2>New Contributors</h2> <ul> <li><a href="https://github.com/gdams"><code>@gdams</code></a> made their first contribution in <a href="https://redirect.github.com/actions/setup-go/pull/721">actions/setup-go#721</a></li> </ul> <p><strong>Full Changelog</strong>: <a href="https://github.com/actions/setup-go/compare/v6...v6.4.0">https://github.com/actions/setup-go/compare/v6...v6.4.0</a></p> <h2>v6.3.0</h2> <h2>What's Changed</h2> <ul> <li>Update default Go module caching to use go.mod by <a href="https://github.com/priyagupta108"><code>@priyagupta108</code></a> in <a href="https://redirect.github.com/actions/setup-go/pull/705">actions/setup-go#705</a></li> <li>Fix golang download url to go.dev by <a href="https://github.com/178inaba"><code>@178inaba</code></a> in <a href="https://redirect.github.com/actions/setup-go/pull/469">actions/setup-go#469</a></li> </ul> <p><strong>Full Changelog</strong>: <a href="https://github.com/actions/setup-go/compare/v6...v6.3.0">https://github.com/actions/setup-go/compare/v6...v6.3.0</a></p> <h2>v6.2.0</h2> <h2>What's Changed</h2> <!-- raw HTML omitted --> </blockquote> <p>... (truncated)</p> </details> <details> <summary>Commits</summary> <ul> <li><a href=" |
||
|
Copilot
|
63730fefaf
|
Fix swapped assert_expr arguments in smt_solver::translate for named assertions (#10135)
With `parallel.enable=true`, Z3 could return a SAT model for a QF_BV
instance that violates its own assertions. The bug traces to solver
translation: named assertions were re-registered with swapped
formula/indicator arguments, corrupting the translated solver's
assertion state.
## Bug
`m_name2assertion` stores `indicator → formula`. In
`smt_solver::translate()`, the structured binding `[k, v]` gives `k =
indicator`, `v = formula`, but `assert_expr(t, a)` expects `(formula,
indicator)`:
```cpp
// Before — args reversed
for (auto& [k, v] : m_name2assertion) {
expr* val = translator(k); // indicator
expr* key = translator(v); // formula
result->assert_expr(val, key); // assert_expr(indicator, formula) ← wrong
}
```
## Fix
```cpp
// After — correct order
for (auto& [k, v] : m_name2assertion) {
expr* fml = translator(v); // formula
expr* ind = translator(k); // indicator
result->assert_expr(fml, ind); // assert_expr(formula, indicator) ✓
}
```
This affects any code path that calls `smt_solver::translate()` and uses
named assertions (`assert_and_track` / `Z3_solver_assert_and_track`),
including all parallel solving modes.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
|
||
|
Nikolaj Bjorner
|
2a3b64a7f9 |
fix #10137
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> |