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>
`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>
* Compute term generations based on minimal match
* Tidy up get_*_f_app
* Update euf_mam to the minimum generation number among matches
* Update euf_mam.cpp
* Move the UNREACHABLE() test to smt_mam.cpp
* Enforce stickiness of max-generation
* Add current generation tracking to bind structure
* Fix build error
---------
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
The arith rewriter now recognizes that x * (x + 1) >= 0 for all
integers, since no integer lies strictly between -1 and 0.
Two changes:
1. is_non_negative: detect products where unpaired factors are
consecutive integer expressions (differ by exactly 1), handling
both +1 and -1 offsets and n-ary additions
2. is_separated: return true for (>= non_negative_mul 0), restricted
to multiplication expressions to avoid disrupting other theories
Also adds regression tests for the new simplification.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The mk_to_real function in fpa2bv_converter.cpp was missing the
normalization shift adjustment (lz) when computing the real-valued
exponent for denormal floating-point numbers.
When unpack(x, sgn, sig, exp, lz, normalize=true) normalizes a denormal
by shifting the significand left by lz positions, the returned exp does
not account for this shift. All other callers (mk_mul, mk_div, mk_fma)
correctly subtract lz from the exponent, but mk_to_real was missing this.
The fix subtracts zero-extended lz from the sign-extended exp to get the
true exponent, matching the convention used by other FP operations.
Fixes incorrect model with (_ FloatingPoint 2 24) and fp.to_real.
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
