mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-01 23:07:59 +00:00
Code Activity

Fix assertion violation in mpzzp_manager::eq from non-normalized values in peek_fresh (#8439)

Browse source 
* Initial plan

* Normalize values in peek_fresh and newton_interpolator::add

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Simplify fix - only normalize in peek_fresh with assertions

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Delete regressions/issue-8292.smt2

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Copilot 2026-01-29 19:19:59 -08:00 • committed by GitHub
parent 0519e6231c
commit 4a1c2f44c5
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 3 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/math/polynomial/polynomial.cpp
View file

@ -4391,9 +4391,12 @@ namespace polynomial {
// select a new random value in GF(p) that is not in vals, and store it in r
void peek_fresh(scoped_numeral_vector const & vals, unsigned p, scoped_numeral & r) {
SASSERT(vals.size() < p); // otherwise we can't keep the fresh value
SASSERT(m().modular()); // ensure we're in modular mode
auto sz = vals.size();
while (true) {
m().set(r, rand() % p);
m().p_normalize(r.get()); // normalize the value to ensure it's in the correct range
SASSERT(m().is_p_normalized(r)); // verify normalization succeeded
// check if fresh value...
unsigned k = 0;
for (; k < sz; ++k) {