From 9b5a9b20895bb53bd0bdbcb43d483c2a6f0e982e Mon Sep 17 00:00:00 2001
From: Josh Berdine <josh@berdine.net>
Date: Sat, 29 Mar 2025 12:56:04 +0000
Subject: [PATCH] Check that Z3_get_numeral_small is given non-null out params

Analogous to other Z3_get_numeral_* functions with out params.
---
 src/api/api_numeral.cpp | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/api/api_numeral.cpp b/src/api/api_numeral.cpp
index 614395240..cee60272e 100644
--- a/src/api/api_numeral.cpp
+++ b/src/api/api_numeral.cpp
@@ -318,6 +318,10 @@ extern "C" {
         LOG_Z3_get_numeral_small(c, a, num, den);
         RESET_ERROR_CODE();
         CHECK_IS_EXPR(a, false);
+        if (!num || !den) {
+            SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
+            return false;
+        }
         rational r;
         bool ok = Z3_get_numeral_rational(c, a, r);
         if (ok) {