diff --git a/src/api/api_rcf.cpp b/src/api/api_rcf.cpp index 684e8c617..3bef38f0e 100644 --- a/src/api/api_rcf.cpp +++ b/src/api/api_rcf.cpp @@ -385,7 +385,7 @@ extern "C" { Z3_CATCH_RETURN(nullptr); } - int Z3_API Z3_rcf_interval(Z3_context c, Z3_rcf_num a, int * lower_is_inf, int * lower_is_open, Z3_rcf_num * lower, int * upper_is_inf, int * upper_is_open, Z3_rcf_num * upper) { + int Z3_API Z3_rcf_interval(Z3_context c, Z3_rcf_num a, bool * lower_is_inf, bool * lower_is_open, Z3_rcf_num * lower, bool * upper_is_inf, bool * upper_is_open, Z3_rcf_num * upper) { Z3_TRY; LOG_Z3_rcf_interval(c, a, lower_is_inf, lower_is_open, lower, upper_is_inf, upper_is_open, upper); RESET_ERROR_CODE(); diff --git a/src/api/z3_rcf.h b/src/api/z3_rcf.h index b3842f1b6..4286f1c43 100644 --- a/src/api/z3_rcf.h +++ b/src/api/z3_rcf.h @@ -272,9 +272,9 @@ extern "C" { \pre Z3_rcf_is_algebraic(ctx, a); - def_API('Z3_rcf_interval', INT, (_in(CONTEXT), _in(RCF_NUM), _out(INT), _out(INT), _out(RCF_NUM), _out(INT), _out(INT), _out(RCF_NUM))) + def_API('Z3_rcf_interval', INT, (_in(CONTEXT), _in(RCF_NUM), _out(BOOL), _out(BOOL), _out(RCF_NUM), _out(BOOL), _out(BOOL), _out(RCF_NUM))) */ - int Z3_API Z3_rcf_interval(Z3_context c, Z3_rcf_num a, int * lower_is_inf, int * lower_is_open, Z3_rcf_num * lower, int * upper_is_inf, int * upper_is_open, Z3_rcf_num * upper); + int Z3_API Z3_rcf_interval(Z3_context c, Z3_rcf_num a, bool * lower_is_inf, bool * lower_is_open, Z3_rcf_num * lower, bool * upper_is_inf, bool * upper_is_open, Z3_rcf_num * upper); /** \brief Return the number of sign conditions of an algebraic number. diff --git a/src/math/realclosure/realclosure.cpp b/src/math/realclosure/realclosure.cpp index 63e942989..0e6cc36f0 100644 --- a/src/math/realclosure/realclosure.cpp +++ b/src/math/realclosure/realclosure.cpp @@ -3429,7 +3429,7 @@ namespace realclosure { } } - bool get_interval(numeral const & a, int & lower_is_inf, int & lower_is_open, numeral & lower, int & upper_is_inf, int & upper_is_open, numeral & upper) + bool get_interval(numeral const & a, bool & lower_is_inf, bool & lower_is_open, numeral & lower, bool & upper_is_inf, bool & upper_is_open, numeral & upper) { if (!is_algebraic(a)) return false; @@ -6475,7 +6475,7 @@ namespace realclosure { return m_imp->get_sign_condition_sign(a, i); } - bool manager::get_interval(numeral const & a, int & lower_is_inf, int & lower_is_open, numeral & lower, int & upper_is_inf, int & upper_is_open, numeral & upper) + bool manager::get_interval(numeral const & a, bool & lower_is_inf, bool & lower_is_open, numeral & lower, bool & upper_is_inf, bool & upper_is_open, numeral & upper) { return m_imp->get_interval(a, lower_is_inf, lower_is_open, lower, upper_is_inf, upper_is_open, upper); } diff --git a/src/math/realclosure/realclosure.h b/src/math/realclosure/realclosure.h index 12247627b..a1fae3e2b 100644 --- a/src/math/realclosure/realclosure.h +++ b/src/math/realclosure/realclosure.h @@ -298,7 +298,7 @@ namespace realclosure { int get_sign_condition_sign(numeral const &a, unsigned i); - bool get_interval(numeral const & a, int & lower_is_inf, int & lower_is_open, numeral & lower, int & upper_is_inf, int & upper_is_open, numeral & upper); + bool get_interval(numeral const & a, bool & lower_is_inf, bool & lower_is_open, numeral & lower, bool & upper_is_inf, bool & upper_is_open, numeral & upper); unsigned num_sign_condition_coefficients(numeral const &a, unsigned i);