The constructor FastRational::FastRational(word num, uword den) was not
normalizing the numerator and denumerator correctly.
If the numerator was negative, one division would mix signed and
unsigned types, causing the signed type to be implicitly casted to
unsigned type, completely changing the value of the numerator.
Fortunately, in our codebase, this particular constructor has never been
called in a way that would cause this bug to manifest. But users could
construct rational numbers in this way when using OpenSMT as a library.
Here we patch the computation to handle signedness correctly.
Longer-term, we should consider using signed type for the denumerator as
well.
It would allow for smaller range of values available for the fast and
compact representation, but it could simplify the code significantly and
avoid any signed/unsigned issues.
The constructor FastRational::FastRational(word num, uword den) was not normalizing the numerator and denumerator correctly. If the numerator was negative, one division would mix signed and unsigned types, causing the signed type to be implicitly casted to unsigned type, completely changing the value of the numerator.
Fortunately, in our codebase, this particular constructor has never been called in a way that would cause this bug to manifest. But users could construct rational numbers in this way when using OpenSMT as a library.
Here we patch the computation to handle signedness correctly. Longer-term, we should consider using signed type for the denumerator as well. It would allow for smaller range of values available for the fast and compact representation, but it could simplify the code significantly and avoid any signed/unsigned issues.