diff --git a/math/py-z3-solver/Makefile b/math/py-z3-solver/Makefile
index bbf694357a70..cbceca293d81 100644
--- a/math/py-z3-solver/Makefile
+++ b/math/py-z3-solver/Makefile
@@ -1,49 +1,49 @@
 PORTNAME=	z3-solver
 DISTVERSIONPREFIX=	z3-
-DISTVERSION=	4.13.2
+DISTVERSION=	4.13.3
 CATEGORIES=	math
 PKGNAMEPREFIX=	${PYTHON_PKGNAMEPREFIX}
 
 MAINTAINER=	yuri@FreeBSD.org
 COMMENT=	Python binding for Z3 Theorem Prover
 WWW=		https://github.com/Z3Prover/z3
 
 LICENSE=	MIT
 LICENSE_FILE=	${WRKSRC}/../../../LICENSE.txt
 
 LIB_DEPENDS=	libz3.so:math/z3
 
 USES=		cmake python
 USE_PYTHON=	flavors autoplist
 
 USE_GITHUB=	yes
 GH_ACCOUNT=	Z3Prover
 GH_PROJECT=	z3
 
 WRKSRC_SUBDIR=	src/api/python
 WRKSRC_top=	${WRKSRC}/../../..
 
 TEST_ENV=	${MAKE_ENV} PYTHONPATH=${STAGEDIR}${PYTHONPREFIX_SITELIBDIR}
 
 NO_ARCH=	yes
 
 post-patch:
 	@${RLN} ${WRKSRC_top}/scripts ${WRKSRC}/scripts
 	@${RLN} ${WRKSRC_top}/src/api ${WRKSRC}/api
 
 do-test:
 .for t in z3 z3num
 	@cd ${WRKSRC_top} && \
 		${CP} ${WRKSRC}/z3test.py . && \
 		${ECHO} "==> running the test ${t}" && \
 		${SETENV} ${TEST_ENV} ${PYTHON_CMD} z3test.py ${t} && \
 		${ECHO} "... test ${t} succeeded"
 .endfor
 .for e in kinematics power-of-two dog-cat-mouse sudoku eight-queens
 	@cd ${WRKSRC}/../../.. && \
 		${ECHO} "==> running the example ${e}" && \
 		${SETENV} ${TEST_ENV} ${PYTHON_CMD} ${FILESDIR}/example-${e}.py && \
 		${ECHO} "... example ${e} succeeded"
 .endfor
 
 .include <bsd.port.mk>
diff --git a/math/py-z3-solver/distinfo b/math/py-z3-solver/distinfo
index 884770bddf55..3a3e98e88025 100644
--- a/math/py-z3-solver/distinfo
+++ b/math/py-z3-solver/distinfo
@@ -1,3 +1,3 @@
-TIMESTAMP = 1728341031
-SHA256 (Z3Prover-z3-z3-4.13.2_GH0.tar.gz) = fd7dc6dd2633074f0a47670d6378b0e5c28c2c26f2b58aa23e9cd7f0bc9ba0dc
-SIZE (Z3Prover-z3-z3-4.13.2_GH0.tar.gz) = 5578178
+TIMESTAMP = 1731045651
+SHA256 (Z3Prover-z3-z3-4.13.3_GH0.tar.gz) = f59c9cf600ea57fb64ffeffbffd0f2d2b896854f339e846f48f069d23bc14ba0
+SIZE (Z3Prover-z3-z3-4.13.3_GH0.tar.gz) = 5583533