diff --git a/sources b/sources
index 5d76ed9..949de7f 100644
--- a/sources
+++ b/sources
@@ -1 +1 @@
-SHA512 (z3-4.13.3.tar.gz) = c899f57d8cb5450801463b07cd651869d766a920e41a4beedc96c4978e940bfadff9af2fbbb5ba10f94f6742bb33f7abaca0a351f3e1803d778e84d735d6829e
+SHA512 (z3-5.1.0.tar.gz) = 03a854f720a56484ab99b8a5517150f1c9106400f54ad758cfa58e3ee2f95e349396a64d4f527a5bb9ee37f10ad9ecfa1916d1f5c921f04089deda409374491b
diff --git a/z3.spec b/z3.spec
index 885ec05..3c1df16 100644
--- a/z3.spec
+++ b/z3.spec
@@ -7,17 +7,21 @@
 # unless somebody is really, really persuasive and available to help fix it
 # if it breaks.
 
+# A Go interface is now available, but Fedora no longer builds Go library
+# packages (https://docs.fedoraproject.org/en-US/packaging-guidelines/Golang/).
+
 # Tests are off by default because some of the tests require more memory than
 # the koji builders have available.
 %bcond test 0
 
-%global giturl  https://github.com/Z3Prover/z3
-
 Name:           z3
-Version:        4.13.3
+Version:        5.1.0
 Release:        %autorelease
 Summary:        Satisfiability Modulo Theories (SMT) solver
 
+%global giturl  https://github.com/Z3Prover/z3
+%global majver  %{gsub %version ^(%d*%.%d*)%..*$ %1}
+
 License:        MIT
 URL:            https://github.com/Z3Prover/z3/wiki
 VCS :           git:%{giturl}.git
@@ -25,7 +29,21 @@ Source:         %{giturl}/archive/%{name}-%{version}.tar.gz
 # Do not try to build or install native OCaml artifacts on bytecode-only arches
 Patch:          %{name}-ocaml.patch
 
-BuildRequires:  cmake
+# See https://fedoraproject.org/wiki/Changes/EncourageI686LeafRemoval
+ExcludeArch:    %{ix86}
+BuildSystem:    cmake
+BuildOption(conf): -G Ninja
+BuildOption(conf): -DCMAKE_INSTALL_INCLUDEDIR=%{_includedir}/z3
+BuildOption(conf): -DZ3_BUILD_DOCUMENTATION:BOOL=ON
+%ifarch %{java_arches}
+BuildOption(conf): -DZ3_BUILD_JAVA_BINDINGS:BOOL=ON
+%endif
+BuildOption(conf): -DZ3_BUILD_PYTHON_BINDINGS:BOOL=ON
+BuildOption(conf): -DCMAKE_INSTALL_PYTHON_PKG_DIR=%{python3_sitelib}
+BuildOption(conf): -DZ3_INCLUDE_GIT_HASH:BOOL=OFF
+BuildOption(conf): -DZ3_INCLUDE_GIT_DESCRIBE:BOOL=OFF
+BuildOption(conf): -DZ3_USE_LIB_GMP:BOOL=ON
+
 BuildRequires:  doxygen
 BuildRequires:  gcc-c++
 BuildRequires:  gmp-devel
@@ -37,40 +55,32 @@ BuildRequires:  javapackages-tools
 %endif
 BuildRequires:  make
 BuildRequires:  ninja-build
-%ifnarch %{ix86}
 BuildRequires:  ocaml
 BuildRequires:  ocaml-findlib
-BuildRequires:  ocaml-ocamldoc
 BuildRequires:  ocaml-zarith-devel
-%endif
 BuildRequires:  python3-devel
 BuildRequires:  %{py3_dist setuptools}
 
 %description
 Z3 is a satisfiability modulo theories (SMT) solver; given a set of
-constraints with variables, it reports a set of values for those
-variables that would meet the constraints.  The Z3 input format is an
-extension of the one defined by the SMT-LIB 2.0 standard.  Z3 supports
-arithmetic, fixed-size bit-vectors, extensional arrays, datatypes,
-uninterpreted functions, and quantifiers.
+constraints with variables, it reports a set of values for those variables
+that would meet the constraints.  The Z3 input format is an extension of the
+one defined by the SMT-LIB 2.0 standard.  Z3 supports arithmetic, fixed-size
+bit-vectors, extensional arrays, datatypes, uninterpreted functions, and
+quantifiers.
 
 %package libs
 Summary:        Library for applications that use z3 functionality
 
-# This can be removed when F40 reaches EOL
-%ifnarch %{java_arches}
-Obsoletes:      java-z3 < 4.8.17-5
-%endif
-
 %description libs
 Library for applications that use z3 functionality.
 
 %package devel
-Summary:        Header files for build applications that use z3
+Summary:        Header files for building applications that use z3
 Requires:       z3-libs%{?_isa} = %{version}-%{release}
 
 %description devel
-Header files for build applications that use z3.
+Header files for building applications that use z3.
 
 %package doc
 # The content is MIT.
@@ -78,37 +88,19 @@ Header files for build applications that use z3.
 # examples/tptp/tptp5.tab.c
 # examples/tptp/tptp5.tab.c
 # Other licenses are due to files installed by doxygen.
-# html/bc_s.png: GPL-1.0-or-later
-# html/bdwn.png: GPL-1.0-or-later
-# html/closed.png: GPL-1.0-or-later
-# html/doc.png: GPL-1.0-or-later
+# html/clipboard.js: MIT
+# html/cookie.js: MIT
 # html/doxygen.css: GPL-1.0-or-later
 # html/doxygen.svg: GPL-1.0-or-later
 # html/dynsections.js: MIT
-# html/folderclosed.png: GPL-1.0-or-later
-# html/folderopen.png: GPL-1.0-or-later
 # html/jquery.js: MIT
-# html/nav_f.png: GPL-1.0-or-later
-# html/nav_g.png: GPL-1.0-or-later
-# html/nav_h.png: GPL-1.0-or-later
-# html/open.png: GPL-1.0-or-later
+# html/navtree.css: GPL-1.0-or-later
 # html/search/search.css: GPL-1.0-or-later
 # html/search/search.js: MIT
-# html/search/search_l.png: GPL-1.0-or-later
-# html/search/search_m.png: GPL-1.0-or-later
-# html/search/search_r.png: GPL-1.0-or-later
-# html/splitbar.png: GPL-1.0-or-later
-# html/sync_off.png: GPL-1.0-or-later
-# html/sync_on.png: GPL-1.0-or-later
-# html/tab_a.png: GPL-1.0-or-later
-# html/tab_b.png: GPL-1.0-or-later
-# html/tab_h.png: GPL-1.0-or-later
-# html/tab_s.png: GPL-1.0-or-later
 # html/tabs.css: GPL-1.0-or-later
 License:        MIT AND GPL-3.0-or-later WITH Bison-exception-2.2 AND GPL-1.0-or-later
 Summary:        API documentation for Z3
-# FIXME: this should be noarch, but we end up with different numbers of inheritance
-# graphs on different architectures.  Why?
+BuildArch:      noarch
 
 %description doc
 API documentation for Z3.
@@ -124,8 +116,6 @@ Requires:       javapackages-tools
 Java interface to z3.
 %endif
 
-# OCaml packages not built on i686 since OCaml 5 / Fedora 39.
-%ifnarch %{ix86}
 %package -n ocaml-z3
 Summary:        Ocaml interface to z3
 Requires:       z3-libs%{?_isa} = %{version}-%{release}
@@ -140,20 +130,22 @@ Requires:       ocaml-zarith-devel%{?_isa}
 
 %description -n ocaml-z3-devel
 Files for building ocaml applications that use z3.
-%endif
 
 %package -n python3-z3
 Summary:        Python 3 interface to z3
 BuildArch:      noarch
 Requires:       z3-libs = %{version}-%{release}
 
+# Provide the PyPI name
+%py_provides python3-z3-solver
+
 %description -n python3-z3
 Python 3 interface to z3.
 
 %prep
 %autosetup -N -n %{name}-%{name}-%{version}
 %ifnarch %{ocaml_native_compiler}
-%patch -P0 -p1
+%patch 0 -p1
 %endif
 
 # Enable verbose builds, use Fedora CFLAGS, preserve timestamps when installing,
@@ -165,37 +157,29 @@ sed \
   -e "s/\(['\"]\)cp\([^[:alnum:]]\)/\1cp -p\2/" \
   -e "s/\(SLIBEXTRAFLAGS = '\)'/\1-Wl,--no-whole-archive'/" \
   -e '/SLIBFLAGS/s|-shared|& %{build_ldflags} -Wl,--whole-archive|' \
-  -e 's/\(libz3$(SO_EXT)\)\(\\n\)/\1 -Wl,--no-whole-archive\2/' \
+  -e 's/\(libz3$(SO_EXT)\)\( \$(SLINK\)/\1 -Wl,--no-whole-archive\2/' \
   -e "s/OCAML_FLAGS = ''/OCAML_FLAGS = '-g'/" \
   -i scripts/mk_util.py
 
 # Comply with the Java packaging guidelines and fill in the version for python
-majver=$(cut -d. -f-2 <<< %{version})
 sed -e '/libz3java/s,\(System\.load\)Library("\(.*\)"),\1("%{_libdir}/z3/\2.so"),' \
-    -e "s/'so'/'so.$majver'/" \
+    -e "s/'so'/'so.%{majver}'/" \
     -i scripts/update_api.py
 
 # Turn off HTML timestamps for reproducible builds
 sed -i '/HTML_TIMESTAMP/s/YES/NO/' doc/z3api.cfg.in doc/z3code.dox
 
-%build
+%build -p
 export PYTHON=%{python3}
 
-%cmake -G Ninja \
-  -DCMAKE_INSTALL_INCLUDEDIR=%{_includedir}/z3 \
-  -DCMAKE_JAVA_COMPILE_FLAGS="-source;1.8;-target;1.8" \
-  -DZ3_BUILD_DOCUMENTATION:BOOL=ON \
-%ifarch %{java_arches}
-  -DZ3_BUILD_JAVA_BINDINGS:BOOL=ON \
-%endif
-  -DZ3_BUILD_PYTHON_BINDINGS:BOOL=ON \
-  -DZ3_INCLUDE_GIT_HASH:BOOL=OFF \
-  -DZ3_INCLUDE_GIT_DESCRIBE:BOOL=OFF \
-  -DZ3_USE_LIB_GMP:BOOL=ON
+%build -a
+# Remove meaningless memory addresses from the pydoc documentation
+# See https://github.com/python/cpython/issues/83572
+sed -ri 's/, handle [0-9a-fA-F]+//' \
+    %{_vpath_builddir}/doc/api/html/z3{,.z3{,num,poly,printer,rcf,util}}.html
+sed -ri 's/ at 0x[0-9a-fA-F]+//g' \
+    %{_vpath_builddir}/doc/api/html/z3.z3core.html
 
-%cmake_build
-
-%ifnarch %{ix86}
 # The cmake build system does not build the OCaml interface.  Do that manually.
 #
 # First, run the configure script to generate several files.
@@ -212,12 +196,8 @@ sed -i '/^api/s/ libz3\$(SO_EXT)//g' build/Makefile
 
 # Fourth, build the OCaml interface
 %make_build -C build ml
-%endif
-
-%install
-# Install the C++, python3, and Java interfaces
-%cmake_install
 
+%install -a
 %ifarch %{java_arches}
 # Move the Java interface to its correct location
 mkdir -p %{buildroot}%{_libdir}/z3
@@ -227,7 +207,6 @@ ln -s %{_jnidir}/com.microsoft.z3.jar %{buildroot}%{_libdir}/z3
 mv %{buildroot}%{_libdir}/libz3java.so %{buildroot}%{_libdir}/z3
 %endif
 
-%ifnarch %{ix86}
 # Install the OCaml interface
 cd build/api/ml
 mkdir -p %{buildroot}%{ocamldir}/Z3
@@ -238,7 +217,6 @@ cp -p META *.{a,cma,cmi,mli} %{buildroot}%{ocamldir}/Z3
 mkdir -p %{buildroot}%{ocamldir}/stublibs
 cp -p *.so %{buildroot}%{ocamldir}/stublibs
 cd -
-%endif
 
 # We handle the documentation files below
 rm -rf %{buildroot}%{_docdir}/Z3
@@ -251,8 +229,8 @@ help2man -N -o %{buildroot}%{_mandir}/man1/z3.1 \
 # Fix the pkgconfig file
 sed -i 's,//usr,,' %{buildroot}%{_libdir}/pkgconfig/z3.pc
 
-%if %{with test}
 %check
+%if %{with test}
 cd build
 make test-z3
 ./test-z3 /a
@@ -266,7 +244,7 @@ cd -
 
 %files libs
 %license LICENSE.txt
-%{_libdir}/libz3.so.4.13*
+%{_libdir}/libz3.so.5.1{,.*}
 
 %files devel
 %{_includedir}/z3/
@@ -281,10 +259,9 @@ cd -
 %ifarch %{java_arches}
 %files -n java-z3
 %{_libdir}/z3/
-%{_jnidir}/com.microsoft.z3*jar
+%{_jnidir}/com.microsoft.z3.jar
 %endif
 
-%ifnarch %{ix86}
 %files -n ocaml-z3
 %dir %{ocamldir}/Z3/
 %{ocamldir}/Z3/META
@@ -293,7 +270,7 @@ cd -
 %ifarch %{ocaml_native_compiler}
 %{ocamldir}/Z3/*.cmxs
 %endif
-%{ocamldir}/stublibs/*.so
+%{ocamldir}/stublibs/dllz3ml.so
 
 %files -n ocaml-z3-devel
 %{ocamldir}/Z3/*.a
@@ -302,7 +279,6 @@ cd -
 %{ocamldir}/Z3/*.cmxa
 %endif
 %{ocamldir}/Z3/*.mli
-%endif
 
 %files -n python3-z3
 %{python3_sitelib}/z3/