From 2160fef57b24ef35d9334f5bb5faa1ba87c8a2f4 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Wed, 23 Feb 2022 19:08:22 +0100 Subject: [PATCH] Fix creation of RAN from non-dyadic rational (#8138) Libpoly only allows to create real algebraic numbers from dyadic rationals. For non-dyadic rationals, we need to create a polynomials and create it the general way. Libpoly requires all defining polynomials to be primitive, in particular the leading coefficient must be positive. We would always have it negative, which only becomes a problem if libpoly has assertions enabled, though. Fixes #8126. --- src/util/real_algebraic_number_poly_imp.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/util/real_algebraic_number_poly_imp.cpp b/src/util/real_algebraic_number_poly_imp.cpp index d464f312d..1880502d6 100644 --- a/src/util/real_algebraic_number_poly_imp.cpp +++ b/src/util/real_algebraic_number_poly_imp.cpp @@ -61,7 +61,7 @@ RealAlgebraicNumber::RealAlgebraicNumber(const Rational& r) else { d_value = poly::AlgebraicNumber( - poly::UPolynomial({numerator(pr), -denominator(pr)}), + poly::UPolynomial({-numerator(pr), denominator(pr)}), poly::DyadicInterval(floor(pr), ceil(pr))); } #endif -- 2.30.2