From: Gereon Kremer <gkremer@cs.stanford.edu>
Date: Wed, 23 Feb 2022 18:08:22 +0000 (+0100)
Subject: Fix creation of RAN from non-dyadic rational (#8138)
X-Git-Tag: cvc5-1.0.0~398
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2160fef57b24ef35d9334f5bb5faa1ba87c8a2f4;p=cvc5.git

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 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