diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 18a0debe9..d322b3acc 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -46,7 +46,7 @@ jobs:
     strategy:
       matrix:
         jdk: [ 11, 17, 21 ]
-        os: [ ubuntu-latest, windows-latest, macos-13 ]
+        os: [ ubuntu-latest, windows-latest, macos-13, macos-latest ]
     runs-on: ${{ matrix.os }}
     steps:
       - name: Checkout
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 787ba297a..20ce03475 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -6,6 +6,11 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 
 [Full changelog](https://github.com/LearnLib/automatalib/compare/automatalib-0.12.1...HEAD)
 
+### Added
+
+* `automata-modelchecking-m3c` now supports ARM-based macOS systems.
+* `automata-modelchecking-m3c` can now be included in jlink images.
+
 ### Changed
 
 * AutomataLib now requires Java 11 at runtime.
diff --git a/distribution/src/it/jlink/pom.xml b/distribution/src/it/jlink/pom.xml
index e863a8cf9..012910343 100644
--- a/distribution/src/it/jlink/pom.xml
+++ b/distribution/src/it/jlink/pom.xml
@@ -39,10 +39,6 @@ limitations under the License.
                     <groupId>net.automatalib</groupId>
                     <artifactId>automata-brics</artifactId>
                 </exclusion>
-                <exclusion>
-                    <groupId>net.automatalib</groupId>
-                    <artifactId>automata-modelchecking-m3c</artifactId>
-                </exclusion>
                 <exclusion>
                     <groupId>net.automatalib</groupId>
                     <artifactId>automata-jung-visualizer</artifactId>
diff --git a/modelchecking/m3c/src/test/java/net/automatalib/modelchecker/m3c/solver/SolverHistoryADDTest.java b/modelchecking/m3c/src/test/java/net/automatalib/modelchecker/m3c/solver/SolverHistoryADDTest.java
index 76e8e62af..1dad4ea7a 100644
--- a/modelchecking/m3c/src/test/java/net/automatalib/modelchecker/m3c/solver/SolverHistoryADDTest.java
+++ b/modelchecking/m3c/src/test/java/net/automatalib/modelchecker/m3c/solver/SolverHistoryADDTest.java
@@ -27,7 +27,6 @@
 import net.automatalib.modelchecker.m3c.transformer.ADDTransformer;
 import net.automatalib.modelchecker.m3c.transformer.ADDTransformerSerializer;
 import org.testng.Assert;
-import org.testng.SkipException;
 
 public class SolverHistoryADDTest extends AbstractSolverHistoryTest<ADDTransformer<String, String>> {
 
@@ -50,12 +49,6 @@ public AbstractDDSolver<ADDTransformer<String, String>, String, String> getSolve
         return new ADDSolver<>(cfmps);
     }
 
-    @Override
-    public void testSolverHistory() {
-        // TODO this test may fail due to a bug in ADDLib. Remove this method once we bump the dependency
-        throw new SkipException("");
-    }
-
     @Override
     public <N> void testInitialPropertyTransformers(SolverData<N, ADDTransformer<String, String>, String, String> data,
                                                     N s1,
diff --git a/pom.xml b/pom.xml
index 533d3ef89..339a94462 100644
--- a/pom.xml
+++ b/pom.xml
@@ -222,7 +222,7 @@ limitations under the License.
         <tidy-pom.version>1.3.0</tidy-pom.version>
 
         <!-- dependency versions -->
-        <addlib.version>3.1.0</addlib.version>
+        <addlib.version>4.0.0</addlib.version>
         <assertj.version>3.17.1</assertj.version>
         <brics-automaton.version>1.12-4</brics-automaton.version>
         <build-tools.version>0.1.1</build-tools.version>