diff --git a/devel/cbmc/Makefile b/devel/cbmc/Makefile
index c7f7b3650e63..92743c0170be 100644
--- a/devel/cbmc/Makefile
+++ b/devel/cbmc/Makefile
@@ -1,46 +1,46 @@
 PORTNAME=	cbmc
-PORTVERSION=	5.95.1
+PORTVERSION=	6.3.1
 DISTVERSIONPREFIX=	cbmc-
 CATEGORIES=	devel
 MASTER_SITES=	DEBIAN/pool/main/m/minisat2:minisat
 DISTFILES=	minisat2_2.2.1.orig.tar.gz:minisat
 
 MAINTAINER=	olivier@FreeBSD.org
 COMMENT=	Bounded Model Checker for C and C++ programs
 WWW=		https://github.com/diffblue/cbmc
 
 LICENSE=	BSD4CLAUSE
 LICENSE_FILE=	${WRKSRC}/LICENSE
 
 BUILD_DEPENDS=	${LOCALBASE}/bin/flex:textproc/flex
 RUN_DEPENDS=	${LOCALBASE}/bin/cvc5:math/cvc5 \
 		${LOCALBASE}/bin/z3:math/z3
 
 USES=		gmake bison python shebangfix
 
 USE_GITHUB=	yes
 GH_ACCOUNT=	diffblue
 SHEBANG_FILES=	${WRKSRC}/scripts/ls_parse.py
 WRKSRC_minisat=	${WRKDIR}/minisat2-2.2.1
 
 post-patch:
 	@${REINPLACE_CMD} -e 's|.*git describe --tags.*|GIT_INFO = ${PORTNAME}-${PORTVERSION}|' \
 		${WRKSRC}/src/util/Makefile
 post-extract:
 	@${MV} ${WRKSRC_minisat} ${WRKSRC}/minisat-2.2.1
 
 do-build:
 	@${MKDIR} ${STAGEDIR}
 	cd ${WRKSRC} && ${GMAKE} -C src -j${MAKE_JOBS_NUMBER}
 
 do-install:
 .  for x in cbmc crangler goto-analyzer goto-cc goto-diff goto-instrument \
 	goto-inspect goto-harness goto-synthesizer symtab2gb
 	${INSTALL_PROGRAM} ${WRKSRC}/src/${x}/${x} ${STAGEDIR}${PREFIX}/bin/
 	${INSTALL_MAN} ${WRKSRC}/doc/man/${x}.1 ${STAGEDIR}${PREFIX}/share/man/man1/
 .  endfor
 	${LN} -sf goto-cc ${STAGEDIR}${PREFIX}/bin/goto-gcc
 	${LN} -sf goto-cc ${STAGEDIR}${PREFIX}/bin/goto-ld
 	${INSTALL_SCRIPT} ${WRKSRC}/scripts/ls_parse.py ${STAGEDIR}${PREFIX}/bin/
 
 .include <bsd.port.mk>
diff --git a/devel/cbmc/distinfo b/devel/cbmc/distinfo
index f3e6d1161c6a..bff667f3f615 100644
--- a/devel/cbmc/distinfo
+++ b/devel/cbmc/distinfo
@@ -1,5 +1,5 @@
-TIMESTAMP = 1706723199
+TIMESTAMP = 1730030005
 SHA256 (minisat2_2.2.1.orig.tar.gz) = e54afa3c192c1753bc8075c0c7e126d5c495d9066e3f90a2588091149ac9ca40
 SIZE (minisat2_2.2.1.orig.tar.gz) = 44229
-SHA256 (diffblue-cbmc-cbmc-5.95.1_GH0.tar.gz) = fdc1e862752430f8d069eb2f9c33dcd05078cf955bbc900e2cc840bcb01b3783
-SIZE (diffblue-cbmc-cbmc-5.95.1_GH0.tar.gz) = 9073428
+SHA256 (diffblue-cbmc-cbmc-6.3.1_GH0.tar.gz) = cc9183eff2046b41cae28c21e551184e5dbb8125b06c6043ceaceb44dd75886c
+SIZE (diffblue-cbmc-cbmc-6.3.1_GH0.tar.gz) = 9120942
diff --git a/devel/cbmc/files/patch-src_common b/devel/cbmc/files/patch-src_common
deleted file mode 100644
index 6944a39d7788..000000000000
--- a/devel/cbmc/files/patch-src_common
+++ /dev/null
@@ -1,11 +0,0 @@
---- src/common.orig	2024-02-01 00:44:35 UTC
-+++ src/common
-@@ -64,7 +64,7 @@ else ifeq ($(filter-out FreeBSD,$(BUILD_ENV_)),)
-   YFLAGS ?= -v
- else ifeq ($(filter-out FreeBSD,$(BUILD_ENV_)),)
-   CP_CXXFLAGS +=
--  LINKLIB = ar rcT $@ $^
-+  LINKLIB = llvm-ar rcT $@ $^
-   LINKBIN = $(CXX) $(LINKFLAGS) -o $@ -Wl,--start-group $^ -Wl,--end-group $(LIBS)
-   LINKNATIVE = $(HOSTCXX) $(HOSTLINKFLAGS) -o $@ $^
-   ifeq ($(origin CC),default)
diff --git a/devel/cbmc/files/patch-src_solvers_sat_external__sat.cpp b/devel/cbmc/files/patch-src_solvers_sat_external__sat.cpp
deleted file mode 100644
index f0dd61cd9963..000000000000
--- a/devel/cbmc/files/patch-src_solvers_sat_external__sat.cpp
+++ /dev/null
@@ -1,13 +0,0 @@
---- src/solvers/sat/external_sat.cpp.orig	2023-10-30 12:11:18 UTC
-+++ src/solvers/sat/external_sat.cpp
-@@ -119,8 +119,8 @@ external_satt::resultt external_satt::parse_result(std
-       {
-         try
-         {
--          signed long long as_long = std::stol(assignment_string);
--          size_t index = std::labs(as_long);
-+          signed long long as_long = std::stoll(assignment_string);
-+          size_t index = std::llabs(as_long);
- 
-           if(index >= number_of_variables)
-           {
diff --git a/devel/cbmc/files/patch-src_util_optional.h b/devel/cbmc/files/patch-src_util_optional.h
deleted file mode 100644
index 4507ce0ade2b..000000000000
--- a/devel/cbmc/files/patch-src_util_optional.h
+++ /dev/null
@@ -1,29 +0,0 @@
---- src/util/optional.h.orig	2023-10-30 12:11:18 UTC
-+++ src/util/optional.h
-@@ -11,20 +11,20 @@ Author: Diffblue Ltd.
- #define CPROVER_UTIL_OPTIONAL_H
- 
- #if defined __clang__
--  #pragma clang diagnostic push ignore "-Wall"
--  #pragma clang diagnostic push ignore "-Wpedantic"
-+  #pragma clang diagnostic push
-+  #pragma clang diagnostic ignored "-Wall"
-+  #pragma clang diagnostic ignored "-Wpedantic"
- #elif defined __GNUC__
--  #pragma GCC diagnostic push ignore "-Wall"
--  #pragma GCC diagnostic push ignore "-Wpedantic"
-+  #pragma GCC diagnostic push
-+  #pragma GCC diagnostic ignored "-Wall"
-+  #pragma GCC diagnostic ignored "-Wpedantic"
- #elif defined _MSC_VER
-   #pragma warning(push)
- #endif
- #include <nonstd/optional.hpp>
- #if defined  __clang__
-   #pragma clang diagnostic pop
--  #pragma clang diagnostic pop
- #elif defined  __GNUC__
--  #pragma GCC diagnostic pop
-   #pragma GCC diagnostic pop
- #elif defined _MSC_VER
-   #pragma warning(pop)