diff --git a/build/ivysettings.xml b/build/ivysettings.xml
index be96cf00b5..c8d01d97a7 100644
--- a/build/ivysettings.xml
+++ b/build/ivysettings.xml
@@ -10,7 +10,6 @@ SPDX-FileCopyrightText: 2018-2020 Dirk Beyer <https://www.sosy-lab.org>
 SPDX-License-Identifier: Apache-2.0
 -->
 
-<!DOCTYPE ivysettings> <!-- generic AcceptAllDTD to make the Eclipse Warning go away -->
 <ivysettings>
     <!-- DO NOT EDIT LOCALLY!
          Keep this file synchronized with
diff --git a/src/org/sosy_lab/java_smt/api/SolverContext.java b/src/org/sosy_lab/java_smt/api/SolverContext.java
index 3fbd476c77..3c7a8ad7d0 100644
--- a/src/org/sosy_lab/java_smt/api/SolverContext.java
+++ b/src/org/sosy_lab/java_smt/api/SolverContext.java
@@ -52,6 +52,36 @@ enum ProverOptions {
      */
     GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS,
 
+    /**
+     * Enables Craig interpolation, using the model-based interpolation strategy. This strategy
+     * constructs interpolants based on the model provided by a solver, i.e. model generation must
+     * be enabled. This interpolation strategy is only usable for solvers supporting quantified
+     * solving over the theories interpolated upon. The solver does not need to support
+     * interpolation itself.
+     */
+    GENERATE_MODEL_BASED_INTERPOLANTS,
+
+    /**
+     * Enables (uniform) Craig interpolation, using the quantifier-based interpolation strategy
+     * utilizing quantifier-elimination in the forward direction. Forward means, that the set of
+     * formulas A, used to interpolate, interpolates towards the set of formulas B (B == all
+     * formulas that are currently asserted, but not in the given set of formulas A used to
+     * interpolate). This interpolation strategy is only usable for solvers supporting
+     * quantifier-elimination over the theories interpolated upon. The solver does not need to
+     * support interpolation itself.
+     */
+    GENERATE_UNIFORM_FORWARD_INTERPOLANTS,
+
+    /**
+     * Enables (uniform) Craig interpolation, using the quantifier-based interpolation strategy
+     * utilizing quantifier-elimination in the backward direction. Backward means, that the set of
+     * formulas B (B == all formulas that are currently asserted, but not in the given set of
+     * formulas A used to interpolate) interpolates towards the set of formulas A. This
+     * interpolation strategy is only usable for solvers supporting quantifier-elimination over the
+     * theories interpolated upon. The solver does not need to support interpolation itself.
+     */
+    GENERATE_UNIFORM_BACKWARD_INTERPOLANTS,
+
     /** Whether the solver should enable support for formulae build in SL theory. */
     ENABLE_SEPARATION_LOGIC
   }
diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java
index 72c894c56f..cf3ade5188 100644
--- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java
+++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java
@@ -17,8 +17,10 @@
 import com.google.common.collect.Multimap;
 import com.google.errorprone.annotations.CanIgnoreReturnValue;
 import java.util.ArrayList;
+import java.util.Collection;
 import java.util.LinkedHashSet;
 import java.util.List;
+import java.util.Map.Entry;
 import java.util.Set;
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.sosy_lab.java_smt.api.BasicProverEnvironment;
@@ -133,6 +135,27 @@ protected ImmutableSet<T> getAssertedConstraintIds() {
     return builder.build();
   }
 
+  /**
+   * Returns a tuple, consisting of 2 sets, that combined form the set of all formulas on the stack.
+   * The set of formulas A is the formulas identified by the set of input interpolation points. The
+   * set of formulas B is the rest of the current asserted formulas.
+   */
+  protected InterpolationFormulas getInterpolationGroups(Collection<T> pFormulasOfA) {
+    ImmutableSet.Builder<BooleanFormula> formulasOfA = ImmutableSet.builder();
+    ImmutableSet.Builder<BooleanFormula> formulasOfB = ImmutableSet.builder();
+    for (Multimap<BooleanFormula, T> assertedFormulasPerLevel : assertedFormulas) {
+      for (Entry<BooleanFormula, T> assertedFormulaAndItpPoint :
+          assertedFormulasPerLevel.entries()) {
+        if (pFormulasOfA.contains(assertedFormulaAndItpPoint.getValue())) {
+          formulasOfA.add(assertedFormulaAndItpPoint.getKey());
+        } else {
+          formulasOfB.add(assertedFormulaAndItpPoint.getKey());
+        }
+      }
+    }
+    return InterpolationFormulas.of(formulasOfA.build(), formulasOfB.build());
+  }
+
   /**
    * This method registers the Evaluator to be cleaned up before the next change on the prover
    * stack.
@@ -157,4 +180,31 @@ public void close() {
     closeAllEvaluators();
     closed = true;
   }
+
+  /** Provides the set of formulas to interpolate on a distinct prover. */
+  public static class InterpolationFormulas {
+    private final Collection<BooleanFormula> formulasForA;
+    private final Collection<BooleanFormula> formulasForB;
+
+    private InterpolationFormulas(
+        Collection<BooleanFormula> pFormulasOfA, Collection<BooleanFormula> pFormulasOfB) {
+      Preconditions.checkNotNull(pFormulasOfA);
+      Preconditions.checkNotNull(pFormulasOfB);
+      formulasForA = pFormulasOfA;
+      formulasForB = pFormulasOfB;
+    }
+
+    protected static InterpolationFormulas of(
+        Collection<BooleanFormula> pFormulasOfA, Collection<BooleanFormula> pFormulasOfB) {
+      return new InterpolationFormulas(pFormulasOfA, pFormulasOfB);
+    }
+
+    protected Collection<BooleanFormula> gotFormulasForA() {
+      return formulasForA;
+    }
+
+    protected Collection<BooleanFormula> gotFormulasForB() {
+      return formulasForB;
+    }
+  }
 }
diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProverWithAllSat.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProverWithAllSat.java
index 084af23c01..f79e11a2f2 100644
--- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProverWithAllSat.java
+++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProverWithAllSat.java
@@ -18,6 +18,7 @@
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.BooleanFormulaManager;
 import org.sosy_lab.java_smt.api.Evaluator;
+import org.sosy_lab.java_smt.api.FormulaManager;
 import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
 import org.sosy_lab.java_smt.api.SolverException;
 
@@ -32,11 +33,9 @@ public abstract class AbstractProverWithAllSat<T> extends AbstractProver<T> {
   private final BooleanFormulaManager bmgr;
 
   protected AbstractProverWithAllSat(
-      Set<ProverOptions> pOptions,
-      BooleanFormulaManager pBmgr,
-      ShutdownNotifier pShutdownNotifier) {
+      Set<ProverOptions> pOptions, FormulaManager pMgr, ShutdownNotifier pShutdownNotifier) {
     super(pOptions);
-    bmgr = pBmgr;
+    bmgr = pMgr.getBooleanFormulaManager();
     shutdownNotifier = pShutdownNotifier;
   }
 
diff --git a/src/org/sosy_lab/java_smt/basicimpl/IndependentInterpolatingProverEnvironment.java b/src/org/sosy_lab/java_smt/basicimpl/IndependentInterpolatingProverEnvironment.java
new file mode 100644
index 0000000000..e0d17a8343
--- /dev/null
+++ b/src/org/sosy_lab/java_smt/basicimpl/IndependentInterpolatingProverEnvironment.java
@@ -0,0 +1,597 @@
+/*
+ * This file is part of JavaSMT,
+ * an API wrapper for a collection of SMT solvers:
+ * https://github.com/sosy-lab/java-smt
+ *
+ * SPDX-FileCopyrightText: 2024 Dirk Beyer <https://www.sosy-lab.org>
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ */
+
+package org.sosy_lab.java_smt.basicimpl;
+
+import static com.google.common.base.Preconditions.checkArgument;
+import static com.google.common.base.Preconditions.checkNotNull;
+import static com.google.common.base.Preconditions.checkState;
+
+import com.google.common.base.Preconditions;
+import com.google.common.collect.ImmutableList;
+import com.google.common.collect.ImmutableSet;
+import edu.umd.cs.findbugs.annotations.SuppressFBWarnings;
+import java.util.ArrayList;
+import java.util.Collection;
+import java.util.HashSet;
+import java.util.List;
+import java.util.Optional;
+import java.util.Set;
+import org.checkerframework.checker.nullness.qual.Nullable;
+import org.sosy_lab.common.UniqueIdGenerator;
+import org.sosy_lab.java_smt.api.BasicProverEnvironment;
+import org.sosy_lab.java_smt.api.BooleanFormula;
+import org.sosy_lab.java_smt.api.BooleanFormulaManager;
+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.InterpolatingProverEnvironment;
+import org.sosy_lab.java_smt.api.Model;
+import org.sosy_lab.java_smt.api.ProverEnvironment;
+import org.sosy_lab.java_smt.api.QuantifiedFormulaManager;
+import org.sosy_lab.java_smt.api.SolverContext;
+import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
+import org.sosy_lab.java_smt.api.SolverException;
+import org.sosy_lab.java_smt.api.UFManager;
+
+public class IndependentInterpolatingProverEnvironment<F, T> extends AbstractProver<F>
+    implements InterpolatingProverEnvironment<F> {
+
+  private final SolverContext solverContext;
+
+  private final BasicProverEnvironment<?> delegate;
+
+  private final FormulaCreator<F, T, ?, ?> creator;
+  private final FormulaManager mgr;
+  private final BooleanFormulaManager bmgr;
+  private final UFManager ufmgr;
+
+  // null for native solver interpolation
+  private final @Nullable ProverOptions interpolationStrategy;
+
+  private static final Set<ProverOptions> ALL_INDEPENDENT_INTERPOLATION_STRATEGIES =
+      ImmutableSet.of(
+          ProverOptions.GENERATE_MODEL_BASED_INTERPOLANTS,
+          ProverOptions.GENERATE_UNIFORM_BACKWARD_INTERPOLANTS,
+          ProverOptions.GENERATE_UNIFORM_FORWARD_INTERPOLANTS);
+  private static final UniqueIdGenerator UNIQUE_ID_GENERATOR = new UniqueIdGenerator();
+  private static final String PREFIX = "__internal_model_itp_generation_";
+  private static final String SYMBOL_QUANTIFIER_FORALL = "ALL";
+  private static final String SYMBOL_QUANTIFIER_EXISTS = "EX";
+
+  public IndependentInterpolatingProverEnvironment(
+      SolverContext pSourceContext,
+      FormulaCreator<F, T, ?, ?> pCreator,
+      BasicProverEnvironment<?> pDelegate,
+      Set<ProverOptions> pOptions) {
+    super(pOptions);
+    solverContext = checkNotNull(pSourceContext);
+    delegate = checkNotNull(pDelegate);
+    creator = pCreator;
+    interpolationStrategy =
+        getIndependentInterpolationStrategy(pOptions, pSourceContext.getFormulaManager());
+    mgr = pSourceContext.getFormulaManager();
+    bmgr = mgr.getBooleanFormulaManager();
+    ufmgr = mgr.getUFManager();
+  }
+
+  /**
+   * Checks, whether an independent interpolation strategy is enabled for the given prover.
+   *
+   * @param options A set of all enabled options for the prover to check.
+   * @return {@code true} if an independent interpolation strategy is configured, {@code false}
+   *     otherwise.
+   */
+  public static boolean hasIndependentInterpolationStrategy(
+      Set<ProverOptions> options, FormulaManager pFormulaManager) {
+    return getIndependentInterpolationStrategy(options, pFormulaManager) != null;
+  }
+
+  @SuppressFBWarnings(value = "DLS_DEAD_LOCAL_STORE", justification = "unused")
+  @SuppressWarnings("unused")
+  private static @Nullable ProverOptions getIndependentInterpolationStrategy(
+      Set<ProverOptions> options, FormulaManager pFormulaManager) {
+    List<ProverOptions> itpStrat = new ArrayList<>(options);
+    itpStrat.retainAll(ALL_INDEPENDENT_INTERPOLATION_STRATEGIES);
+    if (itpStrat.isEmpty()) {
+      return null;
+    }
+    Preconditions.checkState(itpStrat.size() == 1);
+    try {
+      QuantifiedFormulaManager dummy = pFormulaManager.getQuantifiedFormulaManager();
+    } catch (UnsupportedOperationException e) {
+      throw new UnsupportedOperationException(
+          "Solver does not support independent interpolation based on the current strategy, as it"
+              + " is lacking quantifier support.");
+    }
+    return itpStrat.get(0);
+  }
+
+  @SuppressWarnings({"unchecked", "unused"})
+  @Override
+  public BooleanFormula getInterpolant(Collection<F> pFormulasOfA)
+      throws SolverException, InterruptedException {
+    checkArgument(
+        super.getAssertedConstraintIds().containsAll(pFormulasOfA),
+        "interpolation can only be done over previously asserted formulas.");
+
+    if (interpolationStrategy == null) {
+      if (delegate instanceof InterpolatingProverEnvironment) {
+        // Use native solver interpolation
+        return ((InterpolatingProverEnvironment<F>) delegate).getInterpolant(pFormulasOfA);
+      } else {
+        throw new UnsupportedOperationException(
+            "Solver does not natively support interpolation in JavaSMT currently.");
+      }
+    }
+
+    InterpolationFormulas formulasAAndB = super.getInterpolationGroups(pFormulasOfA);
+    Collection<BooleanFormula> formulasOfA = formulasAAndB.gotFormulasForA();
+    Collection<BooleanFormula> formulasOfB = formulasAAndB.gotFormulasForB();
+
+    BooleanFormula conjugatedA = bmgr.and(formulasOfA);
+    BooleanFormula conjugatedB = bmgr.and(formulasOfB);
+
+    List<Formula> varsOfA = getVars(conjugatedA);
+    List<Formula> varsOfB = getVars(conjugatedB);
+
+    ImmutableList<Formula> sharedVars = getSharedVars(varsOfA, varsOfB);
+
+    if (formulasOfA.isEmpty()) {
+      return bmgr.makeTrue();
+    }
+    if (formulasOfB.isEmpty()) {
+      return bmgr.makeFalse();
+    }
+    if (sharedVars.isEmpty()) {
+      return bmgr.makeTrue();
+    }
+
+    Preconditions.checkNotNull(interpolationStrategy);
+
+    if (interpolationStrategy.equals(ProverOptions.GENERATE_MODEL_BASED_INTERPOLANTS)) {
+      return getModelBasedInterpolant(conjugatedA, conjugatedB, varsOfA, varsOfB, sharedVars);
+    } else {
+      return getQuantifierEliminationBasedInterpolant(
+          conjugatedA, conjugatedB, varsOfA, varsOfB, sharedVars);
+    }
+  }
+
+  @SuppressWarnings("unchecked")
+  @Override
+  public List<BooleanFormula> getTreeInterpolants(
+      List<? extends Collection<F>> partitionedFormulas, int[] startOfSubTree)
+      throws SolverException, InterruptedException {
+    if (interpolationStrategy == null) {
+      if (delegate instanceof InterpolatingProverEnvironment) {
+        // Use native solver interpolation
+        return ((InterpolatingProverEnvironment<F>) delegate)
+            .getTreeInterpolants(partitionedFormulas, startOfSubTree);
+      }
+    }
+    throw new UnsupportedOperationException(
+        "Tree interpolants are not supported for independent interpolation currently.");
+  }
+
+  @SuppressWarnings("unchecked")
+  @Override
+  public List<BooleanFormula> getSeqInterpolants(List<? extends Collection<F>> pPartitionedFormulas)
+      throws SolverException, InterruptedException {
+    if (interpolationStrategy == null) {
+      if (delegate instanceof InterpolatingProverEnvironment) {
+        // Use native solver interpolation
+        return ((InterpolatingProverEnvironment<F>) delegate)
+            .getSeqInterpolants(pPartitionedFormulas);
+      }
+    }
+    throw new UnsupportedOperationException(
+        "Sequential interpolants are not supported for independent interpolation currently.");
+  }
+
+  /**
+   * Computes Craig interpolants for a {@link Collection} of {@link BooleanFormula}s using the
+   * model-based solver independent interpolation strategy.
+   *
+   * <p>This interpolation strategy takes two sets of {@link BooleanFormula}s, A and B, as input to
+   * generate Craig interpolants, based on the following definition of Craig interpolation:
+   *
+   * <ol>
+   *   <li>The implication (A -> Itp) is unsatisfiable.
+   *   <li>The implication (Itp -> NOT B) is unsatisfiable.
+   *   <li>The interpolant Itp only contains symbols that appear in both sets of formulas A and B.
+   * </ol>
+   *
+   * <p>Additionally, the Craig interpolant is a satisfying assignment to the following Constrained
+   * Horn Clause:
+   *
+   * <ul>
+   *   <li>For all (a, c). (A(a, c) -> Itp(c))
+   *   <li>For all (b, c). (Itp(c) -> NOT (B(b, c)))
+   * </ul>
+   *
+   * <p>A solver checks, whether the definition of Craig interpolation is satisfied and generates a
+   * model accordingly.
+   *
+   * <p>Please note, that this interpolation strategy is only usable for solvers supporting
+   * quantified solving over the theories interpolated upon. The solver does not need to support
+   * interpolation itself.
+   *
+   * @param formulasOfA A {@link BooleanFormula} representing the set of A.
+   * @param formulasOfB A {@link BooleanFormula} representing the set of B.
+   * @param varsOfA A list of all variables in formulas of A.
+   * @param varsOfB A list of all variables in formulas of B.
+   * @param sharedVars A list of variables found in both sets of formulas A and B.
+   * @return the Craig interpolant, otherwise {@code false} in case an interpolant can not be found.
+   * @see <a href="https://github.com/agurfinkel/spacer-on-jupyter/blob/master/Dagstuhl2019.ipynb">
+   *     Binary Craig Interpolation by reduction to CHC</a>
+   */
+  private BooleanFormula getModelBasedInterpolant(
+      BooleanFormula formulasOfA,
+      BooleanFormula formulasOfB,
+      List<Formula> varsOfA,
+      List<Formula> varsOfB,
+      ImmutableList<Formula> sharedVars)
+      throws InterruptedException, SolverException {
+
+    QuantifiedFormulaManager qfmgr = mgr.getQuantifiedFormulaManager();
+
+    BooleanFormula itp = getUniqueInterpolant(sharedVars);
+    BooleanFormula left = qfmgr.forall(varsOfA, bmgr.implication(formulasOfA, itp));
+    BooleanFormula right = qfmgr.forall(varsOfB, bmgr.implication(itp, bmgr.not(formulasOfB)));
+
+    // check the satisfiability of the constraints and generate a model if possible
+    BooleanFormula interpolant = bmgr.makeFalse();
+    try (ProverEnvironment itpProver = getDistinctProver()) {
+
+      itpProver.push(bmgr.and(left, right));
+
+      if (!itpProver.isUnsat()) {
+        try (Model model = itpProver.getModel()) {
+          interpolant = model.eval(itp);
+        }
+        Preconditions.checkNotNull(interpolant);
+      }
+    }
+    return interpolant;
+  }
+
+  /**
+   * Computes uniform Craig interpolants for a {@link Collection} of {@link BooleanFormula}s using
+   * the quantifier-based solver independent interpolation strategy with quantifier-elimination.
+   *
+   * <p>This interpolation strategy takes two sets of {@link BooleanFormula}s, A and B, as input and
+   * their variables a, b, c, satisfying the following rules to generate uniform Craig interpolants,
+   * a stronger version of Craig interpolants:
+   *
+   * <ul>
+   *   <li>A set of variables a that appears in formulas of A, but not in formulas of B.
+   *   <li>A set of variables b that appears in formulas of B, but not in formulas of A.
+   *   <li>A set of variables c that appear in both sets of formulas A and B.
+   * </ul>
+   *
+   * <p>Quantifier-elimination can be performed in two directions, forward and backward, to generate
+   * uniform Craig interpolants:
+   *
+   * <ul>
+   *   <li>Forward version: interpolation(A(a, c), B(b, c)) = exists a. A(a, c)
+   *   <li>Backward version: interpolation(A(a, c), B(b, c)) = for all b. NOT B(b, c)
+   * </ul>
+   *
+   * <p>A solver verifies, whether the definition of Craig interpolation is satisfied for the
+   * resulting uniform Craig interpolant.
+   *
+   * <p>Please note, that this interpolation strategy is only usable for solver supporting
+   * quantifier-elimination over theories interpolated upon. The solver does not need to support
+   * interpolation itself.
+   *
+   * @param formulasOfA A {@link BooleanFormula} representing the set of A.
+   * @param formulasOfB A {@link BooleanFormula} representing the set of B.
+   * @param varsOfA A list of all variables in formulas of A.
+   * @param varsOfB A list of all variables in formulas of B.
+   * @param sharedVars A list of variables found in both sets of formulas A and B.
+   * @return the uniform Craig interpolant, otherwise {@code false} in case an interpolant can not
+   *     be found.
+   */
+  private BooleanFormula getQuantifierEliminationBasedInterpolant(
+      BooleanFormula formulasOfA,
+      BooleanFormula formulasOfB,
+      List<Formula> varsOfA,
+      List<Formula> varsOfB,
+      ImmutableList<Formula> sharedVars)
+      throws SolverException, InterruptedException {
+
+    Preconditions.checkState(isUnsat());
+    checkNotNull(interpolationStrategy);
+
+    BooleanFormula interpolant = bmgr.makeFalse();
+    if (interpolationStrategy.equals(ProverOptions.GENERATE_UNIFORM_BACKWARD_INTERPOLANTS)) {
+      interpolant = getBackwardInterpolant(formulasOfB, varsOfB, sharedVars);
+    } else if (interpolationStrategy.equals(ProverOptions.GENERATE_UNIFORM_FORWARD_INTERPOLANTS)) {
+      interpolant = getForwardInterpolant(formulasOfA, varsOfA, sharedVars);
+    }
+
+    if (!satisfiesInterpolationCriteria(interpolant, formulasOfA, formulasOfB, sharedVars)) {
+      return bmgr.makeFalse();
+    }
+
+    return interpolant;
+  }
+
+  /**
+   * Computes the uniform Craig interpolant, using the quantifier-based interpolation strategy
+   * utilizing quantifier-elimination in the backward direction.
+   *
+   * <p>Backward means, that the set of formulas B interpolates towards the set of formulas A.
+   *
+   * @param formulasOfB The set of formulas B, combined into one {@link BooleanFormula}.
+   * @param varsOfB A list of all variables in formulas of B.
+   * @param sharedVars A list of variables found in both sets of formulas A and B.
+   * @return a uniform Craig interpolant, using quantifier-elimination in the backward direction.
+   */
+  private BooleanFormula getBackwardInterpolant(
+      BooleanFormula formulasOfB, List<Formula> varsOfB, List<Formula> sharedVars)
+      throws SolverException, InterruptedException {
+
+    BooleanFormula itpBackward = formulasOfB;
+
+    ImmutableList<Formula> boundVars = getBoundVars(varsOfB, sharedVars);
+    QuantifiedFormulaManager qfmgr = mgr.getQuantifiedFormulaManager();
+    if (!boundVars.isEmpty()) {
+      try {
+        BooleanFormula itpBackwardQuantified = qfmgr.forall(boundVars, bmgr.not(formulasOfB));
+        BooleanFormula itpBackwardQuantifierEliminated =
+            qfmgr.eliminateQuantifiers(itpBackwardQuantified);
+        // check if the quantifier has been eliminated properly
+        if (!itpBackwardQuantifierEliminated.toString().contains(SYMBOL_QUANTIFIER_FORALL)) {
+          // check if the shared variables still exist and are not eliminated during the process
+          if (sharedVars.stream()
+              .allMatch(
+                  formula ->
+                      itpBackwardQuantifierEliminated.toString().contains(formula.toString()))) {
+            return itpBackwardQuantifierEliminated;
+          }
+          throw new SolverException(
+              "Quantifier elimination failed. "
+                  + "Shared variables were accidentally deleted during the process.");
+        }
+        throw new SolverException(
+            "Quantifier elimination failed. "
+                + "Resulting interpolant still contains quantifiers.");
+      } catch (UnsupportedOperationException e) {
+        throw new UnsupportedOperationException(
+            "Solver does not support the complete theory of quantifiers.", e);
+      } catch (InterruptedException e) {
+        throw new InterruptedException();
+      }
+    }
+
+    return itpBackward;
+  }
+
+  /**
+   * Computes the uniform Craig interpolant, using the quantifier-based interpolation strategy
+   * utilizing quantifier-elimination in the forward direction.
+   *
+   * <p>Forward means, that the set of formulas A interpolates towards the set of formulas B.
+   *
+   * @param formulasOfA The set of formulas A, combined into one {@link BooleanFormula}.
+   * @param varsOfA A list of all variables in formulas of A.
+   * @param sharedVars A list of variables found in both sets of formulas A and B.
+   * @return a uniform Craig interpolant, using quantifier-elimination in the forward direction.
+   */
+  private BooleanFormula getForwardInterpolant(
+      BooleanFormula formulasOfA, List<Formula> varsOfA, List<Formula> sharedVars)
+      throws SolverException, InterruptedException {
+
+    BooleanFormula itpForward = formulasOfA;
+
+    ImmutableList<Formula> boundVars = getBoundVars(varsOfA, sharedVars);
+    QuantifiedFormulaManager qfmgr = mgr.getQuantifiedFormulaManager();
+    if (!boundVars.isEmpty()) {
+      try {
+        BooleanFormula itpForwardQuantified = qfmgr.exists(boundVars, formulasOfA);
+        BooleanFormula itpForwardQuantifierEliminated =
+            qfmgr.eliminateQuantifiers(itpForwardQuantified);
+        // check if the quantifier has been eliminated properly
+        if (!itpForwardQuantifierEliminated.toString().equals(SYMBOL_QUANTIFIER_EXISTS)) {
+          // check if the shared variables still exist and are not eliminated during the process
+          if (sharedVars.stream()
+              .allMatch(
+                  formula ->
+                      itpForwardQuantifierEliminated.toString().contains(formula.toString()))) {
+            return itpForwardQuantifierEliminated;
+          }
+          throw new SolverException(
+              "Quantifier elimination failed. "
+                  + "Shared variables were accidentally deleted during the process.");
+        }
+        throw new SolverException(
+            "Quantifier elimination failed. "
+                + "Resulting interpolant still contains quantifiers.");
+      } catch (UnsupportedOperationException e) {
+        throw new UnsupportedOperationException(
+            "Solver does not support the complete theory of quantifiers.", e);
+      } catch (InterruptedException e) {
+        throw new InterruptedException();
+      }
+    }
+
+    return itpForward;
+  }
+
+  /**
+   * Identifies all variables present in a set of formulas.
+   *
+   * @param formulas The set of formulas combined into one {@link BooleanFormula} from which all
+   *     variables will be identified.
+   * @return An {@link ImmutableList} containing all variables found in the given set of formulas.
+   */
+  private ImmutableList<Formula> getVars(BooleanFormula formulas) {
+    return ImmutableList.copyOf(mgr.extractVariablesAndUFs(formulas).values());
+  }
+
+  /**
+   * Identifies the shared variables between two sets of {@link BooleanFormula}s A and B.
+   *
+   * @param varsOfA A list of all variables in formulas of A.
+   * @param varsOfB A list of all variables in formulas of B.
+   * @return An {@link ImmutableList} of all variables found in both sets of formulas A and B.
+   */
+  private ImmutableList<Formula> getSharedVars(List<Formula> varsOfA, List<Formula> varsOfB) {
+    return varsOfA.stream().filter(varsOfB::contains).collect(ImmutableList.toImmutableList());
+  }
+
+  /**
+   * Determines the variables bound to a quantifier in a quantified set of formulas used for the
+   * quantifier-based interpolation strategy. These variables appear only in one set of formulas
+   * (either A or B) and can be safely removed by quantifier elimination.
+   *
+   * @param vars A list of variables in the set of formulas to determine the bound variables.
+   * @param sharedVars A list of variables found in both sets of formulas A and B.
+   * @return An {@link ImmutableList} of bound variables, returns an empty list if these variables
+   *     appear in both sets of formulas A and B.
+   */
+  private ImmutableList<Formula> getBoundVars(List<Formula> vars, List<Formula> sharedVars) {
+    return vars.stream()
+        .filter(var -> !sharedVars.contains(var))
+        .collect(ImmutableList.toImmutableList());
+  }
+
+  /**
+   * Declares and calls an uninterpreted function with a unique identifier to generate interpolants.
+   *
+   * @param sharedVars A list of variables found in both sets of formulas A and B.
+   * @return An uninterpreted function with the {@code sharedVars} as symbols
+   */
+  private BooleanFormula getUniqueInterpolant(ImmutableList<Formula> sharedVars) {
+    return ufmgr.declareAndCallUF(
+        PREFIX + UNIQUE_ID_GENERATOR.getFreshId(), FormulaType.BooleanType, sharedVars);
+  }
+
+  /**
+   * Create a new, distinct prover to interpolate on. The set of formulas for interpolation will
+   * need to be translated to and from this new {@link ProverEnvironment} instance.
+   *
+   * @return A new {@link ProverEnvironment} configured to generate models.
+   */
+  private ProverEnvironment getDistinctProver() {
+    return solverContext.newProverEnvironment(ProverOptions.GENERATE_MODELS);
+  }
+
+  /**
+   * Checks, whether the returned interpolant indeed satisfies Craig interpolation.
+   *
+   * @param itp The given interpolant to check if it satisfies the definition of Craig interpolants.
+   * @param formulasOfA The set of formulas A, combined into one {@link BooleanFormula}.
+   * @param formulasOfB The set of formulas B, combined into one {@link BooleanFormula}.
+   * @param sharedVars A list of variables found in both sets of formulas A and B.
+   * @return {@code true}, if the given interpolant is a valid Craig interpolant, returns {@code
+   *     false} otherwise.
+   */
+  private boolean satisfiesInterpolationCriteria(
+      BooleanFormula itp,
+      BooleanFormula formulasOfA,
+      BooleanFormula formulasOfB,
+      List<Formula> sharedVars)
+      throws SolverException, InterruptedException {
+
+    boolean result = false;
+
+    try (ProverEnvironment validationProver = getDistinctProver()) {
+      // the implication A -> Itp holds
+      validationProver.push(bmgr.implication(formulasOfA, itp));
+      if (validationProver.isUnsat()) {
+        return false;
+      }
+      pop();
+
+      // the conjunction Itp /\ B is unsatisfiable
+      validationProver.push(bmgr.and(itp, formulasOfB));
+      if (!validationProver.isUnsat()) {
+        return false;
+      }
+      pop();
+
+      // Itp only contains symbols that occur in both A and B
+      List<Formula> varsOfItp = getVars(itp);
+      if (new HashSet<>(sharedVars).containsAll(varsOfItp)) {
+        return true;
+      }
+    } catch (IllegalArgumentException e) {
+      throw new IllegalArgumentException("Failure when validating interpolant.", e);
+    }
+
+    return result;
+  }
+
+  @Override
+  protected void popImpl() {
+    delegate.pop();
+  }
+
+  @SuppressWarnings("unchecked")
+  @Override
+  protected @Nullable F addConstraintImpl(BooleanFormula constraint) throws InterruptedException {
+    checkState(!closed);
+    Object itpPoint = delegate.addConstraint(constraint);
+    if (itpPoint == null) {
+      return creator.extractInfo(constraint);
+    }
+    return (F) itpPoint;
+  }
+
+  @Override
+  protected void pushImpl() throws InterruptedException {
+    delegate.push();
+  }
+
+  @Override
+  public int size() {
+    return delegate.size();
+  }
+
+  @Override
+  public boolean isUnsat() throws SolverException, InterruptedException {
+    return delegate.isUnsat();
+  }
+
+  @Override
+  public boolean isUnsatWithAssumptions(Collection<BooleanFormula> assumptions)
+      throws SolverException, InterruptedException {
+    return delegate.isUnsatWithAssumptions(assumptions);
+  }
+
+  @Override
+  public Model getModel() throws SolverException {
+    return delegate.getModel();
+  }
+
+  @Override
+  public List<BooleanFormula> getUnsatCore() {
+    return delegate.getUnsatCore();
+  }
+
+  @Override
+  public Optional<List<BooleanFormula>> unsatCoreOverAssumptions(
+      Collection<BooleanFormula> assumptions) throws SolverException, InterruptedException {
+    return delegate.unsatCoreOverAssumptions(assumptions);
+  }
+
+  @Override
+  public void close() {
+    delegate.close();
+  }
+
+  @Override
+  public <R> R allSat(AllSatCallback<R> callback, List<BooleanFormula> important)
+      throws InterruptedException, SolverException {
+    return delegate.allSat(callback, important);
+  }
+}
diff --git a/src/org/sosy_lab/java_smt/example/IndependentInterpolation.java b/src/org/sosy_lab/java_smt/example/IndependentInterpolation.java
new file mode 100644
index 0000000000..4ecc1f3c99
--- /dev/null
+++ b/src/org/sosy_lab/java_smt/example/IndependentInterpolation.java
@@ -0,0 +1,111 @@
+/*
+ * This file is part of JavaSMT,
+ * an API wrapper for a collection of SMT solvers:
+ * https://github.com/sosy-lab/java-smt
+ *
+ * SPDX-FileCopyrightText: 2024 Dirk Beyer <https://www.sosy-lab.org>
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ */
+
+package org.sosy_lab.java_smt.example;
+
+import com.google.common.base.Preconditions;
+import com.google.common.collect.ImmutableList;
+import java.util.logging.Level;
+import org.sosy_lab.common.ShutdownNotifier;
+import org.sosy_lab.common.configuration.Configuration;
+import org.sosy_lab.common.configuration.InvalidConfigurationException;
+import org.sosy_lab.common.log.BasicLogManager;
+import org.sosy_lab.common.log.LogManager;
+import org.sosy_lab.java_smt.SolverContextFactory;
+import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
+import org.sosy_lab.java_smt.api.BooleanFormula;
+import org.sosy_lab.java_smt.api.BooleanFormulaManager;
+import org.sosy_lab.java_smt.api.IntegerFormulaManager;
+import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment;
+import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
+import org.sosy_lab.java_smt.api.SolverContext;
+import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
+import org.sosy_lab.java_smt.api.SolverException;
+
+/** Examples for using independent interpolation procedures. */
+@SuppressWarnings("unused")
+public class IndependentInterpolation {
+
+  private IndependentInterpolation() {
+    // never called
+  }
+
+  public static void main(String... args)
+      throws InvalidConfigurationException, SolverException, InterruptedException {
+
+    // set up a basic environment
+    Configuration config = Configuration.defaultConfiguration();
+    LogManager logger = BasicLogManager.create(config);
+    ShutdownNotifier notifier = ShutdownNotifier.createDummy();
+
+    // choose solver
+    Solvers solver = Solvers.Z3;
+
+    // setup context
+    try (SolverContext context =
+            SolverContextFactory.createSolverContext(config, logger, notifier, solver);
+        InterpolatingProverEnvironment<?> prover =
+            context.newProverEnvironmentWithInterpolation(
+                ProverOptions.GENERATE_UNIFORM_BACKWARD_INTERPOLANTS)) {
+      logger.log(Level.WARNING, "Using solver " + solver + " in version " + context.getVersion());
+
+      BooleanFormulaManager bmgr = context.getFormulaManager().getBooleanFormulaManager();
+      IntegerFormulaManager imgr = context.getFormulaManager().getIntegerFormulaManager();
+
+      // example
+      prover.push();
+      interpolateExample(prover, bmgr, imgr, logger);
+      prover.pop();
+
+    } catch (InvalidConfigurationException | UnsatisfiedLinkError e) {
+
+      // on some machines we support only some solvers,
+      // thus we can ignore these errors.
+      logger.logUserException(Level.INFO, e, "Solver " + solver + " is not available.");
+
+    } catch (UnsupportedOperationException e) {
+      logger.logUserException(Level.INFO, e, e.getMessage());
+    }
+  }
+
+  private static <T> void interpolateExample(
+      InterpolatingProverEnvironment<T> prover,
+      BooleanFormulaManager bmgr,
+      IntegerFormulaManager imgr,
+      LogManager logger)
+      throws InterruptedException, SolverException {
+
+    // create some variables
+    IntegerFormula x = imgr.makeVariable("x");
+    IntegerFormula y = imgr.makeVariable("y");
+    IntegerFormula zero = imgr.makeNumber(0);
+    IntegerFormula two = imgr.makeNumber(2);
+
+    // create and assert some formulas
+    // instead of 'named' formulas, we return a 'handle' (of generic type T)
+
+    // A := (x = 0)
+    T ip0 = prover.push(imgr.equal(x, zero));
+    // B := (y = x + 2) AND (y % 2 != 0)
+    T ip1 =
+        prover.push(
+            bmgr.and(
+                imgr.equal(y, imgr.add(x, two)), bmgr.not(imgr.equal(imgr.modulo(y, two), zero))));
+
+    // check for satisfiability
+    boolean unsat = prover.isUnsat();
+    Preconditions.checkState(unsat, "The example for interpolation should be UNSAT");
+
+    assert ip0 != null;
+    assert ip1 != null;
+    BooleanFormula itp = prover.getInterpolant(ImmutableList.of(ip0, ip1));
+    logger.log(Level.INFO, "Interpolants are:", itp);
+  }
+}
diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaSolverContext.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaSolverContext.java
index 3b2d83bbce..5e6d64b65e 100644
--- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaSolverContext.java
+++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaSolverContext.java
@@ -8,6 +8,7 @@
 
 package org.sosy_lab.java_smt.solvers.bitwuzla;
 
+import static org.sosy_lab.java_smt.basicimpl.IndependentInterpolatingProverEnvironment.hasIndependentInterpolationStrategy;
 import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.BV_SOLVER;
 import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.DBG_CHECK_MODEL;
 import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.DBG_CHECK_UNSAT_CORE;
@@ -69,6 +70,7 @@
 import org.sosy_lab.java_smt.api.OptimizationProverEnvironment;
 import org.sosy_lab.java_smt.api.ProverEnvironment;
 import org.sosy_lab.java_smt.basicimpl.AbstractSolverContext;
+import org.sosy_lab.java_smt.basicimpl.IndependentInterpolatingProverEnvironment;
 import org.sosy_lab.java_smt.solvers.bitwuzla.api.BitwuzlaNative;
 import org.sosy_lab.java_smt.solvers.bitwuzla.api.Option;
 import org.sosy_lab.java_smt.solvers.bitwuzla.api.Options;
@@ -281,10 +283,19 @@ protected ProverEnvironment newProverEnvironment0(Set<ProverOptions> options) {
     return new BitwuzlaTheoremProver(manager, creator, shutdownNotifier, options, solverOptions);
   }
 
+  @SuppressWarnings("resource")
   @Override
   protected InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolation0(
-      Set<ProverOptions> pF) {
-    throw new UnsupportedOperationException("Bitwuzla does not support interpolation");
+      Set<ProverOptions> options) {
+    Preconditions.checkState(!closed, "solver context is already closed");
+    if (!hasIndependentInterpolationStrategy(options, manager)) {
+      throw new UnsupportedOperationException(
+          "Bitwuzla does not support interpolation natively. Try "
+              + "using the independent interpolation options GENERATE_MODEL_BASED_INTERPOLANTS,"
+              + " GENERATE_UNIFORM_BACKWARD_INTERPOLANTS, GENERATE_UNIFORM_FORWARD_INTERPOLANTS.");
+    }
+    return new IndependentInterpolatingProverEnvironment<>(
+        this, creator, newProverEnvironment0(options), options);
   }
 
   @Override
diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaTheoremProver.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaTheoremProver.java
index 56ea0f8d2c..0a58321d5d 100644
--- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaTheoremProver.java
+++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaTheoremProver.java
@@ -55,7 +55,7 @@ protected BitwuzlaTheoremProver(
       ShutdownNotifier pShutdownNotifier,
       Set<ProverOptions> pOptions,
       Options pSolverOptions) {
-    super(pOptions, pManager.getBooleanFormulaManager(), pShutdownNotifier);
+    super(pOptions, pManager, pShutdownNotifier);
     manager = pManager;
     creator = pCreator;
 
diff --git a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorAbstractProver.java b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorAbstractProver.java
index 1608cc098c..5cd081f1dd 100644
--- a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorAbstractProver.java
+++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorAbstractProver.java
@@ -45,7 +45,7 @@ protected BoolectorAbstractProver(
       ShutdownNotifier pShutdownNotifier,
       Set<ProverOptions> pOptions,
       AtomicBoolean pIsAnyStackAlive) {
-    super(pOptions, manager.getBooleanFormulaManager(), pShutdownNotifier);
+    super(pOptions, manager, pShutdownNotifier);
     this.manager = manager;
     this.creator = creator;
     this.btor = btor;
diff --git a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorSolverContext.java b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorSolverContext.java
index 6c90828e93..fc7f4ed4e6 100644
--- a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorSolverContext.java
+++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorSolverContext.java
@@ -8,6 +8,8 @@
 
 package org.sosy_lab.java_smt.solvers.boolector;
 
+import static org.sosy_lab.java_smt.basicimpl.IndependentInterpolatingProverEnvironment.hasIndependentInterpolationStrategy;
+
 import com.google.common.base.Preconditions;
 import com.google.common.base.Splitter;
 import com.google.common.base.Splitter.MapSplitter;
@@ -29,6 +31,7 @@
 import org.sosy_lab.java_smt.api.OptimizationProverEnvironment;
 import org.sosy_lab.java_smt.api.ProverEnvironment;
 import org.sosy_lab.java_smt.basicimpl.AbstractSolverContext;
+import org.sosy_lab.java_smt.basicimpl.IndependentInterpolatingProverEnvironment;
 
 public final class BoolectorSolverContext extends AbstractSolverContext {
 
@@ -204,10 +207,19 @@ protected ProverEnvironment newProverEnvironment0(Set<ProverOptions> pOptions) {
         manager, creator, creator.getEnv(), shutdownNotifier, pOptions, isAnyStackAlive);
   }
 
+  @SuppressWarnings("resource")
   @Override
   protected InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolation0(
-      Set<ProverOptions> pSet) {
-    throw new UnsupportedOperationException("Boolector does not support interpolation");
+      Set<ProverOptions> options) {
+    Preconditions.checkState(!closed, "solver context is already closed");
+    if (!hasIndependentInterpolationStrategy(options, manager)) {
+      throw new UnsupportedOperationException(
+          "Boolector does not support interpolation natively. Try "
+              + "using the independent interpolation options GENERATE_MODEL_BASED_INTERPOLANTS,"
+              + " GENERATE_UNIFORM_BACKWARD_INTERPOLANTS, GENERATE_UNIFORM_FORWARD_INTERPOLANTS.");
+    }
+    return new IndependentInterpolatingProverEnvironment<>(
+        this, creator, newProverEnvironment0(options), options);
   }
 
   @Override
diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4SolverContext.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4SolverContext.java
index b5bd086812..35e826a811 100644
--- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4SolverContext.java
+++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4SolverContext.java
@@ -8,6 +8,8 @@
 
 package org.sosy_lab.java_smt.solvers.cvc4;
 
+import static org.sosy_lab.java_smt.basicimpl.IndependentInterpolatingProverEnvironment.hasIndependentInterpolationStrategy;
+
 import edu.stanford.CVC4.CVC4JNI;
 import edu.stanford.CVC4.Configuration;
 import edu.stanford.CVC4.ExprManager;
@@ -26,6 +28,7 @@
 import org.sosy_lab.java_smt.api.SolverContext;
 import org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager.NonLinearArithmetic;
 import org.sosy_lab.java_smt.basicimpl.AbstractSolverContext;
+import org.sosy_lab.java_smt.basicimpl.IndependentInterpolatingProverEnvironment;
 
 public final class CVC4SolverContext extends AbstractSolverContext {
 
@@ -130,11 +133,7 @@ public Solvers getSolverName() {
   @Override
   public ProverEnvironment newProverEnvironment0(Set<ProverOptions> pOptions) {
     return new CVC4TheoremProver(
-        creator,
-        shutdownNotifier,
-        randomSeed,
-        pOptions,
-        getFormulaManager().getBooleanFormulaManager());
+        creator, shutdownNotifier, randomSeed, pOptions, getFormulaManager());
   }
 
   @Override
@@ -142,10 +141,18 @@ protected boolean supportsAssumptionSolving() {
     return false;
   }
 
+  @SuppressWarnings("resource")
   @Override
   protected InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolation0(
-      Set<ProverOptions> pSet) {
-    throw new UnsupportedOperationException("CVC4 does not support interpolation");
+      Set<ProverOptions> options) {
+    if (!hasIndependentInterpolationStrategy(options, getFormulaManager())) {
+      throw new UnsupportedOperationException(
+          "CVC4 does not support interpolation natively. Try "
+              + "using the independent interpolation options GENERATE_MODEL_BASED_INTERPOLANTS,"
+              + " GENERATE_UNIFORM_BACKWARD_INTERPOLANTS, GENERATE_UNIFORM_FORWARD_INTERPOLANTS.");
+    }
+    return new IndependentInterpolatingProverEnvironment<>(
+        this, creator, newProverEnvironment0(options), options);
   }
 
   @Override
diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java
index 94b7f0dd15..cbca037811 100644
--- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java
+++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java
@@ -22,12 +22,11 @@
 import java.util.List;
 import java.util.Optional;
 import java.util.Set;
-import org.checkerframework.checker.nullness.qual.Nullable;
 import org.sosy_lab.common.ShutdownNotifier;
 import org.sosy_lab.java_smt.api.BasicProverEnvironment;
 import org.sosy_lab.java_smt.api.BooleanFormula;
-import org.sosy_lab.java_smt.api.BooleanFormulaManager;
 import org.sosy_lab.java_smt.api.Evaluator;
+import org.sosy_lab.java_smt.api.FormulaManager;
 import org.sosy_lab.java_smt.api.Model.ValueAssignment;
 import org.sosy_lab.java_smt.api.ProverEnvironment;
 import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
@@ -62,8 +61,8 @@ protected CVC4TheoremProver(
       ShutdownNotifier pShutdownNotifier,
       int randomSeed,
       Set<ProverOptions> pOptions,
-      BooleanFormulaManager pBmgr) {
-    super(pOptions, pBmgr, pShutdownNotifier);
+      FormulaManager pMgr) {
+    super(pOptions, pMgr, pShutdownNotifier);
 
     creator = pFormulaCreator;
     smtEngine = new SmtEngine(exprManager);
@@ -123,7 +122,7 @@ protected void popImpl() {
   }
 
   @Override
-  protected @Nullable Void addConstraintImpl(BooleanFormula pF) throws InterruptedException {
+  protected Void addConstraintImpl(BooleanFormula pF) throws InterruptedException {
     Preconditions.checkState(!closed);
     setChanged();
     Expr exp = creator.extractInfo(pF);
diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java
index 32e83314b1..22669792dd 100644
--- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java
+++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java
@@ -55,7 +55,7 @@ protected CVC5AbstractProver(
       @SuppressWarnings("unused") int randomSeed,
       Set<ProverOptions> pOptions,
       FormulaManager pMgr) {
-    super(pOptions, pMgr.getBooleanFormulaManager(), pShutdownNotifier);
+    super(pOptions, pMgr, pShutdownNotifier);
 
     mgr = pMgr;
     creator = pFormulaCreator;
diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java
index 3e8cd0f5e9..e2b9bd6931 100644
--- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java
+++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java
@@ -27,6 +27,7 @@
 import org.sosy_lab.java_smt.api.SolverContext;
 import org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager.NonLinearArithmetic;
 import org.sosy_lab.java_smt.basicimpl.AbstractSolverContext;
+import org.sosy_lab.java_smt.basicimpl.IndependentInterpolatingProverEnvironment;
 
 public final class CVC5SolverContext extends AbstractSolverContext {
 
@@ -190,17 +191,22 @@ protected boolean supportsAssumptionSolving() {
     return false;
   }
 
+  @SuppressWarnings("resource")
   @Override
   protected InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolation0(
-      Set<ProverOptions> pOptions) {
+      Set<ProverOptions> options) {
     Preconditions.checkState(!closed, "solver context is already closed");
-    return new CVC5InterpolatingProver(
-        creator,
-        shutdownNotifier,
-        randomSeed,
-        pOptions,
-        getFormulaManager(),
-        settings.validateInterpolants);
+
+    CVC5InterpolatingProver itpProver =
+        new CVC5InterpolatingProver(
+            creator,
+            shutdownNotifier,
+            randomSeed,
+            options,
+            getFormulaManager(),
+            settings.validateInterpolants);
+
+    return new IndependentInterpolatingProverEnvironment<>(this, creator, itpProver, options);
   }
 
   @Override
diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5OptimizationProver.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5OptimizationProver.java
index dc7fc69436..1c550589d6 100644
--- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5OptimizationProver.java
+++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5OptimizationProver.java
@@ -27,7 +27,6 @@
 import java.util.Map;
 import java.util.Optional;
 import java.util.Set;
-import org.checkerframework.checker.nullness.qual.Nullable;
 import org.sosy_lab.common.ShutdownNotifier;
 import org.sosy_lab.common.UniqueIdGenerator;
 import org.sosy_lab.common.collect.PathCopyingPersistentTreeMap;
@@ -69,7 +68,6 @@ protected void createConfig(Map<String, String> pConfig) {
   }
 
   @Override
-  @Nullable
   protected Void addConstraintImpl(BooleanFormula constraint) throws InterruptedException {
     msat_assert_formula(curEnv, getMsatTerm(constraint));
     return null;
diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java
index 3eff520873..0784322500 100644
--- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java
+++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java
@@ -46,6 +46,7 @@
 import org.sosy_lab.java_smt.api.ProverEnvironment;
 import org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager.NonLinearArithmetic;
 import org.sosy_lab.java_smt.basicimpl.AbstractSolverContext;
+import org.sosy_lab.java_smt.basicimpl.IndependentInterpolatingProverEnvironment;
 import org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.TerminationCallback;
 
 public final class Mathsat5SolverContext extends AbstractSolverContext {
@@ -265,11 +266,16 @@ protected ProverEnvironment newProverEnvironment0(Set<ProverOptions> options) {
     return new Mathsat5TheoremProver(this, shutdownNotifier, creator, options);
   }
 
+  @SuppressWarnings("resource")
   @Override
   protected InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolation0(
       Set<ProverOptions> options) {
     Preconditions.checkState(!closed, "solver context is already closed");
-    return new Mathsat5InterpolatingProver(this, shutdownNotifier, creator, options);
+    return new IndependentInterpolatingProverEnvironment<>(
+        this,
+        creator,
+        new Mathsat5InterpolatingProver(this, shutdownNotifier, creator, options),
+        options);
   }
 
   @Override
diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5TheoremProver.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5TheoremProver.java
index 4801c5904f..6b0c05ac75 100644
--- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5TheoremProver.java
+++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5TheoremProver.java
@@ -14,7 +14,6 @@
 import com.google.common.base.Preconditions;
 import java.util.Map;
 import java.util.Set;
-import org.checkerframework.checker.nullness.qual.Nullable;
 import org.sosy_lab.common.ShutdownNotifier;
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.ProverEnvironment;
@@ -36,7 +35,6 @@ protected void createConfig(Map<String, String> pConfig) {
   }
 
   @Override
-  @Nullable
   protected Void addConstraintImpl(BooleanFormula constraint) throws InterruptedException {
     Preconditions.checkState(!closed);
     closeAllEvaluators();
diff --git a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java
index 34960c0640..9ff329db99 100644
--- a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java
+++ b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java
@@ -54,7 +54,7 @@ protected OpenSmtAbstractProver(
       ShutdownNotifier pShutdownNotifier,
       SMTConfig pConfig,
       Set<ProverOptions> pOptions) {
-    super(pOptions, pMgr.getBooleanFormulaManager(), pShutdownNotifier);
+    super(pOptions, pMgr, pShutdownNotifier);
 
     creator = pFormulaCreator;
 
diff --git a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtSolverContext.java b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtSolverContext.java
index 0a6e86f3c3..a9638ff41d 100644
--- a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtSolverContext.java
+++ b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtSolverContext.java
@@ -24,6 +24,7 @@
 import org.sosy_lab.java_smt.api.SolverContext;
 import org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager.NonLinearArithmetic;
 import org.sosy_lab.java_smt.basicimpl.AbstractSolverContext;
+import org.sosy_lab.java_smt.basicimpl.IndependentInterpolatingProverEnvironment;
 import org.sosy_lab.java_smt.solvers.opensmt.api.LogicFactory;
 
 public class OpenSmtSolverContext extends AbstractSolverContext {
@@ -143,12 +144,16 @@ protected ProverEnvironment newProverEnvironment0(
         creator, manager, shutdownNotifier, pProverOptions, solverOptions);
   }
 
+  @SuppressWarnings("resource")
   @Override
   protected InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolation0(
-      Set<SolverContext.ProverOptions> pProverOptions) {
+      Set<SolverContext.ProverOptions> options) {
     Preconditions.checkState(!closed, "solver context is already closed");
-    return new OpenSmtInterpolatingProver(
-        creator, manager, shutdownNotifier, pProverOptions, solverOptions);
+    return new IndependentInterpolatingProverEnvironment<>(
+        this,
+        creator,
+        new OpenSmtInterpolatingProver(creator, manager, shutdownNotifier, options, solverOptions),
+        options);
   }
 
   @Override
diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java
index d475a00284..86adaa68a4 100644
--- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java
+++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java
@@ -59,7 +59,7 @@ protected PrincessAbstractProver(
       SimpleAPI pApi,
       ShutdownNotifier pShutdownNotifier,
       Set<ProverOptions> pOptions) {
-    super(pOptions, pMgr.getBooleanFormulaManager(), pShutdownNotifier);
+    super(pOptions, pMgr, pShutdownNotifier);
     this.mgr = pMgr;
     this.creator = creator;
     this.api = checkNotNull(pApi);
diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessSolverContext.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessSolverContext.java
index 36a7444539..07583599ab 100644
--- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessSolverContext.java
+++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessSolverContext.java
@@ -22,6 +22,7 @@
 import org.sosy_lab.java_smt.api.SolverContext;
 import org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager.NonLinearArithmetic;
 import org.sosy_lab.java_smt.basicimpl.AbstractSolverContext;
+import org.sosy_lab.java_smt.basicimpl.IndependentInterpolatingProverEnvironment;
 
 public final class PrincessSolverContext extends AbstractSolverContext {
 
@@ -81,8 +82,12 @@ protected ProverEnvironment newProverEnvironment0(Set<ProverOptions> options) {
   @Override
   protected InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolation0(
       Set<ProverOptions> options) {
-    return (PrincessInterpolatingProver)
-        creator.getEnv().getNewProver(true, manager, creator, options);
+
+    PrincessInterpolatingProver itpProver =
+        (PrincessInterpolatingProver)
+            creator.getEnv().getNewProver(true, manager, creator, options);
+
+    return new IndependentInterpolatingProverEnvironment<>(this, creator, itpProver, options);
   }
 
   @Override
diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessTheoremProver.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessTheoremProver.java
index ab087b3389..1a45cfc954 100644
--- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessTheoremProver.java
+++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessTheoremProver.java
@@ -10,7 +10,6 @@
 
 import ap.api.SimpleAPI;
 import java.util.Set;
-import org.checkerframework.checker.nullness.qual.Nullable;
 import org.sosy_lab.common.ShutdownNotifier;
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.ProverEnvironment;
@@ -28,7 +27,6 @@ class PrincessTheoremProver extends PrincessAbstractProver<Void> implements Prov
   }
 
   @Override
-  @Nullable
   protected Void addConstraintImpl(BooleanFormula constraint) throws InterruptedException {
     addConstraint0(constraint);
     return null;
diff --git a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolSolverContext.java b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolSolverContext.java
index e9620756df..36d982a800 100644
--- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolSolverContext.java
+++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolSolverContext.java
@@ -42,6 +42,7 @@
 import org.sosy_lab.java_smt.api.ProverEnvironment;
 import org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager.NonLinearArithmetic;
 import org.sosy_lab.java_smt.basicimpl.AbstractSolverContext;
+import org.sosy_lab.java_smt.basicimpl.IndependentInterpolatingProverEnvironment;
 
 public final class SmtInterpolSolverContext extends AbstractSolverContext {
 
@@ -235,6 +236,7 @@ protected ProverEnvironment newProverEnvironment0(Set<ProverOptions> options) {
   @Override
   protected InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolation0(
       Set<ProverOptions> options) {
+
     Script newScript = createNewScript(options);
     final SmtInterpolInterpolatingProver prover;
     if (settings.smtLogfile == null) {
@@ -249,7 +251,8 @@ protected InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolatio
               settings.optionsMap,
               settings.smtLogfile.getFreshPath());
     }
-    return prover;
+
+    return new IndependentInterpolatingProverEnvironment<>(this, prover.creator, prover, options);
   }
 
   @Override
diff --git a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolTheoremProver.java b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolTheoremProver.java
index bfb524f0a4..c7a3126fb1 100644
--- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolTheoremProver.java
+++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolTheoremProver.java
@@ -10,7 +10,6 @@
 
 import de.uni_freiburg.informatik.ultimate.logic.Script;
 import java.util.Set;
-import org.checkerframework.checker.nullness.qual.Nullable;
 import org.sosy_lab.common.ShutdownNotifier;
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.ProverEnvironment;
@@ -28,7 +27,6 @@ class SmtInterpolTheoremProver extends SmtInterpolAbstractProver<Void>
   }
 
   @Override
-  @Nullable
   protected Void addConstraintImpl(BooleanFormula constraint) throws InterruptedException {
     addConstraint0(constraint);
     return null;
diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2QuantifiedFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2QuantifiedFormulaManager.java
index 957d078f9b..982d54f5dd 100644
--- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2QuantifiedFormulaManager.java
+++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2QuantifiedFormulaManager.java
@@ -17,6 +17,7 @@
 import org.sosy_lab.java_smt.basicimpl.AbstractQuantifiedFormulaManager;
 import org.sosy_lab.java_smt.basicimpl.FormulaCreator;
 
+@SuppressWarnings("unused")
 public class Yices2QuantifiedFormulaManager
     extends AbstractQuantifiedFormulaManager<Integer, Integer, Long, Integer> {
 
@@ -28,7 +29,6 @@ protected Yices2QuantifiedFormulaManager(
   @Override
   protected Integer eliminateQuantifiers(Integer pExtractInfo)
       throws SolverException, InterruptedException {
-    // TODO Auto-generated method stub
     throw new UnsupportedOperationException("Yices does not support eliminating Quantifiers.");
   }
 
diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2SolverContext.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2SolverContext.java
index c68e90aa3c..01b28ab863 100644
--- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2SolverContext.java
+++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2SolverContext.java
@@ -8,6 +8,7 @@
 
 package org.sosy_lab.java_smt.solvers.yices2;
 
+import static org.sosy_lab.java_smt.basicimpl.IndependentInterpolatingProverEnvironment.hasIndependentInterpolationStrategy;
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_exit;
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_get_major_version;
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_get_patch_level;
@@ -18,31 +19,28 @@
 import java.util.function.Consumer;
 import org.sosy_lab.common.ShutdownNotifier;
 import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
-import org.sosy_lab.java_smt.api.BooleanFormulaManager;
 import org.sosy_lab.java_smt.api.FormulaManager;
 import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment;
 import org.sosy_lab.java_smt.api.OptimizationProverEnvironment;
 import org.sosy_lab.java_smt.api.ProverEnvironment;
 import org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager.NonLinearArithmetic;
 import org.sosy_lab.java_smt.basicimpl.AbstractSolverContext;
+import org.sosy_lab.java_smt.basicimpl.IndependentInterpolatingProverEnvironment;
 
 public class Yices2SolverContext extends AbstractSolverContext {
 
   private final Yices2FormulaCreator creator;
-  private final BooleanFormulaManager bfmgr;
+  private final FormulaManager fmgr;
   private final ShutdownNotifier shutdownManager;
 
   private static int numLoadedInstances = 0;
   private boolean closed = false;
 
   public Yices2SolverContext(
-      FormulaManager pFmgr,
-      Yices2FormulaCreator creator,
-      BooleanFormulaManager pBfmgr,
-      ShutdownNotifier pShutdownManager) {
+      FormulaManager pFmgr, Yices2FormulaCreator creator, ShutdownNotifier pShutdownManager) {
     super(pFmgr);
+    fmgr = pFmgr;
     this.creator = creator;
-    bfmgr = pBfmgr;
     shutdownManager = pShutdownManager;
   }
 
@@ -72,10 +70,15 @@ public static Yices2SolverContext create(
         new Yices2IntegerFormulaManager(creator, pNonLinearArithmetic);
     Yices2RationalFormulaManager rationalTheory =
         new Yices2RationalFormulaManager(creator, pNonLinearArithmetic);
+    /*
+    Yices2QuantifiedFormulaManager quantifiedFormulaManager =
+        new Yices2QuantifiedFormulaManager(creator);*/
+    // TODO: investigate Yices2 quantifier problems
+
     Yices2FormulaManager manager =
         new Yices2FormulaManager(
             creator, functionTheory, booleanTheory, integerTheory, rationalTheory, bitvectorTheory);
-    return new Yices2SolverContext(manager, creator, booleanTheory, pShutdownManager);
+    return new Yices2SolverContext(manager, creator, pShutdownManager);
   }
 
   @Override
@@ -104,13 +107,21 @@ public synchronized void close() {
 
   @Override
   protected ProverEnvironment newProverEnvironment0(Set<ProverOptions> pOptions) {
-    return new Yices2TheoremProver(creator, pOptions, bfmgr, shutdownManager);
+    return new Yices2TheoremProver(creator, pOptions, fmgr, shutdownManager);
   }
 
+  @SuppressWarnings("resource")
   @Override
   protected InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolation0(
-      Set<ProverOptions> pSet) {
-    throw new UnsupportedOperationException("Yices does not support interpolation");
+      Set<ProverOptions> options) {
+    if (!hasIndependentInterpolationStrategy(options, getFormulaManager())) {
+      throw new UnsupportedOperationException(
+          "Yices2 does not support interpolation natively. Try "
+              + "using the independent interpolation options GENERATE_MODEL_BASED_INTERPOLANTS,"
+              + " GENERATE_UNIFORM_BACKWARD_INTERPOLANTS, GENERATE_UNIFORM_FORWARD_INTERPOLANTS.");
+    }
+    return new IndependentInterpolatingProverEnvironment<>(
+        this, creator, newProverEnvironment0(options), options);
   }
 
   @Override
diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2TheoremProver.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2TheoremProver.java
index 30b6eda2a5..f73b25a322 100644
--- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2TheoremProver.java
+++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2TheoremProver.java
@@ -31,10 +31,9 @@
 import java.util.Optional;
 import java.util.Set;
 import java.util.stream.Collectors;
-import org.checkerframework.checker.nullness.qual.Nullable;
 import org.sosy_lab.common.ShutdownNotifier;
 import org.sosy_lab.java_smt.api.BooleanFormula;
-import org.sosy_lab.java_smt.api.BooleanFormulaManager;
+import org.sosy_lab.java_smt.api.FormulaManager;
 import org.sosy_lab.java_smt.api.Model;
 import org.sosy_lab.java_smt.api.ProverEnvironment;
 import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
@@ -70,9 +69,9 @@ class Yices2TheoremProver extends AbstractProverWithAllSat<Void> implements Prov
   protected Yices2TheoremProver(
       Yices2FormulaCreator creator,
       Set<ProverOptions> pOptions,
-      BooleanFormulaManager pBmgr,
+      FormulaManager pMgr,
       ShutdownNotifier pShutdownNotifier) {
-    super(pOptions, pBmgr, pShutdownNotifier);
+    super(pOptions, pMgr, pShutdownNotifier);
     this.creator = creator;
     curCfg = yices_new_config();
     yices_set_config(curCfg, "solver-type", "dpllt");
@@ -94,8 +93,7 @@ protected void popImpl() {
   }
 
   @Override
-  protected @Nullable Void addConstraintImpl(BooleanFormula pConstraint)
-      throws InterruptedException {
+  protected Void addConstraintImpl(BooleanFormula pConstraint) throws InterruptedException {
     if (!generateUnsatCores) { // unsat core does not work with incremental mode
       int constraint = creator.extractInfo(pConstraint);
       yices_assert_formula(curEnv, constraint);
diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java
index e409058777..a0b156a36b 100644
--- a/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java
+++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java
@@ -37,7 +37,7 @@
 import org.sosy_lab.java_smt.basicimpl.AbstractProverWithAllSat;
 import org.sosy_lab.java_smt.basicimpl.CachingModel;
 
-abstract class Z3AbstractProver extends AbstractProverWithAllSat<Void> {
+abstract class Z3AbstractProver<T2> extends AbstractProverWithAllSat<T2> {
 
   protected final Z3FormulaCreator creator;
   protected final long z3context;
@@ -54,7 +54,7 @@ abstract class Z3AbstractProver extends AbstractProverWithAllSat<Void> {
       Set<ProverOptions> pOptions,
       @Nullable PathCounterTemplate pLogfile,
       ShutdownNotifier pShutdownNotifier) {
-    super(pOptions, pMgr.getBooleanFormulaManager(), pShutdownNotifier);
+    super(pOptions, pMgr, pShutdownNotifier);
     creator = pCreator;
     z3context = creator.getEnv();
 
@@ -122,7 +122,7 @@ protected Z3Model getEvaluatorWithoutChecks() {
   protected abstract void assertContraintAndTrack(long constraint, long symbol);
 
   @Override
-  protected Void addConstraintImpl(BooleanFormula f) throws InterruptedException {
+  protected @Nullable T2 addConstraintImpl(BooleanFormula f) throws InterruptedException {
     Preconditions.checkState(!closed);
     long e = creator.extractInfo(f);
     try {
diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3OptimizationProver.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3OptimizationProver.java
index b1eddb2a6b..e44f4f0c0a 100644
--- a/src/org/sosy_lab/java_smt/solvers/z3/Z3OptimizationProver.java
+++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3OptimizationProver.java
@@ -30,7 +30,7 @@
 import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
 import org.sosy_lab.java_smt.api.SolverException;
 
-class Z3OptimizationProver extends Z3AbstractProver implements OptimizationProverEnvironment {
+class Z3OptimizationProver extends Z3AbstractProver<Void> implements OptimizationProverEnvironment {
 
   private final LogManager logger;
   private final long z3optSolver;
diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java
index 7d408faf11..2c569267af 100644
--- a/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java
+++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java
@@ -8,6 +8,8 @@
 
 package org.sosy_lab.java_smt.solvers.z3;
 
+import static org.sosy_lab.java_smt.basicimpl.IndependentInterpolatingProverEnvironment.hasIndependentInterpolationStrategy;
+
 import com.google.common.base.Preconditions;
 import com.google.common.collect.ImmutableList;
 import com.google.common.collect.ImmutableMap;
@@ -16,6 +18,7 @@
 import java.io.IOException;
 import java.nio.charset.StandardCharsets;
 import java.nio.file.Path;
+import java.util.Map;
 import java.util.Set;
 import java.util.function.Consumer;
 import java.util.logging.Level;
@@ -37,6 +40,7 @@
 import org.sosy_lab.java_smt.api.ProverEnvironment;
 import org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager.NonLinearArithmetic;
 import org.sosy_lab.java_smt.basicimpl.AbstractSolverContext;
+import org.sosy_lab.java_smt.basicimpl.IndependentInterpolatingProverEnvironment;
 
 public final class Z3SolverContext extends AbstractSolverContext {
 
@@ -216,26 +220,24 @@ public static synchronized Z3SolverContext create(
   @Override
   protected ProverEnvironment newProverEnvironment0(Set<ProverOptions> options) {
     Preconditions.checkState(!closed, "solver context is already closed");
-    final ImmutableMap<String, Object> solverOptions =
-        ImmutableMap.<String, Object>builder()
-            .put(":random-seed", extraOptions.randomSeed)
-            .put(
-                ":model",
-                options.contains(ProverOptions.GENERATE_MODELS)
-                    || options.contains(ProverOptions.GENERATE_ALL_SAT))
-            .put(
-                ":unsat_core",
-                options.contains(ProverOptions.GENERATE_UNSAT_CORE)
-                    || options.contains(ProverOptions.GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS))
-            .buildOrThrow();
+    final Map<String, Object> solverOptions = buildSolverOptions(options);
     return new Z3TheoremProver(
         creator, manager, options, solverOptions, extraOptions.logfile, shutdownNotifier);
   }
 
+  @SuppressWarnings("resource")
   @Override
   protected InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolation0(
       Set<ProverOptions> options) {
-    throw new UnsupportedOperationException("Z3 does not support interpolation");
+    Preconditions.checkState(!closed, "solver context is already closed");
+    if (!hasIndependentInterpolationStrategy(options, getFormulaManager())) {
+      throw new UnsupportedOperationException(
+          "Z3 does not support interpolation natively. Try "
+              + "using the independent interpolation options GENERATE_MODEL_BASED_INTERPOLANTS,"
+              + " GENERATE_UNIFORM_BACKWARD_INTERPOLANTS, GENERATE_UNIFORM_FORWARD_INTERPOLANTS.");
+    }
+    return new IndependentInterpolatingProverEnvironment<>(
+        this, creator, newProverEnvironment0(options), options);
   }
 
   @Override
@@ -283,4 +285,18 @@ public void close() {
   protected boolean supportsAssumptionSolving() {
     return true;
   }
+
+  private Map<String, Object> buildSolverOptions(Set<ProverOptions> options) {
+    return ImmutableMap.<String, Object>builder()
+        .put(":random-seed", extraOptions.randomSeed)
+        .put(
+            ":model",
+            options.contains(ProverOptions.GENERATE_MODELS)
+                || options.contains(ProverOptions.GENERATE_ALL_SAT))
+        .put(
+            ":unsat_core",
+            options.contains(ProverOptions.GENERATE_UNSAT_CORE)
+                || options.contains(ProverOptions.GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS))
+        .buildOrThrow();
+  }
 }
diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3TheoremProver.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3TheoremProver.java
index 6a1cba2f4f..1fd772eb9d 100644
--- a/src/org/sosy_lab/java_smt/solvers/z3/Z3TheoremProver.java
+++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3TheoremProver.java
@@ -9,11 +9,11 @@
 package org.sosy_lab.java_smt.solvers.z3;
 
 import com.google.common.base.Preconditions;
-import com.google.common.collect.ImmutableMap;
 import com.microsoft.z3.Native;
 import com.microsoft.z3.Z3Exception;
 import com.microsoft.z3.enumerations.Z3_lbool;
 import java.util.Collection;
+import java.util.Map;
 import java.util.Map.Entry;
 import java.util.Set;
 import org.checkerframework.checker.nullness.qual.Nullable;
@@ -25,7 +25,7 @@
 import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
 import org.sosy_lab.java_smt.api.UserPropagator;
 
-class Z3TheoremProver extends Z3AbstractProver implements ProverEnvironment {
+class Z3TheoremProver extends Z3AbstractProver<Void> implements ProverEnvironment {
 
   private final long z3solver;
   private final ShutdownRequestListener interruptListener;
@@ -36,7 +36,7 @@ class Z3TheoremProver extends Z3AbstractProver implements ProverEnvironment {
       Z3FormulaCreator creator,
       Z3FormulaManager pMgr,
       Set<ProverOptions> pOptions,
-      ImmutableMap<String, Object> pSolverOptions,
+      Map<String, Object> pSolverOptions,
       @Nullable PathCounterTemplate pLogfile,
       ShutdownNotifier pShutdownNotifier) {
     super(creator, pMgr, pOptions, pLogfile, pShutdownNotifier);
diff --git a/src/org/sosy_lab/java_smt/test/InterpolatingProverTest.java b/src/org/sosy_lab/java_smt/test/InterpolatingProverTest.java
index 8b4b26b1e5..43364adefa 100644
--- a/src/org/sosy_lab/java_smt/test/InterpolatingProverTest.java
+++ b/src/org/sosy_lab/java_smt/test/InterpolatingProverTest.java
@@ -29,13 +29,15 @@
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment;
 import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
+import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
 import org.sosy_lab.java_smt.api.SolverException;
 import org.sosy_lab.java_smt.solvers.cvc5.CVC5BooleanFormulaManager;
 import org.sosy_lab.java_smt.solvers.opensmt.Logics;
 
 /** This class contains some simple Junit-tests to check the interpolation-API of our solvers. */
 @SuppressWarnings({"resource", "LocalVariableName"})
-public class InterpolatingProverTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 {
+public class InterpolatingProverTest
+    extends SolverBasedTest0.ParameterizedInterpolatingSolverBasedTest0 {
 
   // INFO: OpenSmt only support interpolation for QF_LIA, QF_LRA and QF_UF
   @Override
@@ -46,8 +48,15 @@ protected Logics logicToUse() {
   /** Generate a prover environment depending on the parameter above. */
   @SuppressWarnings("unchecked")
   private <T> InterpolatingProverEnvironment<T> newEnvironmentForTest() {
-    requireInterpolation();
-    return (InterpolatingProverEnvironment<T>) context.newProverEnvironmentWithInterpolation();
+    ProverOptions itpStrat = itpStrategyToUse();
+    requireInterpolation(itpStrategyToUse());
+
+    if (itpStrat == null) {
+      return (InterpolatingProverEnvironment<T>) context.newProverEnvironmentWithInterpolation();
+    } else {
+      return (InterpolatingProverEnvironment<T>)
+          context.newProverEnvironmentWithInterpolation(itpStrat);
+    }
   }
 
   private static final UniqueIdGenerator index = new UniqueIdGenerator(); // to get different names
@@ -55,10 +64,21 @@ private <T> InterpolatingProverEnvironment<T> newEnvironmentForTest() {
   @Test
   @SuppressWarnings("CheckReturnValue")
   public <T> void simpleInterpolation() throws SolverException, InterruptedException {
+    requireInterpolation();
     assume()
         .withMessage("Solver %s runs into timeout on this test", solverToUse())
         .that(solverToUse())
         .isNotEqualTo(Solvers.CVC5);
+    if (interpolationStrategy == ProverOptions.GENERATE_MODEL_BASED_INTERPOLANTS) {
+      assume()
+          .withMessage("Solver %s runs into timeout on this test", solverToUse())
+          .that(solverToUse())
+          .isNoneOf(Solvers.Z3, Solvers.CVC4);
+      assume()
+          .withMessage("Solver %s checkSat call returned Inconclusive", solverToUse())
+          .that(solverToUse())
+          .isNotEqualTo(Solvers.PRINCESS);
+    }
 
     try (InterpolatingProverEnvironment<T> prover = newEnvironmentForTest()) {
       IntegerFormula x = imgr.makeVariable("x");
@@ -88,6 +108,7 @@ public <T> void simpleInterpolation() throws SolverException, InterruptedExcepti
   @Test
   @SuppressWarnings("unchecked")
   public <T> void emptyInterpolationGroup() throws SolverException, InterruptedException {
+    requireIntegers();
     try (InterpolatingProverEnvironment<T> prover = newEnvironmentForTest()) {
       IntegerFormula x = imgr.makeVariable("x");
       IntegerFormula y = imgr.makeVariable("y");
@@ -115,6 +136,7 @@ public <T> void emptyInterpolationGroup() throws SolverException, InterruptedExc
 
   @Test
   public <T> void binaryInterpolation() throws SolverException, InterruptedException {
+    requireIndependentSequentialInterpolation();
     InterpolatingProverEnvironment<T> stack = newEnvironmentForTest();
 
     int i = index.getFreshId();
@@ -164,6 +186,8 @@ public <T> void binaryInterpolation() throws SolverException, InterruptedExcepti
   public <T> void binaryInterpolationWithConstantFalse()
       throws SolverException, InterruptedException {
     InterpolatingProverEnvironment<T> stack = newEnvironmentForTest();
+    requireIndependentInterpolation();
+    requireIndependentInterpolationWithConstantFalse();
 
     // build formula:  [false, false]
     BooleanFormula A = bmgr.makeBoolean(false);
@@ -199,12 +223,20 @@ public <T> void binaryInterpolationWithConstantFalse()
   @Test
   public <T> void binaryBVInterpolation1() throws SolverException, InterruptedException {
     requireBitvectors();
+    requireIndependentSequentialInterpolation();
 
     assume()
         .withMessage("Solver %s runs into timeout on this test", solverToUse())
         .that(solverToUse())
         .isNotEqualTo(Solvers.CVC5);
 
+    if (interpolationStrategy == ProverOptions.GENERATE_MODEL_BASED_INTERPOLANTS) {
+      assume()
+          .withMessage("Solver %s run into timeout on this test", solverToUse())
+          .that(solverToUse())
+          .isNoneOf(Solvers.Z3, Solvers.CVC4, Solvers.BITWUZLA);
+    }
+
     InterpolatingProverEnvironment<T> stack = newEnvironmentForTest();
 
     int i = index.getFreshId();
@@ -258,10 +290,59 @@ private void requireTreeItp() {
         .isAnyOf(Solvers.SMTINTERPOL, Solvers.PRINCESS);
   }
 
+  private void requireIndependentInterpolation() {
+    assume().that(solver).isNotEqualTo(Solvers.BOOLECTOR);
+  }
+
+  private void requireIndependentTreeInterpolation() {
+    requireInterpolation();
+    requireIndependentInterpolation();
+    assume()
+        .withMessage("Tree interpolants are not supported for independent interpolation currently.")
+        .that(interpolationStrategy)
+        .isNoneOf(
+            ProverOptions.GENERATE_MODEL_BASED_INTERPOLANTS,
+            ProverOptions.GENERATE_UNIFORM_FORWARD_INTERPOLANTS,
+            ProverOptions.GENERATE_UNIFORM_BACKWARD_INTERPOLANTS);
+  }
+
+  private void requireIndependentSequentialInterpolation() {
+    requireInterpolation();
+    requireIndependentInterpolation();
+    assume()
+        .withMessage(
+            "Sequential interpolants are not supported for independent interpolation currently.")
+        .that(interpolationStrategy)
+        .isNoneOf(
+            ProverOptions.GENERATE_MODEL_BASED_INTERPOLANTS,
+            ProverOptions.GENERATE_UNIFORM_FORWARD_INTERPOLANTS,
+            ProverOptions.GENERATE_UNIFORM_BACKWARD_INTERPOLANTS);
+  }
+
+  private void requireIndependentInterpolationWithConstantFalse() {
+    if (interpolationStrategy != null) {
+      assume().that(solverToUse()).isNoneOf(Solvers.PRINCESS, Solvers.CVC5);
+    }
+  }
+
+  private void requireIndependentInterpolationSolvingIssue381() {
+    if (interpolationStrategy != null) {
+      assume().that(solverToUse()).isNotEqualTo(Solvers.Z3);
+    }
+
+    if (interpolationStrategy == ProverOptions.GENERATE_MODEL_BASED_INTERPOLANTS) {
+      assume()
+          .withMessage("Solver %s returned null or unknown on sat check", solverToUse())
+          .that(solverToUse())
+          .isNoneOf(Solvers.CVC4, Solvers.CVC5, Solvers.PRINCESS);
+    }
+  }
+
   @Test
   public <T> void sequentialInterpolation() throws SolverException, InterruptedException {
     InterpolatingProverEnvironment<T> stack = newEnvironmentForTest();
     requireIntegers();
+    requireIndependentSequentialInterpolation();
 
     assume()
         .withMessage("Solver %s runs into timeout on this test", solverToUse())
@@ -318,6 +399,7 @@ public <T> void sequentialInterpolationIsNotRepeatedIndividualInterpolation()
       throws SolverException, InterruptedException {
     InterpolatingProverEnvironment<T> stack = newEnvironmentForTest();
     requireIntegers();
+    requireIndependentSequentialInterpolation();
 
     IntegerFormula zero = imgr.makeNumber(0);
     IntegerFormula one = imgr.makeNumber(1);
@@ -367,6 +449,7 @@ public <T> void sequentialInterpolationIsNotRepeatedIndividualInterpolation()
   public <T> void sequentialInterpolationWithoutPartition()
       throws SolverException, InterruptedException {
     requireIntegers();
+    requireIndependentSequentialInterpolation();
     InterpolatingProverEnvironment<T> stack = newEnvironmentForTest();
 
     stack.push(imgr.equal(imgr.makeNumber(0), imgr.makeNumber(1)));
@@ -381,6 +464,7 @@ public <T> void sequentialInterpolationWithoutPartition()
   public <T> void sequentialInterpolationWithOnePartition()
       throws SolverException, InterruptedException {
     requireIntegers();
+    requireIndependentSequentialInterpolation();
 
     InterpolatingProverEnvironment<T> stack = newEnvironmentForTest();
     int i = index.getFreshId();
@@ -409,6 +493,7 @@ public <T> void sequentialInterpolationWithOnePartition()
   public <T> void sequentialInterpolationWithFewPartitions()
       throws SolverException, InterruptedException {
     requireIntegers();
+    requireIndependentSequentialInterpolation();
 
     InterpolatingProverEnvironment<T> stack = newEnvironmentForTest();
     int i = index.getFreshId();
@@ -441,6 +526,7 @@ public <T> void sequentialInterpolationWithFewPartitions()
   @Test
   public <T> void sequentialBVInterpolation() throws SolverException, InterruptedException {
     requireBitvectors();
+    requireIndependentSequentialInterpolation();
 
     assume()
         .withMessage("Solver %s runs into timeout on this test", solverToUse())
@@ -496,6 +582,7 @@ public <T> void sequentialBVInterpolation() throws SolverException, InterruptedE
   public void treeInterpolation() throws SolverException, InterruptedException {
 
     requireTreeItp();
+    requireIndependentTreeInterpolation();
 
     int i = index.getFreshId();
 
@@ -666,6 +753,7 @@ private <T> void testTreeInterpolants2(
   public <T> void treeInterpolation2() throws SolverException, InterruptedException {
 
     requireTreeItp();
+    requireIndependentTreeInterpolation();
 
     InterpolatingProverEnvironment<T> stack = newEnvironmentForTest();
 
@@ -725,6 +813,7 @@ public <T> void treeInterpolation2() throws SolverException, InterruptedExceptio
   public <T> void treeInterpolation3() throws SolverException, InterruptedException {
 
     requireTreeItp();
+    requireIndependentTreeInterpolation();
 
     InterpolatingProverEnvironment<T> stack = newEnvironmentForTest();
 
@@ -781,6 +870,7 @@ public <T> void treeInterpolation3() throws SolverException, InterruptedExceptio
   public <T> void treeInterpolation4() throws SolverException, InterruptedException {
 
     requireTreeItp();
+    requireIndependentTreeInterpolation();
 
     InterpolatingProverEnvironment<T> stack = newEnvironmentForTest();
 
@@ -828,6 +918,7 @@ public <T> void treeInterpolation4() throws SolverException, InterruptedExceptio
   public <T> void treeInterpolationForSequence() throws SolverException, InterruptedException {
 
     requireTreeItp();
+    requireIndependentTreeInterpolation();
 
     InterpolatingProverEnvironment<T> stack = newEnvironmentForTest();
 
@@ -853,6 +944,7 @@ public <T> void treeInterpolationForSequence() throws SolverException, Interrupt
   public <T> void treeInterpolationBranching() throws SolverException, InterruptedException {
 
     requireTreeItp();
+    requireIndependentTreeInterpolation();
 
     InterpolatingProverEnvironment<T> stack = newEnvironmentForTest();
 
@@ -894,6 +986,7 @@ public <T> void treeInterpolationBranching() throws SolverException, Interrupted
   public <T> void treeInterpolationMalFormed1() throws SolverException, InterruptedException {
 
     requireTreeItp();
+    requireIndependentTreeInterpolation();
 
     InterpolatingProverEnvironment<T> stack = newEnvironmentForTest();
     BooleanFormula A = imgr.equal(imgr.makeNumber(0), imgr.makeNumber(1));
@@ -908,6 +1001,7 @@ public <T> void treeInterpolationMalFormed1() throws SolverException, Interrupte
   public <T> void treeInterpolationMalFormed2() throws SolverException, InterruptedException {
 
     requireTreeItp();
+    requireIndependentTreeInterpolation();
 
     InterpolatingProverEnvironment<T> stack = newEnvironmentForTest();
     BooleanFormula A = imgr.equal(imgr.makeNumber(0), imgr.makeNumber(1));
@@ -922,6 +1016,7 @@ public <T> void treeInterpolationMalFormed2() throws SolverException, Interrupte
   public <T> void treeInterpolationMalFormed3() throws SolverException, InterruptedException {
 
     requireTreeItp();
+    requireIndependentTreeInterpolation();
 
     InterpolatingProverEnvironment<T> stack = newEnvironmentForTest();
     BooleanFormula A = imgr.equal(imgr.makeNumber(0), imgr.makeNumber(1));
@@ -936,6 +1031,7 @@ public <T> void treeInterpolationMalFormed3() throws SolverException, Interrupte
   public <T> void treeInterpolationMalFormed4() throws SolverException, InterruptedException {
 
     requireTreeItp();
+    requireIndependentTreeInterpolation();
 
     InterpolatingProverEnvironment<T> stack = newEnvironmentForTest();
     BooleanFormula A = imgr.equal(imgr.makeNumber(0), imgr.makeNumber(1));
@@ -950,6 +1046,7 @@ public <T> void treeInterpolationMalFormed4() throws SolverException, Interrupte
   public <T> void treeInterpolationMalFormed5() throws SolverException, InterruptedException {
 
     requireTreeItp();
+    requireIndependentTreeInterpolation();
 
     InterpolatingProverEnvironment<T> stack = newEnvironmentForTest();
     BooleanFormula A = imgr.equal(imgr.makeNumber(0), imgr.makeNumber(1));
@@ -964,6 +1061,7 @@ public <T> void treeInterpolationMalFormed5() throws SolverException, Interrupte
   public <T> void treeInterpolationMalFormed6() throws SolverException, InterruptedException {
 
     requireTreeItp();
+    requireIndependentTreeInterpolation();
 
     InterpolatingProverEnvironment<T> stack = newEnvironmentForTest();
     BooleanFormula A = imgr.equal(imgr.makeNumber(0), imgr.makeNumber(1));
@@ -977,6 +1075,7 @@ public <T> void treeInterpolationMalFormed6() throws SolverException, Interrupte
   @SuppressWarnings("CheckReturnValue")
   public <T> void treeInterpolationWithoutPartition() throws SolverException, InterruptedException {
     requireTreeItp();
+    requireIndependentTreeInterpolation();
 
     InterpolatingProverEnvironment<T> stack = newEnvironmentForTest();
 
@@ -991,6 +1090,7 @@ public <T> void treeInterpolationWithoutPartition() throws SolverException, Inte
   @Test
   public <T> void treeInterpolationWithOnePartition() throws SolverException, InterruptedException {
     requireTreeItp();
+    requireIndependentTreeInterpolation();
 
     InterpolatingProverEnvironment<T> stack = newEnvironmentForTest();
 
@@ -1021,6 +1121,7 @@ public <T> void treeInterpolationWithOnePartition() throws SolverException, Inte
   public <T> void bigSeqInterpolationTest() throws InterruptedException, SolverException {
     requireBitvectors();
     requireInterpolation();
+    requireIndependentSequentialInterpolation();
 
     assume()
         .withMessage("Solver %s runs into timeout on this test", solverToUse())
@@ -1187,6 +1288,7 @@ public <T> void testInvalidToken() throws InterruptedException, SolverException
    */
   @Test
   public <T> void issue381InterpolationTest1() throws InterruptedException, SolverException {
+    requireIndependentSequentialInterpolation();
     try (InterpolatingProverEnvironment<T> prover = newEnvironmentForTest()) {
       var x = imgr.makeVariable("x");
       var one = imgr.makeNumber(1);
@@ -1213,6 +1315,7 @@ public <T> void issue381InterpolationTest1() throws InterruptedException, Solver
    */
   @Test
   public <T> void issue381InterpolationTest2() throws InterruptedException, SolverException {
+    requireIndependentSequentialInterpolation();
     try (InterpolatingProverEnvironment<T> prover = newEnvironmentForTest()) {
       var x = imgr.makeVariable("x");
       var one = imgr.makeNumber(1);
@@ -1239,6 +1342,8 @@ public <T> void issue381InterpolationTest2() throws InterruptedException, Solver
    */
   @Test
   public <T> void issue381InterpolationTest3() throws InterruptedException, SolverException {
+    requireIntegers();
+    requireIndependentInterpolationSolvingIssue381();
     try (InterpolatingProverEnvironment<T> prover = newEnvironmentForTest()) {
       var x = imgr.makeVariable("x");
       var one = imgr.makeNumber(1);
diff --git a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java
index f38248560d..7aadff65b7 100644
--- a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java
+++ b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java
@@ -12,9 +12,14 @@
 import static org.sosy_lab.java_smt.test.BooleanFormulaSubject.assertUsing;
 import static org.sosy_lab.java_smt.test.ProverEnvironmentSubject.assertThat;
 
+import com.google.common.collect.ImmutableSet;
 import com.google.common.truth.Truth;
 import edu.umd.cs.findbugs.annotations.SuppressFBWarnings;
+import java.util.ArrayList;
+import java.util.Arrays;
 import java.util.Collection;
+import java.util.List;
+import java.util.Set;
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.junit.After;
 import org.junit.Before;
@@ -288,9 +293,14 @@ protected final void requireOptimization() {
     }
   }
 
-  protected final void requireInterpolation() {
+  // TODO: extend all tests with solver-independent interpolation options
+  protected final void requireInterpolation(ProverOptions... options) {
     try {
-      context.newProverEnvironmentWithInterpolation().close();
+      if (Arrays.stream(options).anyMatch(p -> p == null)) {
+        context.newProverEnvironmentWithInterpolation().close();
+      } else {
+        context.newProverEnvironmentWithInterpolation(options).close();
+      }
     } catch (UnsupportedOperationException e) {
       assume()
           .withMessage("Solver %s does not support interpolation", solverToUse())
@@ -438,4 +448,42 @@ protected Solvers solverToUse() {
       return solver;
     }
   }
+
+  @RunWith(Parameterized.class)
+  public abstract static class ParameterizedInterpolatingSolverBasedTest0 extends SolverBasedTest0 {
+
+    private static final Set<ProverOptions> ALL_INDEPENDENT_INTERPOLATION_STRATEGIES =
+        ImmutableSet.of(
+            ProverOptions.GENERATE_MODEL_BASED_INTERPOLANTS,
+            ProverOptions.GENERATE_UNIFORM_BACKWARD_INTERPOLANTS,
+            ProverOptions.GENERATE_UNIFORM_FORWARD_INTERPOLANTS);
+
+    @Parameters(name = "solver {0} with interpolation strategy {1}")
+    public static List<Object[]> getAllSolversAndItpStrategies() {
+      List<Object[]> lst = new ArrayList<>();
+      for (Solvers solver : Solvers.values()) {
+        // No arg for no option (= solver based interpolation)
+        lst.add(new Object[] {solver, null});
+        for (ProverOptions itpStrat : ALL_INDEPENDENT_INTERPOLATION_STRATEGIES) {
+          lst.add(new Object[] {solver, itpStrat});
+        }
+      }
+      return lst;
+    }
+
+    @Parameter(0)
+    public Solvers solver;
+
+    @Parameter(1)
+    public ProverOptions interpolationStrategy;
+
+    @Override
+    protected Solvers solverToUse() {
+      return solver;
+    }
+
+    protected ProverOptions itpStrategyToUse() {
+      return interpolationStrategy;
+    }
+  }
 }