The Windows ARM64 nightly build (`mk_win_dist_cmake.py --arm64-only`)
was failing because the cmake-built `Microsoft.Z3` NuGet package was
produced without any native Windows DLL, causing the downstream dotnet
example build to fail.
## Root causes
- **Wrong DLL path in `Microsoft.Z3.csproj.in`**: Path included
`/$(_DN_CMAKE_CONFIG)/` (e.g., `.../RelWithDebInfo/libz3.dll`), but
`CMakeLists.txt` sets `CMAKE_RUNTIME_OUTPUT_DIRECTORY =
PROJECT_BINARY_DIR` with no config subdir. With Ninja single-config, the
DLL lands at `build-dir/libz3.dll`. The `Exists()` guard silently
excluded the DLL from the package.
- **Wrong runtime identifier**: ARM64 DLL was being packed under
`runtimes\win-x64\native` instead of `runtimes\win-arm64\native`.
- **Legacy copy fires for `net8.0`**: `Microsoft.Z3.targets` excluded
`netstandard`/`netcoreapp` but not modern TFMs like `net8.0`, so
`CopyToOutputDirectory` fired and failed trying to copy the absent
`win-x64` DLL.
## Changes
- **`src/api/dotnet/CMakeLists.txt`**: Introduce `Z3_DOTNET_WIN_RID`
cmake variable (`win-x64` / `win-x86` / `win-arm64`) derived from
`TARGET_ARCHITECTURE`; used at `configure_file` time.
- **`src/api/dotnet/Microsoft.Z3.csproj.in`**: Remove
`/$(_DN_CMAKE_CONFIG)` from the Windows DLL path; replace hardcoded
`runtimes\win-x64\native` with `runtimes\${Z3_DOTNET_WIN_RID}\native`.
- **`src/api/dotnet/Microsoft.Z3.targets`**: Add
`!$(TargetFramework.Contains('.'))` to the legacy-copy condition, which
correctly excludes `net5.0`/`net6.0`/`net7.0`/`net8.0` (all use dotted
TFMs) while keeping `net45`/`net472` etc.
- **`src/api/dotnet/Microsoft.Z3.props`**: Add explicit `arm64`
condition mapping `$(Platform) == 'arm64'` to
`runtimes\win-arm64\native\libz3.dll` for legacy .NET Framework ARM64
consumers.
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This updates the release and nightly pipelines so the Pyodide wheel is
built alongside the existing Python wheels and carried through the
normal publication flow. As a result, Pyodide wheels are included in
nightly assets and in release-time Python package publishing without
introducing a separate publishing path.
- **Pyodide build in release/nightly**
- Added a `pyodide-python` job to both `release.yml` and `nightly.yml`
- Reused the existing Pyodide build flow: install
`pyodide-build`/`pyodide-cli`, provision the matching Emscripten
toolchain, build the wheel, and run `z3test.py` against the built
artifact
- **Artifact integration**
- Upload the built wheel as a dedicated workflow artifact:
`PyodidePythonBuild`
- Extend the existing `python-package` aggregation job in both workflows
to depend on and download that artifact
- **Publication path**
- No new publish logic was added
- The existing downstream steps already publish everything collected in
`src/api/python/dist`, so the Pyodide wheel now flows into:
- nightly GitHub release assets
- release GitHub assets
- release-time PyPI publishing when enabled
```yaml
pyodide-python:
name: "Python bindings (Pyodide)"
...
- name: Upload artifact
uses: actions/upload-artifact@v7.0.1
with:
name: PyodidePythonBuild
path: src/api/python/dist/*.whl
python-package:
needs: [..., pyodide-python]
...
- name: Download Pyodide Build
uses: actions/download-artifact@v8.0.1
with:
name: PyodidePythonBuild
path: artifacts
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Z3 could return `sat` for an unsatisfiable QF_ABV formula equating two
store chains over distinct constant arrays. The rewrite path for array
equalities was missing a necessary base-value constraint in
finite-domain cases where stores cannot cover all indices.
- **Root cause**
- In `array_rewriter::mk_eq_core`, equality rewriting for nested stores
over const-array bases did not enforce equality of the underlying const
values when the index domain size exceeds the number of updated indices.
- **Rewriter fix**
- Added a sound rewrite branch for:
- `store* ((as const ...) v)` vs `store* ((as const ...) w)`
- When `|domain| > (#stores_lhs + #stores_rhs)`, rewrite now includes:
- select equalities for touched indices (existing behavior)
- **and** base-value equality `v = w` (new requirement)
- This prevents spurious models where only updated indices are
constrained.
- **Regression coverage**
- Added a focused regression in `src/test/mod_factor.cpp` that asserts
`unsat` for a minimized constant-array/store-chain BV case with
`(distinct x y)` and one store per side.
```cpp
(assert (distinct x y))
(assert (= (store A0 i0 e0) (store A1 i1 e1)))
(check-sat) ; expected: unsat
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Fix the TPTP frontend so that a bare name used in an equality refers to
a single shared `func_decl`, regardless of how the surrounding context
coerces its sort.
## Problem
With the following input the conjecture was not proved:
```tptp
fof(a1,axiom, ! [X] : (X = a)).
fof(c1,conjecture, b = a).
```
`parse_atomic_formula` created bare names as 0-arity **Bool
predicates**, and `coerce_eq` later retyped them by calling
`m.mk_func_decl(...)` directly, without registering the result in
`m_decls`. So the `a` used inside `! [X] : (X = a)` (coerced to sort
`U`) and the `a` used inside `b = a` (left as Bool) ended up as two
unrelated `func_decl`s sharing only the name. The axiom no longer
constrained the conjecture.
## Fix
In `src/cmd_context/tptp_frontend.cpp`:
1. Add `mk_zero_arity_decl(name, range)` / `coerce_zero_arity(app*,
range)` helpers that memoize the 0-arity `func_decl` per `(name, target
sort)` in `m_decls`, delegating to the existing `mk_decl_or_ho_const`
for `U` and Bool targets.
2. Rewrite `coerce_eq` to use the new helpers and add an explicit Bool /
non-Bool retyping branch so a bare-Bool side is recast to the other
side's sort.
3. In `parse_atomic_formula`, when a bare name is immediately followed
by `=` or `!=`, create it as a non-predicate (sort `U`). Terms in
equalities are no longer first introduced as Bool predicates.
4. Reorder the constructor init-list so `m_univ` is initialized before
the pinned ref vectors (matches declaration order; silences
`-Wreorder`).
Net effect: every reference to a given name at a given sort yields the
same `func_decl`, eliminating duplicate-symbol bugs in equalities over
bare TPTP constants.
## Test
Added `fof-bare-constant-equality` to `src/test/tptp.cpp`. Without the
C++ change the new case asserts; with it, `./build/release/test-z3 /seq
tptp` reports `PASS`.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Preserve the de-linearization of the linear constraints but fixing the
den bug. @ValentinPromies, that is what you had in mind.
---------
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Spacer can crash on small HORN/ADT benchmarks when model construction
reaches datatype enodes without a fully populated constructor state. The
failure manifested as a null/invalid-path dereference inside datatype
model value generation.
- **Root cause area: datatype model extraction path**
- Hardened `theory_datatype::mk_value` to handle incomplete theory state
safely instead of assuming constructor metadata is always present.
- Added guarded fallback to a factory-provided datatype value when:
- `th_var` is missing,
- union-find lookup is invalid,
- var data/constructor is unavailable.
- **Behavioral change**
- Missing constructor state now degrades to a safe model value
(`expr_wrapper_proc`) instead of crashing during model generation.
- **Regression coverage**
- Added a focused API regression in `src/test/api_datalog.cpp` using a
Spacer + ADT HORN script (with reproducing seed) to ensure the code path
executes without parser/runtime failure.
```cpp
// theory_datatype::mk_value fallback shape
if (v == null_theory_var || invalid_var_data || d->m_constructor == nullptr) {
app* val = to_app(m_factory->get_some_value(n->get_sort()));
return alloc(expr_wrapper_proc, val);
}
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This change simplifies recently touched API code in
`src/api/api_ast.cpp` without altering semantics. It removes an
unreachable error path in `Z3_get_index_value` and deletes an empty
comment in `Z3_mk_rec_func_decl`.
- **`Z3_get_index_value`: remove dead branch**
- After validating `a` is non-null and of kind `AST_VAR`, the conversion
to `var*` is already guaranteed by existing AST casting invariants.
- The redundant null-check/error-return branch was removed, leaving a
direct index return.
- **`Z3_mk_rec_func_decl`: remove noise**
- Deleted a stray empty `//` line.
```cpp
// before
var* va = to_var(_a);
if (va) {
return va->get_idx();
}
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
return 0;
// after
var* va = to_var(_a);
return va->get_idx();
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
`sat.smt=true` could return `sat` with an invalid model for QF_UFBV
formulas combining Bool-valued UFs and BV range constraints. The failure
came from broken model-trail reconstruction in `elim_unconstrained`,
where `ADD` entries were effectively turned into identity substitutions.
- **Root-cause fix: restore model-trail substitution composition**
- In `elim_unconstrained::update_model_trail`,
`generic_model_converter::ADD` entries now use `entry.m_def` (rewritten
through accumulated substitutions) instead of creating self-referential
const-to-const mappings.
- This re-enables correct back-substitution for eliminated unconstrained
terms during witness reconstruction.
- **Regression coverage: QF_UFBV + `sat.smt=true` + model validation**
- Added a focused unit test in `src/test/simplifier.cpp` for:
- Bool-valued UF predicate over BV vars
- split BV range constraints (`bvuge` / `bvult`)
- `:sat.smt true` and `:model_validate true`
- The test asserts the solver returns `sat` without emitting an
invalid-model error.
```cpp
// before (effectively no-op back-mapping)
new_def = m.mk_const(entry.m_f);
sub->insert(new_def, new_def, nullptr, nullptr);
// after (compose and apply recorded definition)
new_def = entry.m_def;
(*rp)(new_def);
sub->insert(m.mk_const(entry.m_f), new_def, nullptr, nullptr);
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Recent GCC builds report two warning classes in core codepaths: a
possible uninitialized read in `bound_propagator::relevant_bound`, and
repeated `-Warray-bounds` diagnostics in `mpz_manager::get_sign_cell`
when materializing small integers into a reserved `mpz_cell`.
- **Warning cleanup in bound propagation**
- Initialize `interval_size` at declaration in
`src/ast/simplifiers/bound_propagator.cpp` so the compiler can prove
safety across templated `LOWER/UPPER` instantiations using `std::clamp`.
- Preserves existing control flow and refinement heuristics (`bounded`
remains the gate for interval-based logic).
- **Warning cleanup in mpz small-value cell materialization**
- In `src/util/mpz.h`, replace direct writes through `cell->m_digits[0]`
with writes via a derived digits pointer
(`reinterpret_cast<digit_t*>(cell + 1)`), avoiding zero-length
trailing-array indexing diagnostics.
- Keeps memory layout and semantics unchanged for the stack-reserved
`sign_cell` buffer.
- **Representative change**
```cpp
cell = reserve;
cell->m_size = 1;
digit_t* cell_digits = reinterpret_cast<digit_t*>(cell + 1);
cell_digits[0] = a.value() < 0 ? -a.value() : a.value();
```
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This updates `src/solver/parallel_tactical2.cpp` with targeted
simplifications to align style and reduce local verbosity without
changing solver behavior. The changes are limited to member naming
consistency, cast style consistency, and a small `expr_ref` construction
cleanup.
- **`batch_manager` member naming consistency**
- Renamed the two outlier private fields to follow the existing `m_`
convention:
- `shared_clause_trail` → `m_shared_clause_trail`
- `shared_clause_set` → `m_shared_clause_set`
- Updated all corresponding reads/writes in clause collection, reset,
and clause-return paths.
- **Cast style consistency**
- Replaced C-style cast in thread count calculation with
`static_cast<unsigned>(...)` for consistency with style already used in
the file.
- **Simplified `expr_ref` construction in cube assembly**
- Collapsed default-init + assignment into direct construction when
pushing cube literals.
```cpp
// Before
expr_ref lit(g2l.to());
lit = g2l(cur->get_literal().get());
cube.push_back(std::move(lit));
// After
cube.push_back(expr_ref(g2l(cur->get_literal().get()), g2l.to()));
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Discussion #9524 reported systematic TPTP result polarity errors
(notably `Unsatisfiable/Theorem` cases returned as `Satisfiable`) and
timeout-path instability in the frontend. The dominant issue was
semantic: free variables in FOF/CNF formulas were parsed as constants
instead of implicitly universally quantified variables.
- **Parser semantics: free variables now follow TPTP rules**
- In `/home/runner/work/z3/z3/src/cmd_context/tptp_frontend.cpp`, free
variables encountered while parsing an annotated formula are now
collected in formula scope and wrapped with a top-level `forall`.
- This applies to both term and atomic-formula paths, so variable
occurrences are treated consistently.
- Explicitly bound quantifier variables continue to take precedence over
implicit ones.
- **Scoped implementation cleanup**
- Added scoped state for implicit-variable collection to avoid leaking
parser state across formulas.
- Kept variable binding order stable so quantifier construction is
deterministic.
- **Timeout-path robustness**
- Updated frontend exception catches to `const&` in the TPTP stream
entrypoint to make timeout/error handling behavior consistent with
thrown exception forms.
- **Regression tests**
- Extended `/home/runner/work/z3/z3/src/test/tptp.cpp` with focused
cases for:
- FOF free-variable implicit universal quantification.
- CNF free-variable implicit universal quantification.
```tptp
cnf(c1,axiom, p(X)).
cnf(c2,axiom, ~ p(a)).
```
This now maps to `forall X. p(X)` plus `~p(a)`, yielding `% SZS status
Unsatisfiable` as expected.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
`fpa2bv_converter::mk_to_real` computed `2^(1/|exp|)` instead of
`1/(2^|exp|)` for floats with negative exponents, causing the NRA solver
to reach contradictory conclusions and return spurious `unsat` for
satisfiable QF_FPLRA formulas.
## Root Cause
After the loop that evaluates `exp2 = |unbiased_exp|` as an integer, the
code took `1/exp2` (reciprocal of the integer) before calling
`mk_power`, yielding `2^(1/3)` instead of `2^(-3) = 1/8` for a float
with exponent -3:
```cpp
// Buggy
one_div_exp2 = mk_div(one, exp2); // 1/|exp|, not 1/2^|exp|
exp2 = mk_ite(exp_is_neg, one_div_exp2, exp2);
two_exp2 = mk_power(two, exp2); // 2^(1/3) ≠ 1/8 for exp=-3
```
## Fix
Compute the power of 2 first, then invert it:
```cpp
// Fixed
two_exp2 = mk_power(two, exp2); // 2^|exp|
one_div_two_exp2 = mk_div(one, two_exp2); // 1/(2^|exp|)
two_exp2 = mk_ite(exp_is_neg, one_div_two_exp2, two_exp2); // correct 2^exp
```
## Impact
- **QF_FPLRA**: `to_fp(RTZ, r)` with a symbolic real `r` constrained to
an interval containing a float's exact rational value now correctly
returns `sat`.
- **fp.to_real**: Fixes incorrect real-valued encoding for all floats
with negative exponents, including denormals (which adjust the exponent
by subtracting leading-zero count).
A regression test covering the reported case is added to
`src/test/fpa.cpp`.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This PR targets the main TFF frontend parsing failures: bare numeric
atoms were being treated as uninterpreted terms (`U`) in formula
position, decimal literals were not parsed, and `$uminus` was not
recognized as an arithmetic builtin. These issues caused widespread
parse/type failures in arithmetic-heavy TPTP inputs.
- **Numeric atom parsing in formulas (TFF)**
- Added a shared numeric-literal parser path for term/formula contexts.
- In atomic formulas, numeric LHS now parses as arithmetic numerals
before `=`/`!=` handling, avoiding `U` vs `Int/Real` mismatches.
- **Decimal literal support**
- Extended numeral parsing to accept `d.d` forms and construct `Real`
numerals.
- Keeps existing integer (`d`) and rational (`d/d`) behavior on the same
code path.
- **`$uminus` builtin support**
- Added explicit handling for `$uminus(<arg>)` in term parsing.
- Enforces arity 1 and arithmetic-argument checks; maps directly to
arithmetic unary minus.
- **Focused regression coverage**
- Added/updated TPTP unit cases for:
- bare integer inequality: `31 != 12`
- decimal arithmetic literal usage
- `$uminus` in arithmetic predicates
Example of now-supported inputs:
```tptp
tff(c1,conjecture, 31 != 12).
tff(c2,conjecture, ~ $less(-3.25,-8.69)).
tff(c3,conjecture, $less($uminus(2),0)).
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
