mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-11 05:30:51 +00:00
Code Activity

Check that Z3_get_numeral_small is given non-null out params

Browse source 
Analogous to other Z3_get_numeral_* functions with out params.
This commit is contained in:
Josh Berdine 2025-03-29 12:56:04 +00:00
parent 63ad2837e2
commit 9b5a9b2089
1 changed files with 4 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/api/api_numeral.cpp
View file

@ -318,6 +318,10 @@ extern "C" {
LOG_Z3_get_numeral_small(c, a, num, den); LOG_Z3_get_numeral_small(c, a, num, den);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
CHECK_IS_EXPR(a, false); CHECK_IS_EXPR(a, false);
if (!num || !den) {
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
return false;
}
rational r; rational r;
bool ok = Z3_get_numeral_rational(c, a, r); bool ok = Z3_get_numeral_rational(c, a, r);
if (ok) { if (ok) {