diff --git a/packages/z3/z3.4.12.3/files/optional-python-bytecode.patch b/packages/z3/z3.4.12.3/files/optional-python-bytecode.patch
new file mode 100644
index 00000000000..d21f9d957ae
--- /dev/null
+++ b/packages/z3/z3.4.12.3/files/optional-python-bytecode.patch
@@ -0,0 +1,64 @@
+diff --git a/scripts/mk_util.py b/scripts/mk_util.py
+index 3d3996792..370d643b5 100644
+--- a/scripts/mk_util.py
++++ b/scripts/mk_util.py
+@@ -555,19 +555,19 @@ def set_version(major, minor, build, revision):
+             print("Set Assembly Version (BUILD):", VER_MAJOR, VER_MINOR, VER_BUILD, VER_TWEAK)
+             return
+ 
+-    # use parameters to set up version if not provided by script args            
++    # use parameters to set up version if not provided by script args
+     VER_MAJOR = major
+     VER_MINOR = minor
+     VER_BUILD = build
+     VER_TWEAK = revision
+ 
+-    # update VER_TWEAK base on github     
++    # update VER_TWEAK base on github
+     if GIT_DESCRIBE:
+         branch = check_output(['git', 'rev-parse', '--abbrev-ref', 'HEAD'])
+         VER_TWEAK = int(check_output(['git', 'rev-list', '--count', 'HEAD']))
+-    
++
+     print("Set Assembly Version (DEFAULT):", VER_MAJOR, VER_MINOR, VER_BUILD, VER_TWEAK)
+-    
++
+ def get_version():
+     return (VER_MAJOR, VER_MINOR, VER_BUILD, VER_TWEAK)
+ 
+@@ -1856,7 +1856,7 @@ class JavaDLLComponent(Component):
+                           os.path.join('api', 'java', 'Native'))
+             elif IS_OSX and IS_ARCH_ARM64:
+                 out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) -arch arm64 %s$(OBJ_EXT) libz3$(SO_EXT)\n' %
+-                          os.path.join('api', 'java', 'Native'))                
++                          os.path.join('api', 'java', 'Native'))
+             else:
+                 out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(SO_EXT)\n' %
+                           os.path.join('api', 'java', 'Native'))
+@@ -2852,7 +2852,7 @@ def update_version():
+     revision = VER_TWEAK
+ 
+     print("UpdateVersion:", get_full_version_string(major, minor, build, revision))
+-    
++
+     if major is None or minor is None or build is None or revision is None:
+         raise MKException("set_version(major, minor, build, revision) must be used before invoking update_version()")
+     if not ONLY_MAKEFILES:
+@@ -2994,7 +2994,7 @@ def cp_z3py_to_build():
+                 rmf(os.path.join(root, f))
+     # Compile Z3Py files
+     if compileall.compile_dir(z3py_src, force=1) != 1:
+-        raise MKException("failed to compile Z3Py sources")
++        print("Python bytecode generation in %s failed, but that's ok" % z3py_src)
+     if is_verbose:
+         print("Generated python bytecode")
+     # Copy sources to build
+@@ -3056,7 +3056,7 @@ def mk_bindings(api_files):
+           z3py_output_dir=get_z3py_dir(),
+           dotnet_output_dir=dotnet_output_dir,
+           java_input_dir=java_input_dir,
+-          java_output_dir=java_output_dir,                                  
++          java_output_dir=java_output_dir,
+           java_package_name=java_package_name,
+           ml_output_dir=ml_output_dir,
+           ml_src_dir=ml_output_dir
diff --git a/packages/z3/z3.4.12.3/opam b/packages/z3/z3.4.12.3/opam
new file mode 100644
index 00000000000..d1084cba0a3
--- /dev/null
+++ b/packages/z3/z3.4.12.3/opam
@@ -0,0 +1,47 @@
+opam-version: "2.0"
+maintainer: "weng@cs.jhu.edu"
+authors: "MSR"
+homepage: "https://github.com/Z3prover/z3"
+bug-reports: "https://github.com/Z3prover/z3/issues"
+license: "MIT"
+dev-repo: "git+https://github.com/Z3prover/z3.git"
+depexts: [
+  ["python3-distutils"] {os-family = "debian"}
+]
+patches: ["optional-python-bytecode.patch"]
+build: [
+  [ "python3" "scripts/mk_make.py" "--ml" ]
+  [ make "-C" "build" "-j" jobs ]
+]
+
+install: [
+  [ "sh" "-c" "ocamlfind install z3 build/api/ml/* -dll build/libz3.*"]
+  [ "cp" "build/z3" "%{bin}%/z3"]
+]
+
+depends: [
+  "ocaml" {>= "4.08.0"}
+  "ocamlfind" {build}
+  "zarith"
+  "conf-gmp"
+  "conf-python-3" {build}
+  "conf-c++" {build}
+]
+x-ci-accept-failures: [
+  "centos-7" "oraclelinux-7" # C compiler is too old
+]
+conflicts: [
+  "ocaml-option-bytecode-only"
+]
+synopsis: "Z3 solver"
+extra-files: [
+  ["optional-python-bytecode.patch" "md5=109de0c68786d4739c93ad71f8bda86c"]
+]
+url {
+  src:
+    "https://github.com/Z3Prover/z3/archive/refs/tags/z3-4.12.3.tar.gz"
+  checksum: [
+    "sha256=61670733eb7a74eeca13033244cbec2c4098dca24a6fa3df0e7ae12ee8f33d9c"
+    "sha512=06d667b86e2d941e8cbcafe508392f5ef9307354a97428107e26ac7ef86246a86a0096fbf92034f2a3e47efe41f95ddc74460c2c4797aadec79e14020737afcb"
+  ]
+}