diff --git a/README.md b/README.md
index fe5483d51f..fcf6e4cec6 100644
--- a/README.md
+++ b/README.md
@@ -61,20 +61,20 @@ Only a few SMT solvers provide support for theories like Arrays, Floating Point,
 
 JavaSMT supports several SMT solvers (see [Getting Started](doc/Getting-started.md) for installation):
 
-| SMT Solver                                                              |      Linux x64      |     Linux arm64     |    Windows x64     |   Windows arm64    |                        MacOS x64                        |    MacOS arm64     | Description                                                                 |
-|-------------------------------------------------------------------------|:-------------------:|:-------------------:|:------------------:|:------------------:|:-------------------------------------------------------:|:------------------:|:----------------------------------------------------------------------------|
-| [Bitwuzla](https://bitwuzla.github.io/)                                 | :heavy_check_mark:² | :heavy_check_mark:² | :heavy_check_mark: |                    |                                                         |                    | a fast solver for bitvector logic                                           |
-| [Boolector](https://boolector.github.io/)                               | :heavy_check_mark:  |                     |                    |                    |                                                         |                    | a fast solver for bitvector logic, misses formula introspection, deprecated |
-| [CVC4](https://cvc4.github.io/)                                         | :heavy_check_mark:  |                     |                    |                    |                                                         |                    |                                                                             |
-| [CVC5](https://cvc5.github.io/)                                         | :heavy_check_mark:  | :heavy_check_mark:  | :heavy_check_mark: | :heavy_check_mark: |                   :heavy_check_mark:                    | :heavy_check_mark: |                                                                             |
-| [MathSAT5](http://mathsat.fbk.eu/)                                      | :heavy_check_mark:³ | :heavy_check_mark:³ | :heavy_check_mark: |                    | [maybe](https://github.com/sosy-lab/java-smt/pull/430)⁴ |                    |                                                                             |
-| [OpenSMT](https://verify.inf.usi.ch/opensmt)                            | :heavy_check_mark:² | :heavy_check_mark:² |                    |                    |                                                         |                    |                                                                             |
-| [OptiMathSAT](http://optimathsat.disi.unitn.it/)                        | :heavy_check_mark:  |                     |                    |                    |                                                         |                    | based on MathSAT5, with support for optimization queries                    |
-| [Princess](http://www.philipp.ruemmer.org/princess.shtml)               | :heavy_check_mark:  | :heavy_check_mark:  | :heavy_check_mark: | :heavy_check_mark: |                   :heavy_check_mark:                    | :heavy_check_mark: | Java-based SMT solver                                                       |
-| [SMTInterpol](https://ultimate.informatik.uni-freiburg.de/smtinterpol/) | :heavy_check_mark:  | :heavy_check_mark:  | :heavy_check_mark: | :heavy_check_mark: |                   :heavy_check_mark:                    | :heavy_check_mark: | Java-based SMT solver                                                       |
-| [Yices2](https://yices.csl.sri.com/)                                    | :heavy_check_mark:  |                     | :heavy_check_mark: |                    | [maybe](https://github.com/sosy-lab/java-smt/pull/400)⁴ |                    |                                                                             |
-| [Z3](https://github.com/Z3Prover/z3)                                    | :heavy_check_mark:³ | :heavy_check_mark:³ | :heavy_check_mark: | :heavy_check_mark: |                   :heavy_check_mark:                    | :heavy_check_mark: | mature and well-known solver                                                |
-| [Z3_WITH_INTERPOLATION](https://github.com/Z3Prover/z3)                 | :heavy_check_mark:  | :heavy_check_mark:  |                    |                    |                                                         |                    | an older version of Z3 that still provides interpolation support            |
+| SMT Solver                                                              |      Linux x64      |     Linux arm64     |    Windows x64     |   Windows arm64    |                        MacOS x64                        |                MacOS arm64                | Description                                                                 |
+|-------------------------------------------------------------------------|:-------------------:|:-------------------:|:------------------:|:------------------:|:-------------------------------------------------------:|:-----------------------------------------:|:----------------------------------------------------------------------------|
+| [Bitwuzla](https://bitwuzla.github.io/)                                 | :heavy_check_mark:² | :heavy_check_mark:² | :heavy_check_mark: |                    |                                                         |                                           | a fast solver for bitvector logic                                           |
+| [Boolector](https://boolector.github.io/)                               | :heavy_check_mark:  |                     |                    |                    |                                                         |                                           | a fast solver for bitvector logic, misses formula introspection, deprecated |
+| [CVC4](https://cvc4.github.io/)                                         | :heavy_check_mark:  |                     |                    |                    |                                                         |                                           |                                                                             |
+| [CVC5](https://cvc5.github.io/)                                         | :heavy_check_mark:  | :heavy_check_mark:  | :heavy_check_mark: | :heavy_check_mark: |                   :heavy_check_mark:                    |            :heavy_check_mark:             |                                                                             |
+| [MathSAT5](http://mathsat.fbk.eu/)                                      | :heavy_check_mark:³ | :heavy_check_mark:³ | :heavy_check_mark: |                    | [maybe](https://github.com/sosy-lab/java-smt/pull/430)⁴ |                                           |                                                                             |
+| [OpenSMT](https://verify.inf.usi.ch/opensmt)                            | :heavy_check_mark:² | :heavy_check_mark:² |                    |                    |                                                         |                                           |                                                                             |
+| [OptiMathSAT](http://optimathsat.disi.unitn.it/)                        | :heavy_check_mark:  |                     |                    |                    |                                                         |                                           | based on MathSAT5, with support for optimization queries                    |
+| [Princess](http://www.philipp.ruemmer.org/princess.shtml)               | :heavy_check_mark:  | :heavy_check_mark:  | :heavy_check_mark: | :heavy_check_mark: |                   :heavy_check_mark:                    |            :heavy_check_mark:             | Java-based SMT solver                                                       |
+| [SMTInterpol](https://ultimate.informatik.uni-freiburg.de/smtinterpol/) | :heavy_check_mark:  | :heavy_check_mark:  | :heavy_check_mark: | :heavy_check_mark: |                   :heavy_check_mark:                    |            :heavy_check_mark:             | Java-based SMT solver                                                       |
+| [Yices2](https://yices.csl.sri.com/)                                    | :heavy_check_mark:  |                     | :heavy_check_mark: |                    |        [partial](doc/How-to-build-for-macOS.md)⁴        | [partial](doc/How-to-build-for-macOS.md)⁴ |                                                                             |
+| [Z3](https://github.com/Z3Prover/z3)                                    | :heavy_check_mark:³ | :heavy_check_mark:³ | :heavy_check_mark: | :heavy_check_mark: |                   :heavy_check_mark:                    |            :heavy_check_mark:             | mature and well-known solver                                                |
+| [Z3_WITH_INTERPOLATION](https://github.com/Z3Prover/z3)                 | :heavy_check_mark:  | :heavy_check_mark:  |                    |                    |                                                         |                                           | an older version of Z3 that still provides interpolation support            |
 
 We support a reasonable list of operating systems and versions.
 - Our main target is Linux (mainly Ubuntu or comparable Linux distributions).
diff --git a/build/build-publish-solvers/solver-yices.xml b/build/build-publish-solvers/solver-yices.xml
index 55bdf88f0b..2500d7c5af 100644
--- a/build/build-publish-solvers/solver-yices.xml
+++ b/build/build-publish-solvers/solver-yices.xml
@@ -50,6 +50,13 @@ SPDX-License-Identifier: Apache-2.0
         <condition property="yices-java.installed">
             <available file="${yices2.buildDir}/yices2_java_bindings/dist/lib" type="dir"/>
         </condition>
+
+        <condition property="build.architecture" value="arm64" else="x64">
+            <os arch="aarch64"/>
+        </condition>
+        <condition property="build.homebrew" value="/opt/homebrew" else="/usr/local">
+            <os arch="aarch64"/>
+        </condition>
     </target>
 
     <target name="download-cudd" depends="build-initialize" unless="cudd.downloaded">
@@ -89,6 +96,23 @@ SPDX-License-Identifier: Apache-2.0
             <arg value="clean"/>
         </exec>
     </target>
+    <target name="build-cudd-macOS" depends="download-cudd" unless="cudd.installed">
+        <exec executable="aclocal" dir="${yices2.buildDir}/cudd" failonerror="true"/>
+        <exec executable="autoconf" dir="${yices2.buildDir}/cudd" failonerror="true"/>
+        <exec executable="automake" dir="${yices2.buildDir}/cudd" failonerror="true"/>
+        <!-- macOS build -->
+        <exec executable="./configure" dir="${yices2.buildDir}/cudd" failonerror="true">
+            <env key="CFLAGS" value="-fPIC"/>
+            <arg value="--prefix=${yices2.buildDir}/cudd/install/${build.architecture}-macos"/>
+        </exec>
+        <exec executable="make" dir="${yices2.buildDir}/cudd" failonerror="true">
+            <arg value="-j"/>
+            <arg value="install"/>
+        </exec>
+        <exec executable="make" dir="${yices2.buildDir}/cudd" failonerror="true">
+            <arg value="clean"/>
+        </exec>
+    </target>
 
     <target name="download-libpoly" depends="build-initialize" unless="libpoly.downloaded">
         <exec executable="git" dir="${yices2.buildDir}" failonerror="true">
@@ -129,6 +153,23 @@ SPDX-License-Identifier: Apache-2.0
         </exec>
         <delete dir="${yices2.buildDir}/libpoly/build"/>
     </target>
+    <target name="build-libpoly-macOS" depends="download-libpoly" unless="libpoly.installed">
+        <!-- macOS build -->
+        <mkdir dir="${yices2.buildDir}/libpoly/build"/>
+        <exec executable="cmake" dir="${yices2.buildDir}/libpoly/build" failonerror="true">
+            <arg value=".."/>
+            <arg value="-DCMAKE_BUILD_TYPE=Release"/>
+            <arg value="-DCMAKE_INSTALL_PREFIX=${yices2.buildDir}/libpoly/install/${build.architecture}-macos"/>
+            <arg value="-DGMP_INCLUDE_DIR=${build.homebrew}/include"/>
+            <arg value="-DGMP_LIBRARY=${build.homebrew}/lib/libgmp.a"/>
+            <arg value="-DLIBPOLY_BUILD_PYTHON_API=OFF"/>
+        </exec>
+        <exec executable="make" dir="${yices2.buildDir}/libpoly/build" failonerror="true">
+            <arg value="-j"/>
+            <arg value="install"/>
+        </exec>
+        <delete dir="${yices2.buildDir}/libpoly/build"/>
+    </target>
 
     <target name="download-yices2" depends="build-initialize" unless="yices.downloaded">
         <exec executable="git" dir="${yices2.buildDir}" failonerror="true">
@@ -183,6 +224,33 @@ SPDX-License-Identifier: Apache-2.0
             <arg value="OPTION=mingw32"/>
         </exec>
     </target>
+    <target name="build-yices2-macOS"
+            depends="build-cudd-macOS, build-libpoly-macOS, download-yices2" unless="yices.installed">
+        <exec executable="git" dir="${yices2.buildDir}/yices2" failonerror="true">
+            <arg value="apply"/>
+            <arg value="${basedir}/lib/native/source/yices2/yices.patch"/>
+        </exec>
+        <exec executable="autoconf" dir="${yices2.buildDir}/yices2" failonerror="true"/>
+        <delete file="${yices2.buildDir}/yices2/INSTALL"/>
+        <mkdir dir="${yices2.buildDir}/yices2/install"/>
+        <!-- macOS build -->
+        <exec executable="./configure" dir="${yices2.buildDir}/yices2" failonerror="true">
+            <env key="LDFLAGS" value="-L${build.homebrew}/lib -L${yices2.buildDir}/libpoly/install/${build.architecture}-macos/lib -L${yices2.buildDir}/cudd/install/${build.architecture}-macos/lib"/>
+            <env key="CFLAGS" value="-I${build.homebrew}/include -I${yices2.buildDir}/libpoly/install/${build.architecture}-macos/include -I${yices2.buildDir}/cudd/install/${build.architecture}-macos/include"/>
+            <arg value="--enable-mcsat"/>
+            <arg value="--enable-thread-safety"/>
+            <arg value="--prefix=${yices2.buildDir}/yices2/install/${build.architecture}-macos"/>
+        </exec>
+        <exec executable="make" dir="${yices2.buildDir}/yices2" failonerror="true">
+            <arg value="-j"/>
+        </exec>
+        <exec executable="make" dir="${yices2.buildDir}/yices2" failonerror="true">
+            <arg value="install"/>
+        </exec>
+        <exec executable="make" dir="${yices2.buildDir}/yices2" failonerror="true">
+            <arg value="clean"/>
+        </exec>
+    </target>
     <target name="clean-yices2" depends="build-initialize, clean-yices2-java" if="yices.installed">
         <delete dir="${yices2.buildDir}/yices2/install"/>
         <exec executable="git" dir="${yices2.buildDir}/yices2" failonerror="true">
@@ -235,6 +303,25 @@ SPDX-License-Identifier: Apache-2.0
             <arg value="install"/>
         </exec>
     </target>
+    <target name="build-yices2-java-macOS"
+            depends="build-yices2-macOS, download-yices2-java"
+            unless="yices-java.installed">
+        <exec executable="git" dir="${yices2.buildDir}/yices2_java_bindings" failonerror="true">
+            <arg value="apply"/>
+            <arg value="${basedir}/lib/native/source/yices2/jni.patch"/>
+        </exec>
+        <mkdir dir="${yices2.buildDir}/yices2_java_bindings/dist/lib"/>
+        <!-- macOS build -->
+        <exec executable="ant" dir="${yices2.buildDir}/yices2_java_bindings" failonerror="true">
+            <env key="OS" value="darwin"/>
+            <env key="JNI_PATH" value="${java.home}/include"/>
+            <env key="GMP_PATH" value="${build.homebrew}"/>
+            <env key="CUDD_PATH" value="${yices2.buildDir}/cudd/install/${build.architecture}-macos"/>
+            <env key="POLY_PATH" value="${yices2.buildDir}/libpoly/install/${build.architecture}-macos"/>
+            <env key="YICES_PATH" value="${yices2.buildDir}/yices2/install/${build.architecture}-macos"/>
+            <arg value="install"/>
+        </exec>
+    </target>
     <target name="clean-yices2-java" depends="build-initialize" if="yices-java.installed">
         <exec executable="ant" dir="${yices2.buildDir}/yices2_java_bindings" failonerror="true">
             <arg value="clean"/>
@@ -246,6 +333,15 @@ SPDX-License-Identifier: Apache-2.0
         </exec>
     </target>
 
+    <target name="publish-yices2-macOS" depends="load-ivy, build-yices2-java-macOS"
+            description="Compile Yices2 binaries for macOS">
+        <condition property="install.architecture" value="arm64" else="x86_64">
+            <os arch="aarch64"/>
+        </condition>
+        <mkdir dir="lib/native/${build.architecture}-macosx"/>
+        <copy file="${yices2.buildDir}/yices2_java_bindings/dist/lib/libyices2java.dylib" tofile="lib/native/${install.architecture}-macosx/libyices2java.dylib" failonerror="true"/>
+    </target>
+
     <target name="publish-yices2" depends="load-ivy, build-yices2-java"
         description="Publish Yices2 binaries to Ivy repo.">
         <sequential>
diff --git a/doc/How-to-build-for-macOS.md b/doc/How-to-build-for-macOS.md
new file mode 100644
index 0000000000..9ae95b20f6
--- /dev/null
+++ b/doc/How-to-build-for-macOS.md
@@ -0,0 +1,43 @@
+<!--
+This file is part of JavaSMT,
+an API wrapper for a collection of SMT solvers:
+https://github.com/sosy-lab/java-smt
+
+SPDX-FileCopyrightText: 2021 Dirk Beyer <https://www.sosy-lab.org>
+
+SPDX-License-Identifier: Apache-2.0
+-->
+
+# Building solver binaries for macOS
+
+We currently can't provide binaries for all supported solvers on macOS. However, it's often
+possible to build the necessary binaries from source, and we try to include a simple build
+script wherever possible
+
+## Yices
+
+To build the Yices binaries, we first need some build dependencies and GMP, which can all be
+installed via Homebrew:
+
+```shell
+brew update
+brew install gperf lcov autoconf automake libtool
+brew install gmp
+```
+
+Then, we build the Yices2 binaries by running the build script included with JavaSMT:
+
+```shell
+git clone git@github.com:sosy-lab/java-smt.git
+cd java-smt
+ant publish-yices2-macOS
+```
+
+The script will build several dependencies before compiling Yices and may run for up to 10
+minutes. Once it's finished the binary `libyices2java.dylib` can be found under `lib/native`.
+Depending on your system architecture, it will be either in the `arm64-macos` (ARM) or
+`x64_64-macos` (Intel) folder
+
+You can then either copy the binary to your project folder, or
+set `DYLD_LIBRARY_PATH` to include the binary folder to make sure Yices will be found when
+running JavaSMT
\ No newline at end of file
diff --git a/lib/native/source/yices2/jni.patch b/lib/native/source/yices2/jni.patch
index 6e1338ac6c..9acfd6e406 100644
--- a/lib/native/source/yices2/jni.patch
+++ b/lib/native/source/yices2/jni.patch
@@ -52,9 +52,13 @@ diff --git a/src/main/java/com/sri/yices/Makefile b/src/main/java/com/sri/yices/
 +LIBS := -lyices -lcudd -lpoly -lgmpxx -lgmp
  
  CXX ?= g++
- 
-@@ -86,7 +94,10 @@
- 	$(CXX) $(CPPFLAGS) $(CXXFLAGS) -dynamiclib -o $@ yicesJNI.o $(LIBS)
+
+@@ -83,10 +91,13 @@
+ 	$(CXX) $(CPPFLAGS) $(CXXFLAGS) -Wall -c yicesJNI.cpp
+
+ libyices2java.dylib: yicesJNI.o
+-	$(CXX) $(CPPFLAGS) $(CXXFLAGS) -dynamiclib -o $@ yicesJNI.o $(LIBS)
++	$(CXX) $(CFLAGS) $(LDFLAGS) -o $@ yicesJNI.o -dynamiclib $(YICES_PATH)/lib/libyices.a $(CUDD_PATH)/lib/libcudd.a $(POLY_PATH)/lib/libpoly.a $(GMP_PATH)/lib/libgmpxx.a $(GMP_PATH)/lib/libgmp.a -lc -lm
  
  libyices2java.so: yicesJNI.o
 -	$(CXX) $(CFLAGS) $(LDFLAGS) -shared -o $@ yicesJNI.o $(LIBS)