diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java
index 2b588345af..debe0d080f 100644
--- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java
+++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java
@@ -31,6 +31,7 @@
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.Evaluator;
 import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment;
+import org.sosy_lab.java_smt.api.Model;
 import org.sosy_lab.java_smt.api.OptimizationProverEnvironment;
 import org.sosy_lab.java_smt.api.OptimizationProverEnvironment.OptStatus;
 import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
@@ -99,6 +100,14 @@ protected final void checkGenerateUnsatCoresOverAssumptions() {
         ProverOptions.GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS);
   }
 
+  /**
+   * Checks whether the prover has been closed already. Only to be used if this is the only check
+   * performed in a call.
+   */
+  protected void checkClosed() {
+    Preconditions.checkState(!closed);
+  }
+
   private void checkGenerateInterpolants() {
     Preconditions.checkState(!closed);
     Preconditions.checkState(
@@ -279,6 +288,24 @@ protected ImmutableMap<T, BooleanFormula> getAssertedFormulasById() {
     return builder.buildOrThrow();
   }
 
+  @Override
+  public final Model getModel() throws SolverException {
+    checkGenerateModels();
+    return getModelImpl();
+  }
+
+  protected abstract Model getModelImpl() throws SolverException;
+
+  @Override
+  public final Evaluator getEvaluator() throws SolverException {
+    checkGenerateModels();
+    return getEvaluatorImpl();
+  }
+
+  protected Evaluator getEvaluatorImpl() throws SolverException {
+    return getModel();
+  }
+
   /**
    * This method registers the Evaluator to be cleaned up before the next change on the prover
    * stack.
diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractSolverContext.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractSolverContext.java
index f92574f031..78f68ede48 100644
--- a/src/org/sosy_lab/java_smt/basicimpl/AbstractSolverContext.java
+++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractSolverContext.java
@@ -72,7 +72,7 @@ protected abstract InterpolatingProverEnvironment<?> newProverEnvironmentWithInt
   @Override
   public final OptimizationProverEnvironment newOptimizationProverEnvironment(
       ProverOptions... options) {
-    return newOptimizationProverEnvironment0(toSet(options));
+    return new OptimizationProverDelegate(newOptimizationProverEnvironment0(toSet(options)));
   }
 
   protected abstract OptimizationProverEnvironment newOptimizationProverEnvironment0(
diff --git a/src/org/sosy_lab/java_smt/basicimpl/InterpolatingProverDelegate.java b/src/org/sosy_lab/java_smt/basicimpl/InterpolatingProverDelegate.java
index f5b907e42a..9e186c704d 100644
--- a/src/org/sosy_lab/java_smt/basicimpl/InterpolatingProverDelegate.java
+++ b/src/org/sosy_lab/java_smt/basicimpl/InterpolatingProverDelegate.java
@@ -10,6 +10,7 @@
 
 package org.sosy_lab.java_smt.basicimpl;
 
+import static com.google.common.base.Preconditions.checkArgument;
 import static com.google.common.base.Preconditions.checkNotNull;
 
 import java.util.Collection;
@@ -31,6 +32,7 @@ class InterpolatingProverDelegate<T> implements InterpolatingProverEnvironment<T
   private final InterpolatingProverEnvironment<T> itpProver;
 
   InterpolatingProverDelegate(InterpolatingProverEnvironment<T> pBaseProver) {
+    checkArgument(pBaseProver instanceof AbstractProver<?>);
     itpProver = checkNotNull(pBaseProver);
   }
 
diff --git a/src/org/sosy_lab/java_smt/basicimpl/OptimizationProverDelegate.java b/src/org/sosy_lab/java_smt/basicimpl/OptimizationProverDelegate.java
new file mode 100644
index 0000000000..e73573ae4d
--- /dev/null
+++ b/src/org/sosy_lab/java_smt/basicimpl/OptimizationProverDelegate.java
@@ -0,0 +1,141 @@
+/*
+ * This file is part of JavaSMT,
+ * an API wrapper for a collection of SMT solvers:
+ * https://github.com/sosy-lab/java-smt
+ *
+ * SPDX-FileCopyrightText: 2026 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 java.util.Collection;
+import java.util.List;
+import java.util.Optional;
+import org.checkerframework.checker.nullness.qual.Nullable;
+import org.sosy_lab.common.rationals.Rational;
+import org.sosy_lab.java_smt.api.BooleanFormula;
+import org.sosy_lab.java_smt.api.Formula;
+import org.sosy_lab.java_smt.api.Model;
+import org.sosy_lab.java_smt.api.OptimizationProverEnvironment;
+import org.sosy_lab.java_smt.api.SolverException;
+
+/**
+ * This delegate enables common implementations for methods in {@link OptimizationProverEnvironment}
+ * based on the implementations in the abstract/theorem prover that can not be done using abstract
+ * implementations.
+ */
+public class OptimizationProverDelegate implements OptimizationProverEnvironment {
+
+  private final OptimizationProverEnvironment optimizationProver;
+
+  OptimizationProverDelegate(OptimizationProverEnvironment pBaseProver) {
+    checkArgument(pBaseProver instanceof AbstractProver<?>);
+    optimizationProver = checkNotNull(pBaseProver);
+  }
+
+  @SuppressWarnings("resource")
+  @Override
+  public int maximize(Formula objective) {
+    getDelegateAsAbstractProver().checkClosed();
+    return optimizationProver.maximize(objective);
+  }
+
+  @SuppressWarnings("resource")
+  @Override
+  public int minimize(Formula objective) {
+    getDelegateAsAbstractProver().checkClosed();
+    return optimizationProver.minimize(objective);
+  }
+
+  @SuppressWarnings("resource")
+  @Override
+  public Optional<Rational> upper(int handle, Rational epsilon) {
+    getDelegateAsAbstractProver().checkGenerateModels();
+    return optimizationProver.upper(handle, epsilon);
+  }
+
+  @SuppressWarnings("resource")
+  @Override
+  public Optional<Rational> lower(int handle, Rational epsilon) {
+    getDelegateAsAbstractProver().checkGenerateModels();
+    return optimizationProver.lower(handle, epsilon);
+  }
+
+  @Override
+  public OptStatus check() throws InterruptedException, SolverException {
+    // We don't need to do anything for check, as it is already handled in AbstractProver
+    return optimizationProver.check();
+  }
+
+  /* ########################## Delegate methods of ProverEnvironment ########################## */
+
+  @SuppressWarnings("resource")
+  @Override
+  public Model getModel() throws SolverException {
+    return optimizationProver.getModel();
+  }
+
+  @Override
+  public void pop() {
+    optimizationProver.pop();
+  }
+
+  @Override
+  public @Nullable Void addConstraint(BooleanFormula constraint) throws InterruptedException {
+    return optimizationProver.addConstraint(constraint);
+  }
+
+  @Override
+  public void push() throws InterruptedException {
+    optimizationProver.push();
+  }
+
+  @Override
+  public int size() {
+    return optimizationProver.size();
+  }
+
+  @Override
+  public boolean isUnsat() throws SolverException, InterruptedException {
+    return optimizationProver.isUnsat();
+  }
+
+  @Override
+  public boolean isUnsatWithAssumptions(Collection<BooleanFormula> assumptions)
+      throws SolverException, InterruptedException {
+    return optimizationProver.isUnsatWithAssumptions(assumptions);
+  }
+
+  @Override
+  public List<BooleanFormula> getUnsatCore() {
+    return optimizationProver.getUnsatCore();
+  }
+
+  @Override
+  public Optional<List<BooleanFormula>> unsatCoreOverAssumptions(
+      Collection<BooleanFormula> assumptions) throws SolverException, InterruptedException {
+    return optimizationProver.unsatCoreOverAssumptions(assumptions);
+  }
+
+  @Override
+  public void close() {
+    optimizationProver.close();
+  }
+
+  @Override
+  public <R> R allSat(AllSatCallback<R> callback, List<BooleanFormula> important)
+      throws InterruptedException, SolverException {
+    return optimizationProver.allSat(callback, important);
+  }
+
+  /* ############################### Utility methods ############################### */
+  @SuppressWarnings("unchecked")
+  private AbstractProver<?> getDelegateAsAbstractProver() {
+    return (AbstractProver<?>) optimizationProver;
+  }
+}
diff --git a/src/org/sosy_lab/java_smt/basicimpl/PackageSanityTest.java b/src/org/sosy_lab/java_smt/basicimpl/PackageSanityTest.java
index 375f70d390..6ea4c1aee1 100644
--- a/src/org/sosy_lab/java_smt/basicimpl/PackageSanityTest.java
+++ b/src/org/sosy_lab/java_smt/basicimpl/PackageSanityTest.java
@@ -18,6 +18,9 @@ public class PackageSanityTest extends AbstractPackageSanityTests {
   {
     setDistinctValues(FormulaType.class, FormulaType.BooleanType, FormulaType.IntegerType);
     setDefault(ShutdownNotifier.class, ShutdownManager.create().getNotifier());
-    ignoreClasses(c -> c.equals(InterpolatingProverDelegate.class));
+    ignoreClasses(
+        c ->
+            c.equals(InterpolatingProverDelegate.class)
+                || c.equals(OptimizationProverDelegate.class));
   }
 }
diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaAbstractProver.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaAbstractProver.java
index 452c997a08..23b440fa90 100644
--- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaAbstractProver.java
+++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaAbstractProver.java
@@ -161,8 +161,7 @@ public boolean isUnsatWithAssumptions(Collection<BooleanFormula> assumptions) {
    */
   @SuppressWarnings("resource")
   @Override
-  public Model getModel() throws SolverException {
-    checkGenerateModels();
+  protected Model getModelImpl() throws SolverException {
     // special case for Bitwuzla: Models are not permanent and need to be closed
     // before any change is applied to the prover stack. So, we register the Model as Evaluator.
     return registerEvaluator(
diff --git a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorTheoremProver.java b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorTheoremProver.java
index 4e996798fe..47a565f245 100644
--- a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorTheoremProver.java
+++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorTheoremProver.java
@@ -127,8 +127,7 @@ public boolean isUnsatWithAssumptions(Collection<BooleanFormula> pAssumptions)
   }
 
   @Override
-  public Model getModel() throws SolverException {
-    checkGenerateModels();
+  protected Model getModelImpl() throws SolverException {
     return getEvaluatorWithoutChecks();
   }
 
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 fb041ca180..46e94c3db0 100644
--- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java
+++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java
@@ -143,8 +143,7 @@ private void assertFormula(BooleanFormula pF) {
 
   @SuppressWarnings("resource")
   @Override
-  public CVC4Model getModel() throws SolverException {
-    checkGenerateModels();
+  public CVC4Model getModelImpl() throws SolverException {
     // special case for CVC4: Models are not permanent and need to be closed
     // before any change is applied to the prover stack. So, we register the Model as Evaluator.
     return registerEvaluator(
@@ -156,8 +155,7 @@ public CVC4Model getModel() throws SolverException {
   }
 
   @Override
-  public Evaluator getEvaluator() {
-    checkGenerateModels();
+  protected Evaluator getEvaluatorImpl() {
     return getEvaluatorWithoutChecks();
   }
 
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 92565fb2cb..ef1effd062 100644
--- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java
+++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java
@@ -165,8 +165,7 @@ protected String addConstraint0(BooleanFormula pF) {
 
   @SuppressWarnings("resource")
   @Override
-  public CVC5Model getModel() throws SolverException {
-    checkGenerateModels();
+  public CVC5Model getModelImpl() throws SolverException {
     // special case for CVC5: Models are not permanent and need to be closed
     // before any change is applied to the prover stack. So, we register the Model as Evaluator.
     return registerEvaluator(
@@ -175,8 +174,7 @@ public CVC5Model getModel() throws SolverException {
   }
 
   @Override
-  public Evaluator getEvaluator() {
-    checkGenerateModels();
+  protected Evaluator getEvaluatorImpl() {
     return getEvaluatorWithoutChecks();
   }
 
diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java
index 62f45ae62d..9e9d97920e 100644
--- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java
+++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java
@@ -144,8 +144,7 @@ protected boolean hasPersistentModel() {
 
   @SuppressWarnings("resource")
   @Override
-  public Model getModel() throws SolverException {
-    checkGenerateModels();
+  protected Model getModelImpl() throws SolverException {
     return new CachingModel(new Mathsat5Model(getMsatModel(), creator, this));
   }
 
@@ -153,14 +152,12 @@ public Model getModel() throws SolverException {
    * @throws SolverException if an expected MathSAT failure occurs
    */
   protected long getMsatModel() throws SolverException {
-    checkGenerateModels();
     return Mathsat5NativeApi.msat_get_model(curEnv);
   }
 
   @SuppressWarnings("resource")
   @Override
-  public Evaluator getEvaluator() {
-    checkGenerateModels();
+  protected Evaluator getEvaluatorImpl() {
     return registerEvaluator(new Mathsat5Evaluator(this, creator, curEnv));
   }
 
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 acef855818..348521a75c 100644
--- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5OptimizationProver.java
+++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5OptimizationProver.java
@@ -8,7 +8,6 @@
 
 package org.sosy_lab.java_smt.solvers.mathsat5;
 
-import static com.google.common.base.Preconditions.checkState;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5FormulaManager.getMsatTerm;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_OPTIMUM;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_assert_formula;
@@ -77,7 +76,6 @@ protected Void addConstraintImpl(BooleanFormula constraint) throws InterruptedEx
 
   @Override
   public int maximize(Formula objective) {
-    checkState(!closed);
     long objectiveId = msat_make_maximize(curEnv, getMsatTerm(objective));
     msat_assert_objective(curEnv, objectiveId);
     int id = idGenerator.getFreshId(); // mapping needed to avoid long-int-conversion
@@ -87,7 +85,6 @@ public int maximize(Formula objective) {
 
   @Override
   public int minimize(Formula objective) {
-    checkState(!closed);
     long objectiveId = msat_make_minimize(curEnv, getMsatTerm(objective));
     msat_assert_objective(curEnv, objectiveId);
     int id = idGenerator.getFreshId(); // mapping needed to avoid long-int-conversion
@@ -119,15 +116,11 @@ protected void popImpl() {
 
   @Override
   public Optional<Rational> upper(int handle, Rational epsilon) {
-    checkState(!closed);
-    checkGenerateModels();
     return getValue(handle, epsilon);
   }
 
   @Override
   public Optional<Rational> lower(int handle, Rational epsilon) {
-    checkState(!closed);
-    checkGenerateModels();
     return getValue(handle, epsilon);
   }
 
@@ -146,12 +139,10 @@ private Optional<Rational> getValue(int handle, Rational epsilon) {
   }
 
   @Override
-  public Model getModel() throws SolverException {
-    checkState(!closed);
-    checkGenerateModels(); // Needed before loading objective model!
+  protected Model getModelImpl() throws SolverException {
     if (!objectiveMap.isEmpty()) {
       msat_load_objective_model(curEnv, objectiveMap.values().iterator().next());
     }
-    return super.getModel();
+    return super.getModelImpl();
   }
 }
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 c193becf2f..16b33bb5ec 100644
--- a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java
+++ b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java
@@ -117,16 +117,14 @@ protected T addConstraintImpl(BooleanFormula pF) throws InterruptedException {
 
   @SuppressWarnings("resource")
   @Override
-  public Model getModel() {
-    checkGenerateModels();
+  protected Model getModelImpl() {
     return registerEvaluator(
         new OpenSmtModel(
             this, creator, Collections2.transform(getAssertedFormulas(), creator::extractInfo)));
   }
 
   @Override
-  public Evaluator getEvaluator() {
-    checkGenerateModels();
+  protected Evaluator getEvaluatorImpl() {
     return getEvaluatorWithoutChecks();
   }
 
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 8a1230a9e4..582ca0e388 100644
--- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java
+++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java
@@ -130,8 +130,7 @@ protected void popImpl() {
 
   @SuppressWarnings("resource")
   @Override
-  public Model getModel() throws SolverException {
-    checkGenerateModels();
+  protected Model getModelImpl() throws SolverException {
     return new CachingModel(getEvaluatorWithoutChecks());
   }
 
diff --git a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java
index 44ea0f5e1d..0c9d649a5c 100644
--- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java
+++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java
@@ -140,8 +140,7 @@ protected boolean isUnsatImpl() throws InterruptedException {
 
   @SuppressWarnings("resource")
   @Override
-  public org.sosy_lab.java_smt.api.Model getModel() {
-    checkGenerateModels();
+  public org.sosy_lab.java_smt.api.Model getModelImpl() {
     final Model model;
     try {
       model = env.getModel();
diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2AbstractProver.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2AbstractProver.java
index e1cf284faa..d0c8f45747 100644
--- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2AbstractProver.java
+++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2AbstractProver.java
@@ -207,8 +207,7 @@ public boolean isUnsatWithAssumptions(Collection<BooleanFormula> pAssumptions)
 
   @SuppressWarnings("resource")
   @Override
-  public Model getModel() throws SolverException {
-    checkGenerateModels();
+  protected Model getModelImpl() throws SolverException {
     return new CachingModel(getEvaluatorWithoutChecks());
   }
 
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 e6e036fde5..9e7e27d096 100644
--- a/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java
+++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java
@@ -116,8 +116,7 @@ protected boolean hasPersistentModel() {
 
   @SuppressWarnings("resource")
   @Override
-  public Model getModel() throws SolverException {
-    checkGenerateModels();
+  protected Model getModelImpl() throws SolverException {
     return new CachingModel(getEvaluatorWithoutChecks());
   }
 
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 d583f04267..77171349c0 100644
--- a/src/org/sosy_lab/java_smt/solvers/z3/Z3OptimizationProver.java
+++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3OptimizationProver.java
@@ -8,8 +8,6 @@
 
 package org.sosy_lab.java_smt.solvers.z3;
 
-import static com.google.common.base.Preconditions.checkState;
-
 import com.google.common.base.Preconditions;
 import com.google.common.collect.ImmutableMap;
 import com.microsoft.z3.Native;
@@ -66,13 +64,11 @@ class Z3OptimizationProver extends Z3AbstractProver implements OptimizationProve
 
   @Override
   public int maximize(Formula objective) {
-    Preconditions.checkState(!closed);
     return Native.optimizeMaximize(z3context, z3optSolver, creator.extractInfo(objective));
   }
 
   @Override
   public int minimize(Formula objective) {
-    checkState(!closed);
     return Native.optimizeMinimize(z3context, z3optSolver, creator.extractInfo(objective));
   }
 
@@ -149,15 +145,11 @@ public boolean isUnsatWithAssumptions(Collection<BooleanFormula> assumptions)
 
   @Override
   public Optional<Rational> upper(int handle, Rational epsilon) {
-    checkState(!closed);
-    checkGenerateModels();
     return round(handle, epsilon, Native::optimizeGetUpperAsVector);
   }
 
   @Override
   public Optional<Rational> lower(int handle, Rational epsilon) {
-    checkState(!closed);
-    checkGenerateModels();
     return round(handle, epsilon, Native::optimizeGetLowerAsVector);
   }
 
diff --git a/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyAbstractProver.java b/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyAbstractProver.java
index d883ed9a0d..57be12c432 100644
--- a/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyAbstractProver.java
+++ b/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyAbstractProver.java
@@ -121,8 +121,7 @@ protected boolean hasPersistentModel() {
 
   @SuppressWarnings("resource")
   @Override
-  public Model getModel() throws SolverException {
-    checkGenerateModels();
+  protected Model getModelImpl() throws SolverException {
     return new CachingModel(getEvaluatorWithoutChecks());
   }