diff --git a/packages/z3/z3.4.13.0-1/files/libatomic.patch b/packages/z3/z3.4.13.0-1/files/libatomic.patch
new file mode 100644
index 00000000000..4ed518fbef9
--- /dev/null
+++ b/packages/z3/z3.4.13.0-1/files/libatomic.patch
@@ -0,0 +1,100 @@
+diff --git a/scripts/mk_util.py b/scripts/mk_util.py
+index 014b0e40f..3e6da0b22 100644
+--- a/scripts/mk_util.py
++++ b/scripts/mk_util.py
+@@ -314,6 +314,26 @@ def test_fpmath(cc):
+         FPMATH_FLAGS=""
+         return "UNKNOWN"
+ 
++def test_atomic_required(cc):
++    t = TempFile('tstatomic.cpp')
++    t.add("""
++    #include <atomic>
++    std::atomic<int> x;
++    std::atomic<short> y;
++    std::atomic<char> z;
++    std::atomic<long long> w;
++    int main() {
++        ++z;
++        ++y;
++        ++w;
++        return ++x;
++    }
++    """)
++    t.commit()
++    fails_without = exec_compiler_cmd([cc, CPPFLAGS, '', 'tstatomic.cpp', LDFLAGS, '']) != 0
++    ok_with = exec_compiler_cmd([cc, CPPFLAGS, '', 'tstatomic.cpp', LDFLAGS + ' -latomic', '']) == 0
++    return fails_without and ok_with
++
+ 
+ def find_jni_h(path):
+     for root, dirs, files in os.walk(path):
+@@ -555,19 +575,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)
+ 
+@@ -1858,7 +1878,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'))
+@@ -2600,6 +2620,9 @@ def mk_config():
+         CXXFLAGS = '%s -fvisibility=hidden -fvisibility-inlines-hidden -c' % CXXFLAGS
+         FPMATH = test_fpmath(CXX)
+         CXXFLAGS = '%s %s' % (CXXFLAGS, FPMATH_FLAGS)
++        atomic_required = test_atomic_required(CXX)
++        if atomic_required:
++            LDFLAGS  = '%s -latomic' % LDFLAGS
+         if LOG_SYNC:
+             CXXFLAGS = '%s -DZ3_LOG_SYNC' % CXXFLAGS
+         if SINGLE_THREADED:
+@@ -2710,6 +2733,7 @@ def mk_config():
+             print('Prefix:         %s' % PREFIX)
+             print('64-bit:         %s' % is64())
+             print('FP math:        %s' % FPMATH)
++            print('libatomic:      %s' % ('required' if atomic_required else 'not required'))
+             print("Python pkg dir: %s" % PYTHON_PACKAGE_DIR)
+             if GPROF:
+                 print('gprof:          enabled')
+@@ -2854,7 +2878,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:
+@@ -3068,7 +3092,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.13.0-1/opam b/packages/z3/z3.4.13.0-1/opam
new file mode 100644
index 00000000000..2de50df2a9a
--- /dev/null
+++ b/packages/z3/z3.4.13.0-1/opam
@@ -0,0 +1,43 @@
+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"
+patches: [
+  "libatomic.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"
+url {
+  src:
+    "https://github.com/Z3Prover/z3/archive/refs/tags/z3-4.13.0.tar.gz"
+  checksum: [
+    "sha256=01bcc61c8362e37bb89fd2430f7e3385e86df7915019bd2ce45de9d9bd934502"
+    "sha512=8503787fe0b18592b5a131bcec2cacfa5f5096d76386a1c4fda7a836e472924b154433306d27600ff0d0758ddb710c965901fbfc2e5605919b624b9d4d1bc4fd"
+  ]
+}