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.

diff --git a/src/util/real_algebraic_number_poly_imp.cpp b/src/util/real_algebraic_number_poly_imp.cpp
index d464f312d7a158359c20cd7ddf2d3101852a2ea8..1880502d67e0f5e5f94b960fa8a85ebbe4011baa 100644 (file)
--- 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