From 4a1c2f44c5b3a13d98b1078ced296cb836a4e4ad Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Thu, 29 Jan 2026 19:19:59 -0800 Subject: [PATCH] Fix assertion violation in mpzzp_manager::eq from non-normalized values in peek_fresh (#8439) * 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 --- src/math/polynomial/polynomial.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp index 8228f8d84..2db2e1bb0 100644 --- a/src/math/polynomial/polynomial.cpp +++ b/src/math/polynomial/polynomial.cpp @@ -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) {