diff --git a/cad/yosys/Makefile b/cad/yosys/Makefile
index ba0524ba92af..93b24e0cc50b 100644
--- a/cad/yosys/Makefile
+++ b/cad/yosys/Makefile
@@ -1,45 +1,58 @@
 PORTNAME=	yosys
 DISTVERSIONPREFIX=	yosys-
-DISTVERSION=	0.24
+DISTVERSION=	0.25
 CATEGORIES=	cad
 
 MAINTAINER=	yuri@FreeBSD.org
 COMMENT=	Yosys Open SYnthesis Suite
 WWW=		https://yosyshq.net/yosys/
 
 LICENSE=	ISCL
 LICENSE_FILE=	${WRKSRC}/COPYING
 
 BUILD_DEPENDS=	abc:cad/abc \
 		bash:shells/bash \
 		gawk:lang/gawk
 LIB_DEPENDS=	libffi.so:devel/libffi
 RUN_DEPENDS=	xdot:x11/py-xdot@${PY_FLAVOR}
 TEST_DEPENDS=	bash:shells/bash \
 		iverilog:cad/iverilog
 
 USES=		bison compiler:c++11-lang gmake pkgconfig python:3.6+ readline \
 		shebangfix tcl
 
 SHEBANG_FILES=	backends/smt2/smtbmc.py \
 		misc/yosys-config.in
 SHEBANG_GLOB=	*.sh *.py
 
 USE_GITHUB=	yes
 GH_ACCOUNT=	YosysHQ
 
 BINARY_ALIAS=	python3=${PYTHON_CMD} tclsh=${TCLSH}
 MAKE_ARGS=	ABCEXTERNAL=abc
 MAKE_ENV=	MAKE=${GMAKE}
 
 TEST_TARGET=	test # some tests fail, see https://github.com/YosysHQ/yosys/issues/3505
 
+OPTIONS_GROUP=		SOLVERS
+OPTIONS_GROUP_SOLVERS=	CVC5 YICES Z3
+OPTIONS_DEFAULT=	YICES # same as the default in C++ code
+
+SOLVERS_DESC=		Install SAT solvers
+CVC5_DESC=		CVC SAT Solver
+YICES_DESC=		Yices SAT Solver
+Z3_DESC=		Z3 SAT Solver
+
+CVC5_RUN_DEPENDS=	cvc5:math/cvc5
+YICES_RUN_DEPENDS=	yices_smt2:math/yices
+Z3_RUN_DEPENDS=		z3:math/z3
+
 post-patch:
 	${REINPLACE_CMD} -e '/^CXX =/d; s/^LD = .*/LD = $$(CXX)/' \
 		-e '/^CONFIG/s/clang/${CHOSEN_COMPILER_TYPE}/' \
 		${WRKSRC}/Makefile
 
 post-install:
 	${STRIP_CMD} ${STAGEDIR}${PREFIX}/bin/yosys
 
 .include <bsd.port.mk>
diff --git a/cad/yosys/distinfo b/cad/yosys/distinfo
index f605e81864df..8d1f7daaed54 100644
--- a/cad/yosys/distinfo
+++ b/cad/yosys/distinfo
@@ -1,3 +1,3 @@
-TIMESTAMP = 1670571827
-SHA256 (YosysHQ-yosys-yosys-0.24_GH0.tar.gz) = 6a00b60e2d6bc8df0db1e66aa27af42a0694121cfcd6a3cf6f39c9329ed91263
-SIZE (YosysHQ-yosys-yosys-0.24_GH0.tar.gz) = 2659037
+TIMESTAMP = 1672860519
+SHA256 (YosysHQ-yosys-yosys-0.25_GH0.tar.gz) = 673e87eecb68fd5e889ac94b93dc9ae070f1a27d94dacbd738212cf09f39578c
+SIZE (YosysHQ-yosys-yosys-0.25_GH0.tar.gz) = 2465790
diff --git a/cad/yosys/files/patch-backends_smt2_smtio.py b/cad/yosys/files/patch-backends_smt2_smtio.py
new file mode 100644
index 000000000000..a39fc9c4fc91
--- /dev/null
+++ b/cad/yosys/files/patch-backends_smt2_smtio.py
@@ -0,0 +1,14 @@
+--- backends/smt2/smtio.py.orig	2023-01-04 19:51:15 UTC
++++ backends/smt2/smtio.py
+@@ -182,9 +182,9 @@ class SmtIo:
+                 self.noincr = True
+ 
+             if self.noincr:
+-                self.popen_vargs = ['yices-smt2'] + self.solver_opts
++                self.popen_vargs = ['yices_smt2'] + self.solver_opts
+             else:
+-                self.popen_vargs = ['yices-smt2', '--incremental'] + self.solver_opts
++                self.popen_vargs = ['yices_smt2', '--incremental'] + self.solver_opts
+             if self.timeout != 0:
+                 self.popen_vargs.append('-t')
+                 self.popen_vargs.append('%d' % self.timeout);