diff --git a/src/org/sosy_lab/common/collect/AbstractImmutableSortedUnionFind.java b/src/org/sosy_lab/common/collect/AbstractImmutableSortedUnionFind.java
new file mode 100644
index 000000000..4a010aa79
--- /dev/null
+++ b/src/org/sosy_lab/common/collect/AbstractImmutableSortedUnionFind.java
@@ -0,0 +1,25 @@
+// This file is part of SoSy-Lab Common,
+// a library of useful utilities:
+// https://github.com/sosy-lab/java-common-lib
+//
+// SPDX-FileCopyrightText: 2026 Dirk Beyer <https://www.sosy-lab.org>
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.sosy_lab.common.collect;
+
+import com.google.errorprone.annotations.DoNotCall;
+
+public abstract class AbstractImmutableSortedUnionFind<T extends Comparable<T>>
+    implements SortedUnionFind<T> {
+  /**
+   * @throws UnsupportedOperationException Always.
+   * @deprecated Unsupported operation.
+   */
+  @Deprecated
+  @Override
+  @DoNotCall
+  public final void union(T e1, T e2) {
+    throw new UnsupportedOperationException();
+  }
+}
diff --git a/src/org/sosy_lab/common/collect/AbstractImmutableUnionFind.java b/src/org/sosy_lab/common/collect/AbstractImmutableUnionFind.java
new file mode 100644
index 000000000..d1fd7db87
--- /dev/null
+++ b/src/org/sosy_lab/common/collect/AbstractImmutableUnionFind.java
@@ -0,0 +1,24 @@
+// This file is part of SoSy-Lab Common,
+// a library of useful utilities:
+// https://github.com/sosy-lab/java-common-lib
+//
+// SPDX-FileCopyrightText: 2026 Dirk Beyer <https://www.sosy-lab.org>
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.sosy_lab.common.collect;
+
+import com.google.errorprone.annotations.DoNotCall;
+
+public abstract class AbstractImmutableUnionFind<T> implements UnionFind<T> {
+  /**
+   * @throws UnsupportedOperationException Always.
+   * @deprecated Unsupported operation.
+   */
+  @Deprecated
+  @Override
+  @DoNotCall
+  public final void union(T e1, T e2) {
+    throw new UnsupportedOperationException();
+  }
+}
diff --git a/src/org/sosy_lab/common/collect/PackageSanityTest.java b/src/org/sosy_lab/common/collect/PackageSanityTest.java
index d349efcf9..4d6ad7dfc 100644
--- a/src/org/sosy_lab/common/collect/PackageSanityTest.java
+++ b/src/org/sosy_lab/common/collect/PackageSanityTest.java
@@ -9,6 +9,8 @@
 package org.sosy_lab.common.collect;
 
 import com.google.common.testing.AbstractPackageSanityTests;
+import java.lang.reflect.Constructor;
+import java.lang.reflect.Method;
 import org.sosy_lab.common.Classes;
 
 public class PackageSanityTest extends AbstractPackageSanityTests {
@@ -24,4 +26,19 @@ public class PackageSanityTest extends AbstractPackageSanityTests {
         OurSortedMap.class, OurSortedMap.EmptyImmutableOurSortedMap.of(), singletonMap);
     ignoreClasses(Classes.IS_GENERATED);
   }
+
+  {
+    setDefault(SortedTreeSetUnionFind.class, new SortedTreeSetUnionFind<>());
+    // ignoreClasses(Classes.IS_GENERATED);
+
+    try {
+      setDefault(Constructor.class, PackageSanityTest.class.getConstructor());
+      setDefault(Method.class, PackageSanityTest.class.getDeclaredMethod("defaultMethod"));
+    } catch (NoSuchMethodException e) {
+      throw new AssertionError(e);
+    }
+  }
+
+  @SuppressWarnings("unused")
+  private static void defaultMethod() {}
 }
diff --git a/src/org/sosy_lab/common/collect/PersistentSortedUnionFind.java b/src/org/sosy_lab/common/collect/PersistentSortedUnionFind.java
new file mode 100644
index 000000000..738fabd12
--- /dev/null
+++ b/src/org/sosy_lab/common/collect/PersistentSortedUnionFind.java
@@ -0,0 +1,48 @@
+// This file is part of SoSy-Lab Common,
+// a library of useful utilities:
+// https://github.com/sosy-lab/java-common-lib
+//
+// SPDX-FileCopyrightText: 2026 Dirk Beyer <https://www.sosy-lab.org>
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.sosy_lab.common.collect;
+
+import com.google.errorprone.annotations.CheckReturnValue;
+import com.google.errorprone.annotations.DoNotCall;
+import com.google.errorprone.annotations.Immutable;
+import java.util.Map;
+import java.util.NavigableSet;
+
+/**
+ * Interface for a persistent and sorted union-find. A persistent data structure is immutable, but
+ * provides cheap copy-and-write operations. Thus, all write operations ({@link #union(Comparable,
+ * Comparable)}) will not modify the current instance, but return a new instance instead.
+ *
+ * <p>All modifying operations inherited from {@link SortedUnionFind} are not supported and will
+ * always throw {@link UnsupportedOperationException}.
+ *
+ * @param <T> The type of values.
+ */
+@Immutable(containerOf = "T")
+public interface PersistentSortedUnionFind<T extends Comparable<T>> extends SortedUnionFind<T> {
+
+  /**
+   * Replacement for {@link #union(Comparable, Comparable)} that returns a fresh new instance.
+   *
+   * @param e1 first element
+   * @param e2 second element
+   * @return new instance that the desired changes have been applied to
+   */
+  @CheckReturnValue
+  Map<T, NavigableSet<T>> unionAndCopy(T e1, T e2);
+
+  /**
+   * @throws UnsupportedOperationException Always.
+   * @deprecated Unsupported operation.
+   */
+  @Deprecated
+  @Override
+  @DoNotCall
+  void union(T e1, T e2);
+}
diff --git a/src/org/sosy_lab/common/collect/PersistentUnionFind.java b/src/org/sosy_lab/common/collect/PersistentUnionFind.java
new file mode 100644
index 000000000..f6b0fba2b
--- /dev/null
+++ b/src/org/sosy_lab/common/collect/PersistentUnionFind.java
@@ -0,0 +1,48 @@
+// This file is part of SoSy-Lab Common,
+// a library of useful utilities:
+// https://github.com/sosy-lab/java-common-lib
+//
+// SPDX-FileCopyrightText: 2026 Dirk Beyer <https://www.sosy-lab.org>
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.sosy_lab.common.collect;
+
+import com.google.errorprone.annotations.CheckReturnValue;
+import com.google.errorprone.annotations.DoNotCall;
+import com.google.errorprone.annotations.Immutable;
+import java.util.Map;
+import java.util.NavigableSet;
+
+/**
+ * Interface for a persistent union-find. A persistent data structure is immutable, but provides
+ * cheap copy-and-write operations. Thus, all write operations ({@link #union(Object, Object)}) will
+ * not modify the current instance, but return a new instance instead.
+ *
+ * <p>All modifying operations inherited from {@link UnionFind} are not supported and will always
+ * throw {@link UnsupportedOperationException}.
+ *
+ * @param <T> The type of values.
+ */
+@Immutable(containerOf = "T")
+public interface PersistentUnionFind<T> extends UnionFind<T> {
+
+  /**
+   * Replacement for {@link #union(Object, Object)} that returns a fresh new instance.
+   *
+   * @param e1 first element
+   * @param e2 second element
+   * @return new instance that the desired changes have been applied to
+   */
+  @CheckReturnValue
+  Map<T, NavigableSet<T>> unionAndCopy(T e1, T e2);
+
+  /**
+   * @throws UnsupportedOperationException Always.
+   * @deprecated Unsupported operation.
+   */
+  @Deprecated
+  @Override
+  @DoNotCall
+  void union(T e1, T e2);
+}
diff --git a/src/org/sosy_lab/common/collect/SortedTreeSetUnionFind.java b/src/org/sosy_lab/common/collect/SortedTreeSetUnionFind.java
new file mode 100644
index 000000000..13cf4380e
--- /dev/null
+++ b/src/org/sosy_lab/common/collect/SortedTreeSetUnionFind.java
@@ -0,0 +1,179 @@
+// This file is part of SoSy-Lab Common,
+// a library of useful utilities:
+// https://github.com/sosy-lab/java-common-lib
+//
+// SPDX-FileCopyrightText: 2026 Dirk Beyer <https://www.sosy-lab.org>
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.sosy_lab.common.collect;
+
+import com.google.common.base.Preconditions;
+import com.google.errorprone.annotations.Var;
+import java.util.Collection;
+import java.util.HashMap;
+import java.util.Map;
+import java.util.NavigableSet;
+import java.util.Set;
+import java.util.TreeSet;
+
+/**
+ * An implementation of {@link SortedUnionFind} using a {@link HashMap} of {@link TreeSet}s. In
+ * order to represent subsets by canonical elements, each one is mapped to its representative
+ * canonical element. This is always the first element added to the subset, unless it has changed
+ * due to union operations. The union is implemented as union by size.
+ *
+ * @param <T> type of elements added to the Union-Find. Must be {@link Comparable} to ensure correct
+ *     ordering.
+ */
+public class SortedTreeSetUnionFind<T extends Comparable<T>> implements SortedUnionFind<T> {
+
+  private final Map<T, NavigableSet<T>> setOfSets;
+
+  /** Generates an empty {@link SortedTreeSetUnionFind}. */
+  public SortedTreeSetUnionFind() {
+    setOfSets = new HashMap<>();
+  }
+
+  /**
+   * Returns the canonical element of the set containing the provided element.
+   *
+   * @param e element for which set is to be found
+   * @return canonical element of the found set
+   * @throws IllegalArgumentException if element is not contained in any subset
+   */
+  @Override
+  public T find(T e) {
+
+    Preconditions.checkNotNull(e);
+    for (NavigableSet<T> current : setOfSets.values()) {
+      if (current.contains(e)) {
+        for (T element : current) {
+          if (setOfSets.containsKey(element)) {
+            return element;
+          }
+        }
+      }
+    }
+
+    throw new IllegalArgumentException("Element not contained");
+  }
+
+  /**
+   * Merges the sets represented by the two input values according to standard Union-Find behaviour.
+   *
+   * <p>USES: Add new element as new set: pass it as both e1 and e2. Add new element to existing
+   * set: one input value is the new element, the other the canonical element of the set to be added
+   * to. Merge two existing sets: e1, e2 canonical elements of sets to be merged.
+   *
+   * @param e1 first element
+   * @param e2 second element
+   */
+  @Override
+  public void union(T e1, T e2) {
+
+    Preconditions.checkNotNull(e1);
+    Preconditions.checkNotNull(e2);
+
+    if (e1.equals(e2)) {
+      addElementAsNewSet(e1);
+    } else {
+      Set<T> canonicalElements = setOfSets.keySet();
+
+      if (canonicalElements.contains(e1)) {
+        if (canonicalElements.contains(e2)) {
+          mergeExistingSets(e1, e2);
+        } else {
+          addElementToExistingSet(e2, e1);
+        }
+      } else if (canonicalElements.contains(e2)) {
+        addElementToExistingSet(e1, e2);
+      } else {
+        addElementAsNewSet(e1);
+        addElementToExistingSet(e2, e1);
+      }
+    }
+  }
+
+  private void addElementAsNewSet(T e) {
+
+    if (!contains(e)) {
+      NavigableSet<T> newSet = new TreeSet<>();
+      newSet.add(e);
+      setOfSets.put(e, newSet);
+    }
+  }
+
+  private void addElementToExistingSet(T e, T canon) {
+
+    if (!contains(e)) {
+      for (NavigableSet<T> currentSet : setOfSets.values()) {
+        if (currentSet.contains(canon)) {
+          currentSet.add(e);
+          setOfSets.replace(canon, currentSet);
+          break;
+        }
+      }
+    } else {
+      mergeExistingSets(e, canon);
+    }
+  }
+
+  private void mergeExistingSets(T e1, T e2) {
+
+    @Var NavigableSet<T> set1 = null;
+    @Var NavigableSet<T> set2 = null;
+
+    for (NavigableSet<T> current : setOfSets.values()) {
+      if (current.contains(e1)) {
+        set1 = current;
+      } else if (current.contains(e2)) {
+        set2 = current;
+      }
+    }
+
+    assert set1 != null;
+    assert set2 != null;
+
+    int size1 = set1.size();
+    int size2 = set2.size();
+
+    if (size1 > size2) {
+      set1.addAll(set2);
+      setOfSets.remove(e2);
+    } else {
+      set2.addAll(set1);
+      setOfSets.remove(e1);
+    }
+  }
+
+  /**
+   * Provides a {@link Collection} containing all current subsets.
+   *
+   * @return {@link Collection} containing all current subsets
+   */
+  @Override
+  public Collection<? extends Set<T>> getAllSubsets() {
+    return setOfSets.values();
+  }
+
+  /**
+   * Checks whether the provided element is contained in any current subset and returns true or
+   * false accordingly.
+   *
+   * @param e element to be searched for
+   * @return true if contained, false if not
+   */
+  @Override
+  public boolean contains(T e) {
+
+    Preconditions.checkNotNull(e);
+
+    for (NavigableSet<T> current : setOfSets.values()) {
+      if (current.contains(e)) {
+        return true;
+      }
+    }
+    return false;
+  }
+}
diff --git a/src/org/sosy_lab/common/collect/SortedUnionFind.java b/src/org/sosy_lab/common/collect/SortedUnionFind.java
new file mode 100644
index 000000000..818e91cc0
--- /dev/null
+++ b/src/org/sosy_lab/common/collect/SortedUnionFind.java
@@ -0,0 +1,53 @@
+// This file is part of SoSy-Lab Common,
+// a library of useful utilities:
+// https://github.com/sosy-lab/java-common-lib
+//
+// SPDX-FileCopyrightText: 2026 Dirk Beyer <https://www.sosy-lab.org>
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.sosy_lab.common.collect;
+
+import java.util.Collection;
+import java.util.Set;
+
+/**
+ * Interface for a sorted Union-Find or Disjoint-Set data structure. Uses a {@link Collection} of
+ * {@link Set}s.
+ *
+ * @param <T> type of elements added to the Union-Find. Must be {@link Comparable} to ensure correct
+ *     ordering.
+ */
+public interface SortedUnionFind<T extends Comparable<T>> {
+  /**
+   * Returns the canonical element of the set containing the provided element.
+   *
+   * @param e element for which set is to be found
+   * @return canonical element of the found set
+   */
+  T find(T e);
+
+  /**
+   * Merges the sets represented by the two input values according to standard Union-Find behaviour.
+   *
+   * @param e1 first element
+   * @param e2 second element
+   */
+  void union(T e1, T e2);
+
+  /**
+   * Provides a {@link Collection} containing all current subsets.
+   *
+   * @return {@link Collection} containing all current subsets
+   */
+  Collection<? extends Set<T>> getAllSubsets();
+
+  /**
+   * Checks whether the provided element is contained in any current subset and returns true or
+   * false accordingly.
+   *
+   * @param e element to be searched for
+   * @return true if contained, false if not
+   */
+  boolean contains(T e);
+}
diff --git a/src/org/sosy_lab/common/collect/SortedUnionFindTest.java b/src/org/sosy_lab/common/collect/SortedUnionFindTest.java
new file mode 100644
index 000000000..5e0aae8e3
--- /dev/null
+++ b/src/org/sosy_lab/common/collect/SortedUnionFindTest.java
@@ -0,0 +1,103 @@
+// This file is part of SoSy-Lab Common,
+// a library of useful utilities:
+// https://github.com/sosy-lab/java-common-lib
+//
+// SPDX-FileCopyrightText: 2026 Dirk Beyer <https://www.sosy-lab.org>
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.sosy_lab.common.collect;
+
+import static com.google.common.truth.Truth.assertThat;
+
+import com.google.common.collect.Range;
+import com.google.errorprone.annotations.Var;
+import org.junit.BeforeClass;
+import org.junit.Test;
+
+public class SortedUnionFindTest {
+
+  static final Range<Integer> LOW_NUMS = Range.closed(0, 4);
+  static final Range<Integer> HIGH_NUMS = Range.closed(5, 9);
+
+  static SortedUnionFind<Integer> unionFind = new SortedTreeSetUnionFind<>();
+
+  @BeforeClass
+  public static void setup() {
+    unionFind = new SortedTreeSetUnionFind<>();
+
+    for (int i = 0; i <= 4; i++) {
+      unionFind.union(0, i);
+    }
+    for (int i = 5; i <= 9; i++) {
+      unionFind.union(5, i);
+    }
+  }
+
+  @Test
+  public void testFind_ElementNotContained() {
+    assertThat(LOW_NUMS.contains(unionFind.find(8))).isFalse();
+    assertThat(HIGH_NUMS.contains(unionFind.find(2))).isFalse();
+  }
+
+  @Test
+  public void testFind_ElementContained() {
+    assertThat(LOW_NUMS.contains(unionFind.find(2))).isTrue();
+    assertThat(HIGH_NUMS.contains(unionFind.find(8))).isTrue();
+  }
+
+  @Test
+  public void testUnion_CorrectCanonicalElementAndCorrectSubsetAfterUnionBySize() {
+    assertThat(unionFind.getAllSubsets().size() == 2).isTrue();
+
+    for (int i = 0; i <= 4; i++) {
+      assertThat(unionFind.find(i).equals(0)).isTrue();
+    }
+    for (int i = 5; i <= 9; i++) {
+      assertThat(unionFind.find(i).equals(5)).isTrue();
+    }
+  }
+
+  @Test
+  public void testUnion_MergeExistingSubsets() {
+    unionFind.union(0, 5);
+
+    assertThat(unionFind.getAllSubsets().size() == 1).isTrue();
+
+    @Var boolean canonUnknown = true;
+    @Var Integer canon = null;
+
+    for (int i = 0; i <= 9; i++) {
+      if (canonUnknown) {
+        canon = unionFind.find(i);
+        canonUnknown = false;
+      }
+      assertThat(unionFind.find(i).equals(canon)).isTrue();
+    }
+  }
+
+  @Test
+  public void testUnion_ConstantCanonicalElementDuringNonlinearInsertion() {
+    SortedUnionFind<Integer> newUnionFind = new SortedTreeSetUnionFind<>();
+
+    newUnionFind.union(3, 3);
+    newUnionFind.union(3, 2);
+    newUnionFind.union(3, 5);
+    newUnionFind.union(3, 1);
+    newUnionFind.union(3, 8);
+    newUnionFind.union(3, 6);
+    newUnionFind.union(3, 9);
+    newUnionFind.union(3, 7);
+    newUnionFind.union(3, 4);
+
+    assertThat(newUnionFind.find(3)).isEqualTo(3);
+    assertThat(newUnionFind.find(2)).isEqualTo(3);
+    assertThat(newUnionFind.find(5)).isEqualTo(3);
+    assertThat(newUnionFind.find(1)).isEqualTo(3);
+    assertThat(newUnionFind.find(8)).isEqualTo(3);
+    assertThat(newUnionFind.find(6)).isEqualTo(3);
+    assertThat(newUnionFind.find(9)).isEqualTo(3);
+    assertThat(newUnionFind.find(7)).isEqualTo(3);
+    assertThat(newUnionFind.find(4)).isEqualTo(3);
+  }
+}
diff --git a/src/org/sosy_lab/common/collect/UnionFind.java b/src/org/sosy_lab/common/collect/UnionFind.java
new file mode 100644
index 000000000..73220f5f8
--- /dev/null
+++ b/src/org/sosy_lab/common/collect/UnionFind.java
@@ -0,0 +1,52 @@
+// This file is part of SoSy-Lab Common,
+// a library of useful utilities:
+// https://github.com/sosy-lab/java-common-lib
+//
+// SPDX-FileCopyrightText: 2026 Dirk Beyer <https://www.sosy-lab.org>
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.sosy_lab.common.collect;
+
+import java.util.Collection;
+import java.util.Set;
+
+/**
+ * Interface for a sorted Union-Find or Disjoint-Set data structure. Uses a {@link Collection} of
+ * {@link Set}s.
+ *
+ * @param <T> type of elements added to the Union-Find.
+ */
+public interface UnionFind<T> {
+  /**
+   * Returns the canonical element of the set containing the provided element.
+   *
+   * @param e element for which set is to be found
+   * @return canonical element of the found set
+   */
+  T find(T e);
+
+  /**
+   * Merges the sets represented by the two input values according to standard Union-Find behaviour.
+   *
+   * @param e1 first element
+   * @param e2 second element
+   */
+  void union(T e1, T e2);
+
+  /**
+   * Provides a {@link Collection} containing all current subsets.
+   *
+   * @return {@link Collection} containing all current subsets
+   */
+  Collection<? extends Set<T>> getAllSubsets();
+
+  /**
+   * Checks whether the provided element is contained in any current subset and returns true or
+   * false accordingly.
+   *
+   * @param e element to be searched for
+   * @return true if contained, false if not
+   */
+  boolean contains(T e);
+}