diff --git a/math/py-z3-solver/Makefile b/math/py-z3-solver/Makefile
index b8d3d8b1378e..40d18c74e1f4 100644
--- a/math/py-z3-solver/Makefile
+++ b/math/py-z3-solver/Makefile
@@ -1,51 +1,50 @@
 PORTNAME=	z3-solver
 DISTVERSIONPREFIX=	z3-
-DISTVERSION=	4.14.1
-PORTREVISION=	2
+DISTVERSION=	4.16.0
 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"
 	@${ECHO} "All tests succeeded."
 .endfor
 
 .include <bsd.port.mk>
diff --git a/math/py-z3-solver/distinfo b/math/py-z3-solver/distinfo
index 7626b5b86593..e2a94a1fdfec 100644
--- a/math/py-z3-solver/distinfo
+++ b/math/py-z3-solver/distinfo
@@ -1,3 +1,3 @@
-TIMESTAMP = 1742764116
-SHA256 (Z3Prover-z3-z3-4.14.1_GH0.tar.gz) = 81a02c2c64c64d6c3df233f59186b95627990ada0c4c2fc901c9c25a7072672a
-SIZE (Z3Prover-z3-z3-4.14.1_GH0.tar.gz) = 5844214
+TIMESTAMP = 1744070000
+SHA256 (Z3Prover-z3-z3-4.16.0_GH0.tar.gz) = c68c3e5e4810b16126b8cb4c47eee85c1ac3e24a81914c8e371b40de9dd33ac7
+SIZE (Z3Prover-z3-z3-4.16.0_GH0.tar.gz) = 6136396
diff --git a/math/py-z3-solver/files/patch-CMakeLists.txt b/math/py-z3-solver/files/patch-CMakeLists.txt
index 670b2e2e4e50..7e66518bee38 100644
--- a/math/py-z3-solver/files/patch-CMakeLists.txt
+++ b/math/py-z3-solver/files/patch-CMakeLists.txt
@@ -1,30 +1,41 @@
---- CMakeLists.txt.orig	2024-10-07 22:51:28 UTC
+--- CMakeLists.txt.orig	2026-02-18 22:57:51 UTC
 +++ CMakeLists.txt
-@@ -1,4 +1,27 @@ message(STATUS "Emitting rules to build Z3 python bind
+@@ -1,4 +1,38 @@ message(STATUS "Emitting rules to build Z3 python bind
  message(STATUS "Emitting rules to build Z3 python bindings")
 +
 +## portion of src/CMakeLists.txt
 +set(Z3_API_HEADER_FILES_TO_SCAN
 +  z3_api.h
 +  z3_ast_containers.h
 +  z3_algebraic.h
 +  z3_polynomial.h
 +  z3_rcf.h
 +  z3_fixedpoint.h
 +  z3_optimization.h
 +  z3_fpa.h
 +  z3_spacer.h
 +)
 +set(Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN "")
 +foreach (header_file ${Z3_API_HEADER_FILES_TO_SCAN})
 +  set(full_path_api_header_file "${CMAKE_CURRENT_SOURCE_DIR}/api/${header_file}")
 +  list(APPEND Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN "${full_path_api_header_file}")
 +  if (NOT EXISTS "${full_path_api_header_file}")
 +    message(FATAL_ERROR "API header file \"${full_path_api_header_file}\" does not exist")
 +  endif()
 +endforeach()
 +
++## Define libz3 as an imported target pointing to the pre-installed library
++if (NOT TARGET libz3)
++  find_library(LIBZ3_LIBRARY NAMES z3 libz3)
++  if (NOT LIBZ3_LIBRARY)
++    message(FATAL_ERROR "Could not find libz3 library")
++  endif()
++  add_library(libz3 SHARED IMPORTED)
++  set_target_properties(libz3 PROPERTIES
++    IMPORTED_LOCATION "${LIBZ3_LIBRARY}"
++  )
++endif()
 +
  ###############################################################################
  # Add target to build python bindings for the build directory
  ###############################################################################