From b9466587b1d583a3aa1c6a46c30e6369b079f20d Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Tue, 2 Sep 2025 12:10:08 +0100 Subject: [PATCH] Make rcf is_rational and is_rational_function operations handle zero The representation of the zero rcf numeral is nullptr, and the is_rational and is_rational_function operations are not expecting to be called with nullptr. But there isn't a way to test for that in the API, other than checking if Z3_rcf_num_to_string returns "0". This patch adds a couple conditions so that is_rational and is_rational_function operations handle zero. Maybe this isn't the desired change. For instance, the is_zero operation could instead be exposed in the API and preconditions added to the relevant operations. Signed-off-by: Josh Berdine --- src/math/realclosure/realclosure.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/math/realclosure/realclosure.cpp b/src/math/realclosure/realclosure.cpp index 3e3ab2e0f..63e942989 100644 --- a/src/math/realclosure/realclosure.cpp +++ b/src/math/realclosure/realclosure.cpp @@ -1021,7 +1021,7 @@ namespace realclosure { } static bool is_rational_function(numeral const & a) { - return is_rational_function(a.m_value); + return !is_zero(a) && is_rational_function(a.m_value); } static rational_function_value * to_rational_function(numeral const & a) { @@ -2521,7 +2521,7 @@ namespace realclosure { \brief Return true if a is a rational. */ bool is_rational(numeral const & a) { - return a.m_value->is_rational(); + return is_zero(a) || a.m_value->is_rational(); }