diff --git a/src/org/sosy_lab/java_smt/api/FormulaManager.java b/src/org/sosy_lab/java_smt/api/FormulaManager.java
index 1dcefec063..b52a82300f 100644
--- a/src/org/sosy_lab/java_smt/api/FormulaManager.java
+++ b/src/org/sosy_lab/java_smt/api/FormulaManager.java
@@ -8,8 +8,10 @@
 
 package org.sosy_lab.java_smt.api;
 
+import com.google.common.collect.ImmutableList;
 import com.google.common.collect.ImmutableMap;
 import com.google.errorprone.annotations.CanIgnoreReturnValue;
+import java.util.Collection;
 import java.util.List;
 import java.util.Map;
 import org.sosy_lab.common.Appender;
@@ -131,6 +133,46 @@ <T extends Formula> T makeApplication(
    */
   <T extends Formula> T makeApplication(FunctionDeclaration<T> declaration, Formula... args);
 
+  /**
+   * Create an equality formula between the given arguments. We return "true" if all arguments are
+   * equal, even if there are less than two arguments.
+   *
+   * @param pArgs Arguments to be compared for equality, ordering does not matter.
+   * @return Equality formula
+   */
+  default BooleanFormula equal(Formula... pArgs) {
+    return equal(ImmutableList.copyOf(pArgs));
+  }
+
+  /**
+   * Create an equality formula between the given arguments. We return "true" if all arguments are
+   * equal, even if there are less than two arguments.
+   *
+   * @param pArgs Arguments to be compared for equality, ordering does not matter.
+   * @return Equality formula
+   */
+  BooleanFormula equal(Collection<Formula> pArgs);
+
+  /**
+   * Create a distinctness formula between the given arguments. We return "true" if all arguments
+   * are pairwise distinct, even if there are less than two arguments.
+   *
+   * @param pArgs Arguments to be compared for distinctness, ordering does not matter.
+   * @return Distinctness formula
+   */
+  default BooleanFormula distinct(Formula... pArgs) {
+    return distinct(ImmutableList.copyOf(pArgs));
+  }
+
+  /**
+   * Create a distinctness formula between the given arguments. We return "true" if all arguments
+   * are pairwise distinct, even if there are less than two arguments.
+   *
+   * @param pArgs Arguments to be compared for distinctness, ordering does not matter.
+   * @return Distinctness formula
+   */
+  BooleanFormula distinct(Collection<Formula> pArgs);
+
   /** Returns the type of the given Formula. */
   <T extends Formula> FormulaType<T> getFormulaType(T formula);
 
diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java
index d9c3f691f6..ca21bb8134 100644
--- a/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java
+++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java
@@ -14,12 +14,15 @@
 import com.google.common.annotations.VisibleForTesting;
 import com.google.common.base.CharMatcher;
 import com.google.common.base.Preconditions;
+import com.google.common.collect.Collections2;
 import com.google.common.collect.ImmutableBiMap;
 import com.google.common.collect.ImmutableList;
 import com.google.common.collect.ImmutableMap;
 import com.google.common.collect.ImmutableSet;
 import com.google.common.collect.Iterables;
 import java.io.IOException;
+import java.util.ArrayList;
+import java.util.Collection;
 import java.util.List;
 import java.util.Map;
 import org.checkerframework.checker.nullness.qual.Nullable;
@@ -264,6 +267,88 @@ public EnumerationFormulaManager getEnumerationFormulaManager() {
     return enumManager;
   }
 
+  /** Override if the solver API only supports binary equality. */
+  protected TFormulaInfo equalImpl(TFormulaInfo pArg1, TFormulaInfo pArgs) {
+    return equalImpl(ImmutableList.of(pArg1, pArgs));
+  }
+
+  @Override
+  public BooleanFormula equal(Collection<Formula> pArgs) {
+    if (pArgs.size() < 2) {
+      return booleanManager.makeTrue(); // trivially true
+    }
+    final Collection<FormulaType<Formula>> types =
+        Collections2.transform(pArgs, formulaCreator::getFormulaType);
+    Preconditions.checkArgument(
+        ImmutableSet.copyOf(types).size() == 1,
+        "All arguments to `equal` must have the same type, but found %s different types: %s",
+        types.size(),
+        types);
+    return formulaCreator.encapsulateBoolean(
+        equalImpl(Collections2.transform(pArgs, formulaCreator::extractInfo)));
+  }
+
+  /** Override if the solver API supports equality with many arguments. */
+  protected TFormulaInfo equalImpl(Collection<TFormulaInfo> pArgs) {
+    List<TFormulaInfo> equalities = new ArrayList<>();
+    for (TFormulaInfo[] pair : pairwise(pArgs)) {
+      equalities.add(equalImpl(pair[0], pair[1]));
+    }
+    return booleanManager.andImpl(equalities);
+  }
+
+  /** for an Iterable [1, 2, 3, 4, 5], collect pairs [(1,2), (2,3), (3,4), (4,5)]. */
+  @SuppressWarnings("unchecked")
+  private <T> List<T[]> pairwise(Iterable<T> pArgs) {
+    final List<T[]> result = new ArrayList<>();
+    T prev = null;
+    for (T arg : pArgs) {
+      if (prev != null) {
+        result.add((T[]) new Object[] {prev, arg});
+      }
+      prev = arg;
+    }
+    return result;
+  }
+
+  @Override
+  public BooleanFormula distinct(Collection<Formula> pArgs) {
+    if (pArgs.size() < 2) {
+      return booleanManager.makeTrue(); // trivially true
+    }
+    final Collection<FormulaType<Formula>> types =
+        Collections2.transform(pArgs, formulaCreator::getFormulaType);
+    Preconditions.checkArgument(
+        ImmutableSet.copyOf(types).size() == 1,
+        "All arguments to `equal` must have the same type, but found %s different types: %s",
+        types.size(),
+        types);
+    return formulaCreator.encapsulateBoolean(distinctImpl(formulaCreator.extractInfo(pArgs)));
+  }
+
+  /** Override if the solver API supports <code>distinct</code>. */
+  protected TFormulaInfo distinctImpl(Collection<TFormulaInfo> pArgs) {
+    List<TFormulaInfo> inequalities = new ArrayList<>();
+    for (TFormulaInfo[] pair : allUniquePairs(pArgs)) {
+      inequalities.add(booleanManager.not(equalImpl(pair[0], pair[1])));
+    }
+    return booleanManager.andImpl(inequalities);
+  }
+
+  /** for an Iterable [1, 2, 3, 4], collect all pairs [(1,2), (1,3), (1,4), (2,3), (2,4), (3,4)]. */
+  @SuppressWarnings("unchecked")
+  private <T> List<T[]> allUniquePairs(Iterable<T> pArgs) {
+    final List<T[]> result = new ArrayList<>();
+    final List<T> seenSoFar = new ArrayList<>(); // local cache for visited elements
+    for (T current : pArgs) {
+      for (T previous : seenSoFar) {
+        result.add((T[]) new Object[] {previous, current});
+      }
+      seenSoFar.add(current);
+    }
+    return result;
+  }
+
   protected abstract TFormulaInfo parseImpl(String formulaStr) throws IllegalArgumentException;
 
   /**
diff --git a/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java b/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java
index 1e1ed943f4..9b2dbd1e7d 100644
--- a/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java
+++ b/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java
@@ -16,6 +16,7 @@
 import com.google.common.collect.Sets;
 import com.google.errorprone.annotations.CanIgnoreReturnValue;
 import java.util.ArrayDeque;
+import java.util.Collection;
 import java.util.Deque;
 import java.util.HashMap;
 import java.util.LinkedHashMap;
@@ -25,6 +26,7 @@
 import java.util.Set;
 import java.util.function.BiConsumer;
 import java.util.function.Predicate;
+import java.util.stream.Collectors;
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.sosy_lab.java_smt.api.ArrayFormula;
 import org.sosy_lab.java_smt.api.BitvectorFormula;
@@ -320,8 +322,8 @@ public <R> R visit(Formula input, FormulaVisitor<R> visitor) {
    */
   public abstract <R> R visit(FormulaVisitor<R> visitor, Formula formula, TFormulaInfo f);
 
-  protected List<TFormulaInfo> extractInfo(List<? extends Formula> input) {
-    return Lists.transform(input, this::extractInfo);
+  protected List<TFormulaInfo> extractInfo(Collection<? extends Formula> input) {
+    return input.stream().map(this::extractInfo).collect(Collectors.toList());
   }
 
   /**
diff --git a/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingFormulaManager.java b/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingFormulaManager.java
index ce5c4b24aa..f16afa4098 100644
--- a/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingFormulaManager.java
+++ b/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingFormulaManager.java
@@ -13,6 +13,7 @@
 import com.google.common.collect.ImmutableMap;
 import java.io.IOException;
 import java.util.ArrayList;
+import java.util.Collection;
 import java.util.List;
 import java.util.Map;
 import org.sosy_lab.common.Appender;
@@ -148,6 +149,24 @@ public <T extends Formula> T makeApplication(
     return result;
   }
 
+  @Override
+  public BooleanFormula equal(Collection<Formula> pArgs) {
+    debugging.assertThreadLocal();
+    pArgs.forEach(debugging::assertFormulaInContext);
+    BooleanFormula result = delegate.equal(pArgs);
+    debugging.addFormulaTerm(result);
+    return result;
+  }
+
+  @Override
+  public BooleanFormula distinct(Collection<Formula> pArgs) {
+    debugging.assertThreadLocal();
+    pArgs.forEach(debugging::assertFormulaInContext);
+    BooleanFormula result = delegate.distinct(pArgs);
+    debugging.addFormulaTerm(result);
+    return result;
+  }
+
   @Override
   public <T extends Formula> FormulaType<T> getFormulaType(T formula) {
     debugging.assertThreadLocal();
diff --git a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsFormulaManager.java b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsFormulaManager.java
index 7e92bdce21..a0ee098186 100644
--- a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsFormulaManager.java
+++ b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsFormulaManager.java
@@ -12,6 +12,7 @@
 
 import com.google.common.collect.ImmutableMap;
 import java.io.IOException;
+import java.util.Collection;
 import java.util.List;
 import java.util.Map;
 import org.sosy_lab.common.Appender;
@@ -121,6 +122,20 @@ public <T extends Formula> T makeApplication(
     return delegate.makeApplication(pDeclaration, pArgs);
   }
 
+  @Override
+  public BooleanFormula equal(Collection<Formula> pArgs) {
+    // can be more than one operation, however, we count only once
+    stats.booleanOperations.getAndIncrement();
+    return delegate.equal(pArgs);
+  }
+
+  @Override
+  public BooleanFormula distinct(Collection<Formula> pArgs) {
+    // can be more than one operation, however, we count only once
+    stats.booleanOperations.getAndIncrement();
+    return delegate.distinct(pArgs);
+  }
+
   @Override
   public <T extends Formula> FormulaType<T> getFormulaType(T pFormula) {
     return delegate.getFormulaType(pFormula);
diff --git a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedFormulaManager.java b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedFormulaManager.java
index d30ce5ad77..3737614acf 100644
--- a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedFormulaManager.java
+++ b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedFormulaManager.java
@@ -12,6 +12,7 @@
 
 import com.google.common.collect.ImmutableMap;
 import java.io.IOException;
+import java.util.Collection;
 import java.util.List;
 import java.util.Map;
 import org.sosy_lab.common.Appender;
@@ -151,6 +152,20 @@ public <T extends Formula> T makeApplication(
     }
   }
 
+  @Override
+  public BooleanFormula equal(Collection<Formula> pArgs) {
+    synchronized (sync) {
+      return delegate.equal(pArgs);
+    }
+  }
+
+  @Override
+  public BooleanFormula distinct(Collection<Formula> pArgs) {
+    synchronized (sync) {
+      return delegate.distinct(pArgs);
+    }
+  }
+
   @Override
   public <T extends Formula> FormulaType<T> getFormulaType(T pFormula) {
     synchronized (sync) {
diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaManager.java
index fe91db4ea1..85eb80e409 100644
--- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaManager.java
+++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaManager.java
@@ -13,16 +13,19 @@
 import com.google.common.collect.Iterables;
 import com.google.common.collect.Table;
 import com.google.common.collect.Table.Cell;
+import java.util.Collection;
 import java.util.List;
 import org.sosy_lab.java_smt.api.Formula;
 import org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager;
 import org.sosy_lab.java_smt.basicimpl.Tokenizer;
 import org.sosy_lab.java_smt.solvers.bitwuzla.api.Bitwuzla;
+import org.sosy_lab.java_smt.solvers.bitwuzla.api.Kind;
 import org.sosy_lab.java_smt.solvers.bitwuzla.api.Map_TermTerm;
 import org.sosy_lab.java_smt.solvers.bitwuzla.api.Options;
 import org.sosy_lab.java_smt.solvers.bitwuzla.api.Parser;
 import org.sosy_lab.java_smt.solvers.bitwuzla.api.Sort;
 import org.sosy_lab.java_smt.solvers.bitwuzla.api.Term;
+import org.sosy_lab.java_smt.solvers.bitwuzla.api.Vector_Int;
 import org.sosy_lab.java_smt.solvers.bitwuzla.api.Vector_Term;
 
 public final class BitwuzlaFormulaManager
@@ -57,6 +60,18 @@ public final class BitwuzlaFormulaManager
     bitwuzlaOption = pBitwuzlaOptions;
   }
 
+  @Override
+  public Term equalImpl(Collection<Term> pArgs) {
+    return creator.getTermManager().mk_term(Kind.EQUAL, new Vector_Term(pArgs), new Vector_Int());
+  }
+
+  @Override
+  public Term distinctImpl(Collection<Term> pArgs) {
+    return creator
+        .getTermManager()
+        .mk_term(Kind.DISTINCT, new Vector_Term(pArgs), new Vector_Int());
+  }
+
   @Override
   public Term parseImpl(String formulaStr) throws IllegalArgumentException {
     // Split the input string into a list of SMT-LIB2 commands
diff --git a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorFormulaManager.java
index 864d261346..9f3c81ce9b 100644
--- a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorFormulaManager.java
+++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorFormulaManager.java
@@ -34,6 +34,11 @@ final class BoolectorFormulaManager extends AbstractFormulaManager<Long, Long, L
         null);
   }
 
+  @Override
+  protected Long equalImpl(Long pArg1, Long pArgs) {
+    return BtorJNI.boolector_eq(getEnvironment(), pArg1, pArgs);
+  }
+
   @Override
   public Long parseImpl(String pS) throws IllegalArgumentException {
     throw new UnsupportedOperationException("Boolector can not parse single formulas.");
diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaManager.java
index 03b7ccc7e4..82016c89ac 100644
--- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaManager.java
+++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaManager.java
@@ -13,9 +13,12 @@
 import de.uni_freiburg.informatik.ultimate.logic.PrintTerm;
 import edu.stanford.CVC4.Expr;
 import edu.stanford.CVC4.ExprManager;
+import edu.stanford.CVC4.Kind;
 import edu.stanford.CVC4.Type;
+import edu.stanford.CVC4.vectorExpr;
 import java.io.IOException;
 import java.io.OutputStream;
+import java.util.Collection;
 import java.util.LinkedHashMap;
 import java.util.Map;
 import org.sosy_lab.java_smt.api.Formula;
@@ -63,6 +66,20 @@ static Expr getCVC4Expr(Formula pT) {
         "Cannot get the formula info of type " + pT.getClass().getSimpleName() + " in the Solver!");
   }
 
+  @Override
+  public Expr equalImpl(Expr pArg1, Expr pArgs) {
+    return getEnvironment().mkExpr(Kind.EQUAL, pArg1, pArgs);
+  }
+
+  @Override
+  public Expr distinctImpl(Collection<Expr> pArgs) {
+    vectorExpr vec = new vectorExpr();
+    for (Expr e : pArgs) {
+      vec.add(e);
+    }
+    return getEnvironment().mkExpr(Kind.DISTINCT, vec);
+  }
+
   @Override
   public Expr parseImpl(String formulaStr) throws IllegalArgumentException {
     throw new UnsupportedOperationException();
diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java
index e77d109188..46dd896ff2 100644
--- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java
+++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java
@@ -16,6 +16,7 @@
 import io.github.cvc5.Sort;
 import io.github.cvc5.Term;
 import io.github.cvc5.TermManager;
+import java.util.Collection;
 import java.util.LinkedHashMap;
 import java.util.Map;
 import org.sosy_lab.java_smt.api.Formula;
@@ -64,6 +65,16 @@ static Term getCVC5Term(Formula pT) {
         "Cannot get the formula info of type " + pT.getClass().getSimpleName() + " in the Solver!");
   }
 
+  @Override
+  public Term equalImpl(Collection<Term> pArgs) {
+    return getEnvironment().mkTerm(Kind.EQUAL, pArgs.toArray(new Term[0]));
+  }
+
+  @Override
+  public Term distinctImpl(Collection<Term> pArgs) {
+    return getEnvironment().mkTerm(Kind.DISTINCT, pArgs.toArray(new Term[0]));
+  }
+
   @Override
   public Term parseImpl(String formulaStr) throws IllegalArgumentException {
     throw new UnsupportedOperationException();
diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaManager.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaManager.java
index 2d38c0b802..5ad55840f6 100644
--- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaManager.java
+++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaManager.java
@@ -11,6 +11,7 @@
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_apply_substitution;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_from_smtlib2;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_copy_from;
+import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_eq;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_simplify;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_to_smtlib2;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_to_smtlib2_ext;
@@ -68,6 +69,11 @@ static long[] getMsatTerm(Collection<? extends Formula> pFormulas) {
     return Longs.toArray(Collections2.transform(pFormulas, Mathsat5FormulaManager::getMsatTerm));
   }
 
+  @Override
+  protected Long equalImpl(Long pArg1, Long pArgs) {
+    return msat_make_eq(getEnvironment(), pArg1, pArgs);
+  }
+
   @Override
   public Long parseImpl(String pS) throws IllegalArgumentException {
     return msat_from_smtlib2(getEnvironment(), pS);
diff --git a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtFormulaManager.java
index 43561b2256..2be0c4f652 100644
--- a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtFormulaManager.java
+++ b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtFormulaManager.java
@@ -10,6 +10,7 @@
 
 import com.google.common.base.Joiner;
 import com.google.common.collect.Lists;
+import java.util.Collection;
 import java.util.Map;
 import org.sosy_lab.java_smt.api.FormulaType;
 import org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager;
@@ -18,6 +19,7 @@
 import org.sosy_lab.java_smt.solvers.opensmt.api.SRef;
 import org.sosy_lab.java_smt.solvers.opensmt.api.SymRef;
 import org.sosy_lab.java_smt.solvers.opensmt.api.Symbol;
+import org.sosy_lab.java_smt.solvers.opensmt.api.VectorPTRef;
 
 class OpenSmtFormulaManager extends AbstractFormulaManager<PTRef, SRef, Logic, SymRef> {
   private final OpenSmtFormulaCreator creator;
@@ -48,6 +50,16 @@ class OpenSmtFormulaManager extends AbstractFormulaManager<PTRef, SRef, Logic, S
     osmtLogic = pFormulaCreator.getEnv();
   }
 
+  @Override
+  protected PTRef equalImpl(Collection<PTRef> pArgs) {
+    return getEnvironment().mkEq(new VectorPTRef(pArgs));
+  }
+
+  @Override
+  public PTRef distinctImpl(Collection<PTRef> pArgs) {
+    return getEnvironment().mkDistinct(new VectorPTRef(pArgs));
+  }
+
   @Override
   public PTRef parseImpl(String pS) throws IllegalArgumentException {
     return osmtLogic.parseFormula(pS);
diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaManager.java
index db166985cc..98f7f60f31 100644
--- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaManager.java
+++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaManager.java
@@ -8,8 +8,11 @@
 
 package org.sosy_lab.java_smt.solvers.princess;
 
+import ap.parser.IBinFormula;
+import ap.parser.IBinJunctor;
 import ap.parser.IExpression;
 import ap.parser.IFormula;
+import ap.parser.ITerm;
 import ap.types.Sort;
 import com.google.common.base.Preconditions;
 import java.io.IOException;
@@ -55,6 +58,15 @@ BooleanFormula encapsulateBooleanFormula(IExpression t) {
     return getFormulaCreator().encapsulateBoolean(t);
   }
 
+  @Override
+  protected IExpression equalImpl(IExpression pArg1, IExpression pArgs) {
+    if (pArg1 instanceof IFormula) {
+      return new IBinFormula(IBinJunctor.Eqv(), (IFormula) pArg1, (IFormula) pArgs);
+    } else {
+      return ((ITerm) pArg1).$eq$eq$eq((ITerm) pArgs);
+    }
+  }
+
   @Override
   public IExpression parseImpl(String pS) throws IllegalArgumentException {
     List<? extends IExpression> formulas = getEnvironment().parseStringToTerms(pS, creator);
diff --git a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolFormulaManager.java
index 97fd17e496..8487d963b9 100644
--- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolFormulaManager.java
+++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolFormulaManager.java
@@ -26,6 +26,7 @@
 import de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment;
 import java.io.StringReader;
 import java.util.ArrayDeque;
+import java.util.Collection;
 import java.util.Collections;
 import java.util.Deque;
 import java.util.HashSet;
@@ -68,6 +69,16 @@ BooleanFormula encapsulateBooleanFormula(Term t) {
     return getFormulaCreator().encapsulateBoolean(t);
   }
 
+  @Override
+  protected Term equalImpl(Collection<Term> pArgs) {
+    return getEnvironment().getTheory().equals(pArgs.toArray(new Term[0]));
+  }
+
+  @Override
+  protected Term distinctImpl(Collection<Term> pArgs) {
+    return getEnvironment().getTheory().distinct(pArgs.toArray(new Term[0]));
+  }
+
   @Override
   public Term parseImpl(String pS) throws IllegalArgumentException {
     FormulaCollectionScript parseScript =
diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaCreator.java
index 0944361ff9..c43e788432 100644
--- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaCreator.java
+++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaCreator.java
@@ -490,6 +490,9 @@ private <R> R visitFunctionApplication(
       case YICES_EQ_TERM:
         functionKind = FunctionDeclarationKind.EQ; // Covers all equivalences
         break;
+      case YICES_DISTINCT_TERM:
+        functionKind = FunctionDeclarationKind.DISTINCT;
+        break;
       case YICES_NOT_TERM:
         if (isNestedExists(pF)) {
           int existsTerm = Iterables.getOnlyElement(getArgs(pF));
diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaManager.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaManager.java
index 69b0c8ae82..e1300451d4 100644
--- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaManager.java
+++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaManager.java
@@ -11,6 +11,8 @@
 import static com.google.common.base.CharMatcher.inRange;
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_APP_TERM;
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_bvtype_size;
+import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_distinct;
+import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_eq;
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_parse_term;
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_term_child;
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_term_constructor;
@@ -24,7 +26,9 @@
 import com.google.common.base.CharMatcher;
 import com.google.common.base.Preconditions;
 import com.google.common.base.Strings;
+import com.google.common.primitives.Ints;
 import java.io.IOException;
+import java.util.Collection;
 import java.util.Locale;
 import java.util.Map;
 import org.sosy_lab.java_smt.api.Formula;
@@ -68,6 +72,16 @@ static Integer getYicesTerm(Formula pT) {
     return ((Yices2Formula) pT).getTerm();
   }
 
+  @Override
+  protected Integer equalImpl(Integer pArg1, Integer pArgs) {
+    return yices_eq(pArg1, pArgs);
+  }
+
+  @Override
+  protected Integer distinctImpl(Collection<Integer> pArgs) {
+    return yices_distinct(pArgs.size(), Ints.toArray(pArgs));
+  }
+
   @Override
   public Integer parseImpl(String pS) throws IllegalArgumentException {
     // TODO Might expect Yices input language instead of smt-lib2 notation
diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaManager.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaManager.java
index d5abf99371..0c8f880552 100644
--- a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaManager.java
+++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaManager.java
@@ -14,6 +14,7 @@
 import com.microsoft.z3.Native;
 import com.microsoft.z3.Z3Exception;
 import java.util.ArrayList;
+import java.util.Collection;
 import java.util.List;
 import java.util.Map;
 import java.util.regex.Matcher;
@@ -58,6 +59,20 @@ final class Z3FormulaManager extends AbstractFormulaManager<Long, Long, Long, Lo
     formulaCreator = pFormulaCreator;
   }
 
+  @Override
+  public Long equalImpl(Long pArg1, Long pArgs) {
+    // We need to add a phantom reference here, otherwise Z3 will hang
+    // TODO Remove this hack
+    var term = Native.mkEq(getEnvironment(), pArg1, pArgs);
+    Native.incRef(getEnvironment(), term);
+    return term;
+  }
+
+  @Override
+  public Long distinctImpl(Collection<Long> pArgs) {
+    return Native.mkDistinct(getEnvironment(), pArgs.size(), Longs.toArray(pArgs));
+  }
+
   @Override
   public Long parseImpl(String str) throws IllegalArgumentException {
 
diff --git a/src/org/sosy_lab/java_smt/test/FormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/FormulaManagerTest.java
index 2cf4a2eaf6..ac5943e06a 100644
--- a/src/org/sosy_lab/java_smt/test/FormulaManagerTest.java
+++ b/src/org/sosy_lab/java_smt/test/FormulaManagerTest.java
@@ -10,27 +10,237 @@
 
 import static com.google.common.truth.Truth.assertThat;
 import static com.google.common.truth.TruthJUnit.assume;
+import static org.junit.Assert.assertThrows;
 import static org.sosy_lab.java_smt.api.FormulaType.BooleanType;
 import static org.sosy_lab.java_smt.api.FormulaType.IntegerType;
+import static org.sosy_lab.java_smt.api.FormulaType.RationalType;
+import static org.sosy_lab.java_smt.api.FormulaType.getArrayType;
+import static org.sosy_lab.java_smt.api.FormulaType.getBitvectorTypeWithSize;
 
 import com.google.common.collect.ImmutableList;
 import com.google.common.collect.ImmutableMap;
 import com.google.common.testing.EqualsTester;
 import java.math.BigDecimal;
 import java.math.BigInteger;
+import java.util.List;
 import java.util.Map;
 import org.junit.Test;
 import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
 import org.sosy_lab.java_smt.api.ArrayFormula;
 import org.sosy_lab.java_smt.api.BitvectorFormula;
 import org.sosy_lab.java_smt.api.BooleanFormula;
+import org.sosy_lab.java_smt.api.Formula;
+import org.sosy_lab.java_smt.api.FormulaManager;
 import org.sosy_lab.java_smt.api.FormulaType;
 import org.sosy_lab.java_smt.api.FunctionDeclaration;
 import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
 import org.sosy_lab.java_smt.api.SolverException;
+import org.sosy_lab.java_smt.api.visitors.FormulaTransformationVisitor;
 
 public class FormulaManagerTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 {
 
+  @Test
+  public void testWrongSorts() {
+    // Check that an exception is thrown if the arguments to `=` or `distinct` don't have matching
+    // types
+    var formulaType = imgr != null ? IntegerType : getBitvectorTypeWithSize(8);
+
+    var var1 = mgr.makeVariable(BooleanType, "var1");
+    var var2 = mgr.makeVariable(formulaType, "var2");
+
+    assertThrows(IllegalArgumentException.class, () -> mgr.equal(var1, var2));
+    assertThrows(IllegalArgumentException.class, () -> mgr.distinct(var1, var2));
+
+    if (bvmgr != null) {
+      var bv1 = mgr.makeVariable(getBitvectorTypeWithSize(8), "bv1");
+      var bv2 = mgr.makeVariable(getBitvectorTypeWithSize(16), "bv2");
+
+      assertThrows(IllegalArgumentException.class, () -> mgr.equal(bv1, bv2));
+      assertThrows(IllegalArgumentException.class, () -> mgr.distinct(bv1, bv2));
+    }
+
+    if (amgr != null) {
+      var domainType = formulaType;
+      var rangeType = formulaType == IntegerType ? RationalType : getBitvectorTypeWithSize(16);
+
+      var arr1 = mgr.makeVariable(getArrayType(domainType, rangeType), "arr1");
+      var arr2 = mgr.makeVariable(getArrayType(rangeType, domainType), "arr2");
+
+      assertThrows(IllegalArgumentException.class, () -> mgr.equal(arr1, arr2));
+      assertThrows(IllegalArgumentException.class, () -> mgr.distinct(arr1, arr2));
+    }
+  }
+
+  @Test
+  public void testSmallNumberOfArgs() {
+    var formulaType = imgr != null ? IntegerType : getBitvectorTypeWithSize(8);
+    var var1 = mgr.makeVariable(formulaType, "var1");
+
+    assertThat(mgr.equal()).isEqualTo(bmgr.makeTrue());
+    assertThat(mgr.distinct()).isEqualTo(bmgr.makeTrue());
+
+    assertThat(mgr.equal(var1)).isEqualTo(bmgr.makeTrue());
+    assertThat(mgr.distinct(var1)).isEqualTo(bmgr.makeTrue());
+  }
+
+  @Test
+  public void testEquality() {
+    // Check if `=` terms are rewritten
+    var formulaType = imgr != null ? IntegerType : getBitvectorTypeWithSize(8);
+
+    var var1 = mgr.makeVariable(formulaType, "var1");
+    var var2 = mgr.makeVariable(formulaType, "var2");
+    var var3 = mgr.makeVariable(formulaType, "var3");
+
+    var f = mgr.equal(var1, var2, var3);
+    var g = bmgr.and(mgr.equal(var1, var2), mgr.equal(var2, var3));
+
+    if (solver == Solvers.SMTINTERPOL) {
+      // Only SmtInterpol support equality with more than two arguments
+      assertThat(f).isNotEqualTo(g);
+    } else {
+      // ... all other solvers will rewrite
+      assertThat(f).isEqualTo(g);
+    }
+  }
+
+  private class Rebuilder extends FormulaTransformationVisitor {
+    Rebuilder(FormulaManager fmgr) {
+      super(fmgr);
+    }
+
+    @Override
+    public Formula visitFreeVariable(Formula f, String name) {
+      return mgr.makeVariable(mgr.getFormulaType(f), name);
+    }
+
+    @SuppressWarnings("unchecked")
+    @Override
+    public Formula visitFunction(
+        Formula f, List<Formula> args, FunctionDeclaration<?> functionDeclaration) {
+      switch (functionDeclaration.getKind()) {
+        case AND:
+          return bmgr.and((List<BooleanFormula>) (List<?>) args);
+        case NOT:
+          return bmgr.not((BooleanFormula) args.get(0));
+        case EQ:
+          return mgr.equal(args);
+        case DISTINCT:
+          return mgr.distinct(args);
+        default:
+          throw new UnsupportedOperationException();
+      }
+    }
+  }
+
+  @Test
+  public void testEqualityVisitor() {
+    assume().that(solver).isNotEqualTo(Solvers.BOOLECTOR);
+
+    var formulaType = imgr != null ? IntegerType : getBitvectorTypeWithSize(8);
+
+    var var1 = mgr.makeVariable(formulaType, "var1");
+    var var2 = mgr.makeVariable(formulaType, "var2");
+    var var3 = mgr.makeVariable(formulaType, "var3");
+
+    var f = mgr.equal(var1, var2, var3);
+    var g = mgr.transformRecursively(f, new Rebuilder(mgr));
+
+    assertThat(f).isEqualTo(g);
+  }
+
+  @Test
+  public void testEqualityParser() {
+    // Check that we can recreate `=` terms from the parser
+    requireParser();
+
+    var formulaType = imgr != null ? IntegerType : getBitvectorTypeWithSize(8);
+
+    var var1 = mgr.makeVariable(formulaType, "var1");
+    var var2 = mgr.makeVariable(formulaType, "var2");
+    var var3 = mgr.makeVariable(formulaType, "var3");
+
+    var formulaSort = imgr != null ? "Int" : "(_ BitVec 8)";
+
+    var str =
+        String.format("(define-const %s %s)", var1, formulaSort)
+            + String.format("(define-const %s %s)", var2, formulaSort)
+            + String.format("(define-const %s %s)", var3, formulaSort)
+            + String.format("(assert (= %s %s %s))", var1, var2, var3);
+
+    var f = mgr.equal(var1, var2, var3);
+    var g = mgr.parse(str);
+
+    assertThat(f).isEqualTo(g);
+  }
+
+  @Test
+  public void testDistinct() {
+    // Check if `distinct` terms are rewritten
+    var formulaType = imgr != null ? IntegerType : getBitvectorTypeWithSize(8);
+
+    var var1 = mgr.makeVariable(formulaType, "var1");
+    var var2 = mgr.makeVariable(formulaType, "var2");
+    var var3 = mgr.makeVariable(formulaType, "var3");
+
+    var f = mgr.distinct(var1, var2, var3);
+    var g =
+        bmgr.and(
+            bmgr.not(mgr.equal(var1, var2)),
+            bmgr.not(mgr.equal(var1, var3)),
+            bmgr.not(mgr.equal(var2, var3)));
+
+    if (ImmutableList.of(Solvers.BOOLECTOR, Solvers.MATHSAT5, Solvers.PRINCESS).contains(solver)) {
+      // Solvers that rewrite
+      assertThat(f).isEqualTo(g);
+    } else {
+      // Solvers that keep the distinct term
+      // Note that Bitwuzla will partially rewrite and only supports distinct for 2 arguments
+      assertThat(f).isNotEqualTo(g);
+    }
+  }
+
+  @Test
+  public void testDistinctVisitor() {
+    assume().that(solver).isNotEqualTo(Solvers.BOOLECTOR);
+
+    var formulaType = imgr != null ? IntegerType : getBitvectorTypeWithSize(8);
+
+    var var1 = mgr.makeVariable(formulaType, "var1");
+    var var2 = mgr.makeVariable(formulaType, "var2");
+    var var3 = mgr.makeVariable(formulaType, "var3");
+
+    var f = mgr.distinct(var1, var2, var3);
+    var g = mgr.transformRecursively(f, new Rebuilder(mgr));
+
+    assertThat(f).isEqualTo(g);
+  }
+
+  @Test
+  public void testDistinctParser() {
+    // Check that we can recreate `distinct` terms from the parser
+    requireParser();
+
+    var formulaType = imgr != null ? IntegerType : getBitvectorTypeWithSize(8);
+
+    var var1 = mgr.makeVariable(formulaType, "var1");
+    var var2 = mgr.makeVariable(formulaType, "var2");
+    var var3 = mgr.makeVariable(formulaType, "var3");
+
+    var formulaSort = imgr != null ? "Int" : "(_ BitVec 8)";
+
+    var str =
+        String.format("(define-const %s %s)", var1, formulaSort)
+            + String.format("(define-const %s %s)", var2, formulaSort)
+            + String.format("(define-const %s %s)", var3, formulaSort)
+            + String.format("(assert (distinct %s %s %s))", var1, var2, var3);
+
+    var f = mgr.distinct(var1, var2, var3);
+    var g = mgr.parse(str);
+
+    assertThat(f).isEqualTo(g);
+  }
+
   @Test
   public void testEmptySubstitution() throws SolverException, InterruptedException {
     requireSubstitution();