Fix creation of RAN from non-dyadic rational (#8138)
authorGereon Kremer <gkremer@cs.stanford.edu>
Wed, 23 Feb 2022 18:08:22 +0000 (19:08 +0100)
committerGitHub <noreply@github.com>
Wed, 23 Feb 2022 18:08:22 +0000 (18:08 +0000)
commit2160fef57b24ef35d9334f5bb5faa1ba87c8a2f4
tree63b7e4653f73b1c60e5ad3fff5cc20ce50fa05b1
parent659068a3b3ba4bc9fed9a53ee5e1cf06e66d8df5
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