mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-22 05:36:41 +00:00
Code Activity

Make rcf is_rational and is_rational_function operations handle zero

Browse source 
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 <josh@berdine.net>
This commit is contained in:
Josh Berdine 2025-09-02 12:10:08 +01:00
parent 11fb5c7dc4
commit b9466587b1
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/realclosure/realclosure.cpp
View file

@ -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();
}