diff --git a/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java b/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java
index dd086f6728..d832794937 100644
--- a/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java
+++ b/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java
@@ -32,7 +32,7 @@ public interface BasicProverEnvironment<T> extends AutoCloseable {
    */
   @Nullable
   @CanIgnoreReturnValue
-  default T push(BooleanFormula f) throws InterruptedException {
+  default T push(BooleanFormula f) throws InterruptedException, SolverException {
     push();
     return addConstraint(f);
   }
@@ -46,7 +46,7 @@ default T push(BooleanFormula f) throws InterruptedException {
   /** Add a constraint to the latest backtracking point. */
   @Nullable
   @CanIgnoreReturnValue
-  T addConstraint(BooleanFormula constraint) throws InterruptedException;
+  T addConstraint(BooleanFormula constraint) throws InterruptedException, SolverException;
 
   /**
    * Create a new backtracking point, i.e., a new level on the assertion stack. Each level can hold
@@ -55,7 +55,7 @@ default T push(BooleanFormula f) throws InterruptedException {
    * <p>If formulas are added before creating the first backtracking point, they can not be removed
    * via a POP-operation.
    */
-  void push() throws InterruptedException;
+  void push() throws InterruptedException, SolverException;
 
   /**
    * Get the number of backtracking points/levels on the current stack.
@@ -87,7 +87,7 @@ boolean isUnsatWithAssumptions(Collection<BooleanFormula> assumptions)
    * <p>A model might contain additional symbols with their evaluation, if a solver uses its own
    * temporary symbols. There should be at least a value-assignment for each free symbol.
    */
-  Model getModel() throws SolverException;
+  Model getModel() throws SolverException, InterruptedException;
 
   /**
    * Get a temporary view on the current satisfying assignment. This should be called only
@@ -95,7 +95,7 @@ boolean isUnsatWithAssumptions(Collection<BooleanFormula> assumptions)
    * should no longer be used as soon as any constraints are added to, pushed, or popped from the
    * prover stack.
    */
-  default Evaluator getEvaluator() throws SolverException {
+  default Evaluator getEvaluator() throws SolverException, InterruptedException {
     return getModel();
   }
 
@@ -107,7 +107,8 @@ default Evaluator getEvaluator() throws SolverException {
    * <p>Note that if you need to iterate multiple times over the model it may be more efficient to
    * use this method instead of {@link #getModel()} (depending on the solver).
    */
-  default ImmutableList<Model.ValueAssignment> getModelAssignments() throws SolverException {
+  default ImmutableList<Model.ValueAssignment> getModelAssignments()
+      throws SolverException, InterruptedException {
     try (Model model = getModel()) {
       return model.asList();
     }
diff --git a/src/org/sosy_lab/java_smt/api/Evaluator.java b/src/org/sosy_lab/java_smt/api/Evaluator.java
index 03ca8b00a0..7fa0199467 100644
--- a/src/org/sosy_lab/java_smt/api/Evaluator.java
+++ b/src/org/sosy_lab/java_smt/api/Evaluator.java
@@ -47,7 +47,7 @@ public interface Evaluator extends AutoCloseable {
    * @return evaluation of the given formula or <code>null</code> if the solver does not provide a
    *     better evaluation.
    */
-  @Nullable <T extends Formula> T eval(T formula);
+  @Nullable <T extends Formula> T eval(T formula) throws SolverException, InterruptedException;
 
   /**
    * Evaluate a given formula substituting the values from the model.
@@ -62,56 +62,60 @@ public interface Evaluator extends AutoCloseable {
    * @return Either of: - Number (Rational/Double/BigInteger/Long/Integer) - Boolean
    * @throws IllegalArgumentException if a formula has unexpected type, e.g. Array.
    */
-  @Nullable Object evaluate(Formula formula);
+  @Nullable Object evaluate(Formula formula) throws SolverException, InterruptedException;
 
   /**
    * Type-safe evaluation for integer formulas.
    *
    * <p>The formula does not need to be a variable, we also allow complex expression.
    */
-  @Nullable BigInteger evaluate(IntegerFormula formula);
+  @Nullable BigInteger evaluate(IntegerFormula formula)
+      throws SolverException, InterruptedException;
 
   /**
    * Type-safe evaluation for rational formulas.
    *
    * <p>The formula does not need to be a variable, we also allow complex expression.
    */
-  @Nullable Rational evaluate(RationalFormula formula);
+  @Nullable Rational evaluate(RationalFormula formula) throws SolverException, InterruptedException;
 
   /**
    * Type-safe evaluation for boolean formulas.
    *
    * <p>The formula does not need to be a variable, we also allow complex expression.
    */
-  @Nullable Boolean evaluate(BooleanFormula formula);
+  @Nullable Boolean evaluate(BooleanFormula formula) throws SolverException, InterruptedException;
 
   /**
    * Type-safe evaluation for bitvector formulas.
    *
    * <p>The formula does not need to be a variable, we also allow complex expression.
    */
-  @Nullable BigInteger evaluate(BitvectorFormula formula);
+  @Nullable BigInteger evaluate(BitvectorFormula formula)
+      throws SolverException, InterruptedException;
 
   /**
    * Type-safe evaluation for string formulas.
    *
    * <p>The formula does not need to be a variable, we also allow complex expression.
    */
-  @Nullable String evaluate(StringFormula formula);
+  @Nullable String evaluate(StringFormula formula) throws SolverException, InterruptedException;
 
   /**
    * Type-safe evaluation for enumeration formulas.
    *
    * <p>The formula does not need to be a variable, we also allow complex expression.
    */
-  @Nullable String evaluate(EnumerationFormula formula);
+  @Nullable String evaluate(EnumerationFormula formula)
+      throws SolverException, InterruptedException;
 
   /**
    * Type-safe evaluation for floating-point formulas.
    *
    * <p>The formula does not need to be a variable, we also allow complex expression.
    */
-  @Nullable FloatingPointNumber evaluate(FloatingPointFormula formula);
+  @Nullable FloatingPointNumber evaluate(FloatingPointFormula formula)
+      throws SolverException, InterruptedException;
 
   /**
    * Free resources associated with this evaluator (existing {@link Formula} instances stay valid,
diff --git a/src/org/sosy_lab/java_smt/api/Model.java b/src/org/sosy_lab/java_smt/api/Model.java
index 27a5e7a9b1..816fbdad7a 100644
--- a/src/org/sosy_lab/java_smt/api/Model.java
+++ b/src/org/sosy_lab/java_smt/api/Model.java
@@ -49,14 +49,27 @@ public interface Model extends Evaluator, Iterable<ValueAssignment>, AutoCloseab
    *       within a quantified context, some value assignments can be missing in the iteration.
    *       Please use a direct evaluation query to get the evaluation in such a case.
    * </ul>
+   *
+   * <p>Warning: This method may throw the checked exceptions SolverException (in case of solver
+   * failures) and InterruptedException (in case of shutdown requests) although these exceptions are
+   * not declared with throws.
    */
   @Override
   default Iterator<ValueAssignment> iterator() {
-    return asList().iterator();
+    try {
+      return asList().iterator();
+    } catch (SolverException | InterruptedException ex) {
+      throw sneakyThrow(ex);
+    }
+  }
+
+  @SuppressWarnings("unchecked")
+  private static <E extends Throwable> RuntimeException sneakyThrow(Throwable e) throws E {
+    throw (E) e;
   }
 
   /** Build a list of assignments that stays valid after closing the model. */
-  ImmutableList<ValueAssignment> asList();
+  ImmutableList<ValueAssignment> asList() throws SolverException, InterruptedException;
 
   /**
    * Pretty-printing of the model values.
diff --git a/src/org/sosy_lab/java_smt/api/OptimizationProverEnvironment.java b/src/org/sosy_lab/java_smt/api/OptimizationProverEnvironment.java
index 3d6b895a1b..0980864317 100644
--- a/src/org/sosy_lab/java_smt/api/OptimizationProverEnvironment.java
+++ b/src/org/sosy_lab/java_smt/api/OptimizationProverEnvironment.java
@@ -68,7 +68,7 @@ public interface OptimizationProverEnvironment extends BasicProverEnvironment<Vo
    * (epsilon is irrelevant here and can be zero). The model returns the optimal assignment x=9.
    */
   @Override
-  Model getModel() throws SolverException;
+  Model getModel() throws SolverException, InterruptedException;
 
   /** Status of the optimization problem. */
   enum OptStatus {
diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractEvaluator.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractEvaluator.java
index fd8afe0d60..fde81062e1 100644
--- a/src/org/sosy_lab/java_smt/basicimpl/AbstractEvaluator.java
+++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractEvaluator.java
@@ -22,6 +22,7 @@
 import org.sosy_lab.java_smt.api.Formula;
 import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
 import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula;
+import org.sosy_lab.java_smt.api.SolverException;
 import org.sosy_lab.java_smt.api.StringFormula;
 
 @SuppressWarnings("ClassTypeParameterName")
@@ -40,7 +41,7 @@ protected AbstractEvaluator(
   @SuppressWarnings("unchecked")
   @Nullable
   @Override
-  public final <T extends Formula> T eval(T f) {
+  public final <T extends Formula> T eval(T f) throws SolverException, InterruptedException {
     Preconditions.checkState(!isClosed());
     TFormulaInfo evaluation = evalImpl(creator.extractInfo(f));
     return evaluation == null ? null : (T) creator.encapsulateWithTypeOf(evaluation);
@@ -48,14 +49,14 @@ public final <T extends Formula> T eval(T f) {
 
   @Nullable
   @Override
-  public final BigInteger evaluate(IntegerFormula f) {
+  public final BigInteger evaluate(IntegerFormula f) throws SolverException, InterruptedException {
     Preconditions.checkState(!isClosed());
     return (BigInteger) evaluateImpl(creator.extractInfo(f));
   }
 
   @Nullable
   @Override
-  public Rational evaluate(RationalFormula f) {
+  public Rational evaluate(RationalFormula f) throws SolverException, InterruptedException {
     Object value = evaluateImpl(creator.extractInfo(f));
     if (value instanceof BigInteger) {
       // We simplified the value internally. Here, we need to convert it back to Rational.
@@ -67,41 +68,43 @@ public Rational evaluate(RationalFormula f) {
 
   @Nullable
   @Override
-  public final Boolean evaluate(BooleanFormula f) {
+  public final Boolean evaluate(BooleanFormula f) throws SolverException, InterruptedException {
     Preconditions.checkState(!isClosed());
     return (Boolean) evaluateImpl(creator.extractInfo(f));
   }
 
   @Nullable
   @Override
-  public final String evaluate(StringFormula f) {
+  public final String evaluate(StringFormula f) throws SolverException, InterruptedException {
     Preconditions.checkState(!isClosed());
     return (String) evaluateImpl(creator.extractInfo(f));
   }
 
   @Nullable
   @Override
-  public final String evaluate(EnumerationFormula f) {
+  public final String evaluate(EnumerationFormula f) throws SolverException, InterruptedException {
     Preconditions.checkState(!isClosed());
     return (String) evaluateImpl(creator.extractInfo(f));
   }
 
   @Override
-  public final @Nullable FloatingPointNumber evaluate(FloatingPointFormula f) {
+  public final @Nullable FloatingPointNumber evaluate(FloatingPointFormula f)
+      throws SolverException, InterruptedException {
     Preconditions.checkState(!isClosed());
     return (FloatingPointNumber) evaluateImpl(creator.extractInfo(f));
   }
 
   @Nullable
   @Override
-  public final BigInteger evaluate(BitvectorFormula f) {
+  public final BigInteger evaluate(BitvectorFormula f)
+      throws SolverException, InterruptedException {
     Preconditions.checkState(!isClosed());
     return (BigInteger) evaluateImpl(creator.extractInfo(f));
   }
 
   @Nullable
   @Override
-  public final Object evaluate(Formula f) {
+  public final Object evaluate(Formula f) throws SolverException, InterruptedException {
     Preconditions.checkState(!isClosed());
     Preconditions.checkArgument(
         !(f instanceof ArrayFormula),
@@ -114,7 +117,8 @@ public final Object evaluate(Formula f) {
    * set in the model and evaluation aborts, return <code>null</code>.
    */
   @Nullable
-  protected abstract TFormulaInfo evalImpl(TFormulaInfo formula);
+  protected abstract TFormulaInfo evalImpl(TFormulaInfo formula)
+      throws SolverException, InterruptedException;
 
   /**
    * Simplify the given formula and replace all symbols with their model values. If a symbol is not
@@ -122,7 +126,7 @@ public final Object evaluate(Formula f) {
    * into a Java object as far as possible, i.e., try to match a primitive or simple type.
    */
   @Nullable
-  protected final Object evaluateImpl(TFormulaInfo f) {
+  protected Object evaluateImpl(TFormulaInfo f) throws SolverException, InterruptedException {
     Preconditions.checkState(!isClosed());
     TFormulaInfo evaluatedF = evalImpl(f);
     return evaluatedF == null ? null : creator.convertValue(f, evaluatedF);
diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java
index 07dbbbb5d6..e6d81c1f53 100644
--- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java
+++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java
@@ -26,6 +26,7 @@
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.Evaluator;
 import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
+import org.sosy_lab.java_smt.api.SolverException;
 
 public abstract class AbstractProver<T> implements BasicProverEnvironment<T> {
 
@@ -88,13 +89,13 @@ public int size() {
   }
 
   @Override
-  public final void push() throws InterruptedException {
+  public final void push() throws InterruptedException, SolverException {
     checkState(!closed);
     pushImpl();
     assertedFormulas.add(LinkedHashMultimap.create());
   }
 
-  protected abstract void pushImpl() throws InterruptedException;
+  protected abstract void pushImpl() throws InterruptedException, SolverException;
 
   @Override
   public final void pop() {
@@ -108,7 +109,8 @@ public final void pop() {
 
   @Override
   @CanIgnoreReturnValue
-  public final @Nullable T addConstraint(BooleanFormula constraint) throws InterruptedException {
+  public final @Nullable T addConstraint(BooleanFormula constraint)
+      throws InterruptedException, SolverException {
     checkState(!closed);
     T t = addConstraintImpl(constraint);
     Iterables.getLast(assertedFormulas).put(constraint, t);
@@ -116,7 +118,7 @@ public final void pop() {
   }
 
   protected abstract @Nullable T addConstraintImpl(BooleanFormula constraint)
-      throws InterruptedException;
+      throws InterruptedException, SolverException;
 
   protected ImmutableSet<BooleanFormula> getAssertedFormulas() {
     ImmutableSet.Builder<BooleanFormula> builder = ImmutableSet.builder();
diff --git a/src/org/sosy_lab/java_smt/basicimpl/CachingModel.java b/src/org/sosy_lab/java_smt/basicimpl/CachingModel.java
index ee379c61e1..0ae815d644 100644
--- a/src/org/sosy_lab/java_smt/basicimpl/CachingModel.java
+++ b/src/org/sosy_lab/java_smt/basicimpl/CachingModel.java
@@ -22,6 +22,7 @@
 import org.sosy_lab.java_smt.api.Model;
 import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
 import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula;
+import org.sosy_lab.java_smt.api.SolverException;
 import org.sosy_lab.java_smt.api.StringFormula;
 
 public class CachingModel implements Model {
@@ -35,7 +36,7 @@ public CachingModel(Model pDelegate) {
   }
 
   @Override
-  public ImmutableList<ValueAssignment> asList() {
+  public ImmutableList<ValueAssignment> asList() throws SolverException, InterruptedException {
     if (modelAssignments == null) {
       modelAssignments = delegate.asList();
     }
@@ -48,47 +49,55 @@ public void close() {
   }
 
   @Override
-  public <T extends Formula> @Nullable T eval(T formula) {
+  public <T extends Formula> @Nullable T eval(T formula)
+      throws SolverException, InterruptedException {
     return delegate.eval(formula);
   }
 
   @Override
-  public @Nullable Object evaluate(Formula formula) {
+  public @Nullable Object evaluate(Formula formula) throws SolverException, InterruptedException {
     return delegate.evaluate(formula);
   }
 
   @Override
-  public @Nullable BigInteger evaluate(IntegerFormula formula) {
+  public @Nullable BigInteger evaluate(IntegerFormula formula)
+      throws SolverException, InterruptedException {
     return delegate.evaluate(formula);
   }
 
   @Override
-  public @Nullable Rational evaluate(RationalFormula formula) {
+  public @Nullable Rational evaluate(RationalFormula formula)
+      throws SolverException, InterruptedException {
     return delegate.evaluate(formula);
   }
 
   @Override
-  public @Nullable Boolean evaluate(BooleanFormula formula) {
+  public @Nullable Boolean evaluate(BooleanFormula formula)
+      throws SolverException, InterruptedException {
     return delegate.evaluate(formula);
   }
 
   @Override
-  public @Nullable BigInteger evaluate(BitvectorFormula formula) {
+  public @Nullable BigInteger evaluate(BitvectorFormula formula)
+      throws SolverException, InterruptedException {
     return delegate.evaluate(formula);
   }
 
   @Override
-  public @Nullable String evaluate(StringFormula formula) {
+  public @Nullable String evaluate(StringFormula formula)
+      throws SolverException, InterruptedException {
     return delegate.evaluate(formula);
   }
 
   @Override
-  public @Nullable String evaluate(EnumerationFormula formula) {
+  public @Nullable String evaluate(EnumerationFormula formula)
+      throws SolverException, InterruptedException {
     return delegate.evaluate(formula);
   }
 
   @Override
-  public @Nullable FloatingPointNumber evaluate(FloatingPointFormula formula) {
+  public @Nullable FloatingPointNumber evaluate(FloatingPointFormula formula)
+      throws SolverException, InterruptedException {
     return delegate.evaluate(formula);
   }
 
diff --git a/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/BasicProverWithAssumptionsWrapper.java b/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/BasicProverWithAssumptionsWrapper.java
index 596f30f4eb..b1ee0e3b15 100644
--- a/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/BasicProverWithAssumptionsWrapper.java
+++ b/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/BasicProverWithAssumptionsWrapper.java
@@ -43,13 +43,13 @@ public void pop() {
   }
 
   @Override
-  public T addConstraint(BooleanFormula constraint) throws InterruptedException {
+  public T addConstraint(BooleanFormula constraint) throws InterruptedException, SolverException {
     clearAssumptions();
     return delegate.addConstraint(constraint);
   }
 
   @Override
-  public void push() throws InterruptedException {
+  public void push() throws InterruptedException, SolverException {
     clearAssumptions();
     delegate.push();
   }
@@ -80,12 +80,13 @@ public boolean isUnsatWithAssumptions(Collection<BooleanFormula> assumptions)
   protected void registerPushedFormula(@SuppressWarnings("unused") T pPushResult) {}
 
   @Override
-  public Model getModel() throws SolverException {
+  public Model getModel() throws SolverException, InterruptedException {
     return delegate.getModel();
   }
 
   @Override
-  public ImmutableList<Model.ValueAssignment> getModelAssignments() throws SolverException {
+  public ImmutableList<Model.ValueAssignment> getModelAssignments()
+      throws SolverException, InterruptedException {
     return delegate.getModelAssignments();
   }
 
diff --git a/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingBasicProverEnvironment.java b/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingBasicProverEnvironment.java
index c548d30384..3cc3f92d47 100644
--- a/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingBasicProverEnvironment.java
+++ b/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingBasicProverEnvironment.java
@@ -36,14 +36,15 @@ public void pop() {
   }
 
   @Override
-  public @Nullable T addConstraint(BooleanFormula constraint) throws InterruptedException {
+  public @Nullable T addConstraint(BooleanFormula constraint)
+      throws InterruptedException, SolverException {
     debugging.assertThreadLocal();
     debugging.assertFormulaInContext(constraint);
     return delegate.addConstraint(constraint);
   }
 
   @Override
-  public void push() throws InterruptedException {
+  public void push() throws InterruptedException, SolverException {
     debugging.assertThreadLocal();
     delegate.push();
   }
@@ -72,7 +73,7 @@ public boolean isUnsatWithAssumptions(Collection<BooleanFormula> assumptions)
 
   @SuppressWarnings("resource")
   @Override
-  public Model getModel() throws SolverException {
+  public Model getModel() throws SolverException, InterruptedException {
     debugging.assertThreadLocal();
     return new DebuggingModel(delegate.getModel(), debugging);
   }
diff --git a/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingModel.java b/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingModel.java
index 29b11eea9a..2f6c1a5cc8 100644
--- a/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingModel.java
+++ b/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingModel.java
@@ -23,6 +23,7 @@
 import org.sosy_lab.java_smt.api.Model;
 import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
 import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula;
+import org.sosy_lab.java_smt.api.SolverException;
 import org.sosy_lab.java_smt.api.StringFormula;
 
 public class DebuggingModel implements Model {
@@ -35,7 +36,8 @@ public class DebuggingModel implements Model {
   }
 
   @Override
-  public <T extends Formula> @Nullable T eval(T formula) {
+  public <T extends Formula> @Nullable T eval(T formula)
+      throws SolverException, InterruptedException {
     debugging.assertThreadLocal();
     debugging.assertFormulaInContext(formula);
     T result = delegate.eval(formula);
@@ -44,63 +46,70 @@ public class DebuggingModel implements Model {
   }
 
   @Override
-  public @Nullable Object evaluate(Formula formula) {
+  public @Nullable Object evaluate(Formula formula) throws SolverException, InterruptedException {
     debugging.assertThreadLocal();
     debugging.assertFormulaInContext(formula);
     return delegate.evaluate(formula);
   }
 
   @Override
-  public @Nullable BigInteger evaluate(IntegerFormula formula) {
+  public @Nullable BigInteger evaluate(IntegerFormula formula)
+      throws SolverException, InterruptedException {
     debugging.assertThreadLocal();
     debugging.assertFormulaInContext(formula);
     return delegate.evaluate(formula);
   }
 
   @Override
-  public @Nullable Rational evaluate(RationalFormula formula) {
+  public @Nullable Rational evaluate(RationalFormula formula)
+      throws SolverException, InterruptedException {
     debugging.assertThreadLocal();
     debugging.assertFormulaInContext(formula);
     return delegate.evaluate(formula);
   }
 
   @Override
-  public @Nullable Boolean evaluate(BooleanFormula formula) {
+  public @Nullable Boolean evaluate(BooleanFormula formula)
+      throws SolverException, InterruptedException {
     debugging.assertThreadLocal();
     debugging.assertFormulaInContext(formula);
     return delegate.evaluate(formula);
   }
 
   @Override
-  public @Nullable BigInteger evaluate(BitvectorFormula formula) {
+  public @Nullable BigInteger evaluate(BitvectorFormula formula)
+      throws SolverException, InterruptedException {
     debugging.assertThreadLocal();
     debugging.assertFormulaInContext(formula);
     return delegate.evaluate(formula);
   }
 
   @Override
-  public @Nullable String evaluate(StringFormula formula) {
+  public @Nullable String evaluate(StringFormula formula)
+      throws SolverException, InterruptedException {
     debugging.assertThreadLocal();
     debugging.assertFormulaInContext(formula);
     return delegate.evaluate(formula);
   }
 
   @Override
-  public @Nullable String evaluate(EnumerationFormula formula) {
+  public @Nullable String evaluate(EnumerationFormula formula)
+      throws SolverException, InterruptedException {
     debugging.assertThreadLocal();
     debugging.assertFormulaInContext(formula);
     return delegate.evaluate(formula);
   }
 
   @Override
-  public @Nullable FloatingPointNumber evaluate(FloatingPointFormula formula) {
+  public @Nullable FloatingPointNumber evaluate(FloatingPointFormula formula)
+      throws SolverException, InterruptedException {
     debugging.assertThreadLocal();
     debugging.assertFormulaInContext(formula);
     return delegate.evaluate(formula);
   }
 
   @Override
-  public ImmutableList<ValueAssignment> asList() {
+  public ImmutableList<ValueAssignment> asList() throws SolverException, InterruptedException {
     debugging.assertThreadLocal();
     ImmutableList<ValueAssignment> result = delegate.asList();
     for (ValueAssignment v : result) {
diff --git a/src/org/sosy_lab/java_smt/delegate/logging/LoggingBasicProverEnvironment.java b/src/org/sosy_lab/java_smt/delegate/logging/LoggingBasicProverEnvironment.java
index 2f194c6125..3e0124a223 100644
--- a/src/org/sosy_lab/java_smt/delegate/logging/LoggingBasicProverEnvironment.java
+++ b/src/org/sosy_lab/java_smt/delegate/logging/LoggingBasicProverEnvironment.java
@@ -39,7 +39,7 @@ class LoggingBasicProverEnvironment<T> implements BasicProverEnvironment<T> {
   }
 
   @Override
-  public @Nullable T push(BooleanFormula f) throws InterruptedException {
+  public @Nullable T push(BooleanFormula f) throws InterruptedException, SolverException {
     logger.log(Level.FINE, "up to level " + level++);
     logger.log(Level.FINE, "formula pushed:", f);
     return wrapped.push(f);
@@ -52,12 +52,13 @@ public void pop() {
   }
 
   @Override
-  public @Nullable T addConstraint(BooleanFormula constraint) throws InterruptedException {
+  public @Nullable T addConstraint(BooleanFormula constraint)
+      throws InterruptedException, SolverException {
     return wrapped.addConstraint(constraint);
   }
 
   @Override
-  public void push() throws InterruptedException {
+  public void push() throws InterruptedException, SolverException {
     logger.log(Level.FINE, "up to level " + level++);
     wrapped.push();
   }
@@ -87,14 +88,15 @@ public boolean isUnsatWithAssumptions(Collection<BooleanFormula> pAssumptions)
   }
 
   @Override
-  public Model getModel() throws SolverException {
+  public Model getModel() throws SolverException, InterruptedException {
     Model m = wrapped.getModel();
     logger.log(Level.FINE, "model", m);
     return m;
   }
 
   @Override
-  public ImmutableList<ValueAssignment> getModelAssignments() throws SolverException {
+  public ImmutableList<ValueAssignment> getModelAssignments()
+      throws SolverException, InterruptedException {
     ImmutableList<ValueAssignment> m = wrapped.getModelAssignments();
     logger.log(Level.FINE, "model", m);
     return m;
diff --git a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsBasicProverEnvironment.java b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsBasicProverEnvironment.java
index 49106d6324..f88e27cb9d 100644
--- a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsBasicProverEnvironment.java
+++ b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsBasicProverEnvironment.java
@@ -42,13 +42,14 @@ public void pop() {
   }
 
   @Override
-  public @Nullable T addConstraint(BooleanFormula pConstraint) throws InterruptedException {
+  public @Nullable T addConstraint(BooleanFormula pConstraint)
+      throws InterruptedException, SolverException {
     stats.constraint.getAndIncrement();
     return delegate.addConstraint(pConstraint);
   }
 
   @Override
-  public void push() throws InterruptedException {
+  public void push() throws InterruptedException, SolverException {
     stats.push.getAndIncrement();
     delegate.push();
   }
@@ -81,7 +82,7 @@ public boolean isUnsatWithAssumptions(Collection<BooleanFormula> pAssumptions)
 
   @SuppressWarnings("resource")
   @Override
-  public Model getModel() throws SolverException {
+  public Model getModel() throws SolverException, InterruptedException {
     stats.model.getAndIncrement();
     return new StatisticsModel(delegate.getModel(), stats);
   }
diff --git a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsModel.java b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsModel.java
index e16ae324e1..d64795021d 100644
--- a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsModel.java
+++ b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsModel.java
@@ -23,6 +23,7 @@
 import org.sosy_lab.java_smt.api.Model;
 import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
 import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula;
+import org.sosy_lab.java_smt.api.SolverException;
 import org.sosy_lab.java_smt.api.StringFormula;
 
 class StatisticsModel implements Model {
@@ -36,61 +37,68 @@ class StatisticsModel implements Model {
   }
 
   @Override
-  public <T extends Formula> @Nullable T eval(T pFormula) {
+  public <T extends Formula> @Nullable T eval(T pFormula)
+      throws SolverException, InterruptedException {
     stats.modelEvaluations.getAndIncrement();
     return delegate.eval(pFormula);
   }
 
   @Override
-  public @Nullable Object evaluate(Formula pF) {
+  public @Nullable Object evaluate(Formula pF) throws SolverException, InterruptedException {
     stats.modelEvaluations.getAndIncrement();
     return delegate.evaluate(pF);
   }
 
   @Override
-  public @Nullable BigInteger evaluate(IntegerFormula pF) {
+  public @Nullable BigInteger evaluate(IntegerFormula pF)
+      throws SolverException, InterruptedException {
     stats.modelEvaluations.getAndIncrement();
     return delegate.evaluate(pF);
   }
 
   @Override
-  public @Nullable Rational evaluate(RationalFormula pF) {
+  public @Nullable Rational evaluate(RationalFormula pF)
+      throws SolverException, InterruptedException {
     stats.modelEvaluations.getAndIncrement();
     return delegate.evaluate(pF);
   }
 
   @Override
-  public @Nullable Boolean evaluate(BooleanFormula pF) {
+  public @Nullable Boolean evaluate(BooleanFormula pF)
+      throws SolverException, InterruptedException {
     stats.modelEvaluations.getAndIncrement();
     return delegate.evaluate(pF);
   }
 
   @Override
-  public @Nullable BigInteger evaluate(BitvectorFormula pF) {
+  public @Nullable BigInteger evaluate(BitvectorFormula pF)
+      throws SolverException, InterruptedException {
     stats.modelEvaluations.getAndIncrement();
     return delegate.evaluate(pF);
   }
 
   @Override
-  public @Nullable String evaluate(StringFormula pF) {
+  public @Nullable String evaluate(StringFormula pF) throws SolverException, InterruptedException {
     stats.modelEvaluations.getAndIncrement();
     return delegate.evaluate(pF);
   }
 
   @Override
-  public @Nullable String evaluate(EnumerationFormula pF) {
+  public @Nullable String evaluate(EnumerationFormula pF)
+      throws SolverException, InterruptedException {
     stats.modelEvaluations.getAndIncrement();
     return delegate.evaluate(pF);
   }
 
   @Override
-  public @Nullable FloatingPointNumber evaluate(FloatingPointFormula pF) {
+  public @Nullable FloatingPointNumber evaluate(FloatingPointFormula pF)
+      throws SolverException, InterruptedException {
     stats.modelEvaluations.getAndIncrement();
     return delegate.evaluate(pF);
   }
 
   @Override
-  public ImmutableList<ValueAssignment> asList() {
+  public ImmutableList<ValueAssignment> asList() throws SolverException, InterruptedException {
     stats.modelListings.getAndIncrement();
     return delegate.asList();
   }
diff --git a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironment.java b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironment.java
index f0401c6db2..ef1c1f11a3 100644
--- a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironment.java
+++ b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironment.java
@@ -39,14 +39,15 @@ public void pop() {
   }
 
   @Override
-  public @Nullable T addConstraint(BooleanFormula pConstraint) throws InterruptedException {
+  public @Nullable T addConstraint(BooleanFormula pConstraint)
+      throws InterruptedException, SolverException {
     synchronized (sync) {
       return delegate.addConstraint(pConstraint);
     }
   }
 
   @Override
-  public void push() throws InterruptedException {
+  public void push() throws InterruptedException, SolverException {
     synchronized (sync) {
       delegate.push();
     }
@@ -76,7 +77,7 @@ public boolean isUnsatWithAssumptions(Collection<BooleanFormula> pAssumptions)
 
   @SuppressWarnings("resource")
   @Override
-  public Model getModel() throws SolverException {
+  public Model getModel() throws SolverException, InterruptedException {
     synchronized (sync) {
       return new SynchronizedModel(delegate.getModel(), sync);
     }
diff --git a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironmentWithContext.java b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironmentWithContext.java
index 43922ccc25..4ffe92e595 100644
--- a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironmentWithContext.java
+++ b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironmentWithContext.java
@@ -58,7 +58,8 @@ public void pop() {
   }
 
   @Override
-  public @Nullable T addConstraint(BooleanFormula pConstraint) throws InterruptedException {
+  public @Nullable T addConstraint(BooleanFormula pConstraint)
+      throws InterruptedException, SolverException {
     BooleanFormula constraint;
     synchronized (sync) {
       constraint = otherManager.translateFrom(pConstraint, manager);
@@ -67,7 +68,7 @@ public void pop() {
   }
 
   @Override
-  public void push() throws InterruptedException {
+  public void push() throws InterruptedException, SolverException {
     delegate.push();
   }
 
@@ -91,7 +92,7 @@ public boolean isUnsatWithAssumptions(Collection<BooleanFormula> pAssumptions)
 
   @SuppressWarnings("resource")
   @Override
-  public Model getModel() throws SolverException {
+  public Model getModel() throws SolverException, InterruptedException {
     synchronized (sync) {
       return new SynchronizedModelWithContext(delegate.getModel(), sync, manager, otherManager);
     }
diff --git a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedModel.java b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedModel.java
index 3ebd078170..dbdf186521 100644
--- a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedModel.java
+++ b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedModel.java
@@ -24,6 +24,7 @@
 import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
 import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula;
 import org.sosy_lab.java_smt.api.SolverContext;
+import org.sosy_lab.java_smt.api.SolverException;
 import org.sosy_lab.java_smt.api.StringFormula;
 
 class SynchronizedModel implements Model {
@@ -37,70 +38,77 @@ class SynchronizedModel implements Model {
   }
 
   @Override
-  public <T extends Formula> @Nullable T eval(T pFormula) {
+  public <T extends Formula> @Nullable T eval(T pFormula)
+      throws SolverException, InterruptedException {
     synchronized (sync) {
       return delegate.eval(pFormula);
     }
   }
 
   @Override
-  public @Nullable Object evaluate(Formula pF) {
+  public @Nullable Object evaluate(Formula pF) throws SolverException, InterruptedException {
     synchronized (sync) {
       return delegate.evaluate(pF);
     }
   }
 
   @Override
-  public @Nullable BigInteger evaluate(IntegerFormula pF) {
+  public @Nullable BigInteger evaluate(IntegerFormula pF)
+      throws SolverException, InterruptedException {
     synchronized (sync) {
       return delegate.evaluate(pF);
     }
   }
 
   @Override
-  public @Nullable Rational evaluate(RationalFormula pF) {
+  public @Nullable Rational evaluate(RationalFormula pF)
+      throws SolverException, InterruptedException {
     synchronized (sync) {
       return delegate.evaluate(pF);
     }
   }
 
   @Override
-  public @Nullable Boolean evaluate(BooleanFormula pF) {
+  public @Nullable Boolean evaluate(BooleanFormula pF)
+      throws SolverException, InterruptedException {
     synchronized (sync) {
       return delegate.evaluate(pF);
     }
   }
 
   @Override
-  public @Nullable BigInteger evaluate(BitvectorFormula pF) {
+  public @Nullable BigInteger evaluate(BitvectorFormula pF)
+      throws SolverException, InterruptedException {
     synchronized (sync) {
       return delegate.evaluate(pF);
     }
   }
 
   @Override
-  public @Nullable String evaluate(StringFormula pF) {
+  public @Nullable String evaluate(StringFormula pF) throws SolverException, InterruptedException {
     synchronized (sync) {
       return delegate.evaluate(pF);
     }
   }
 
   @Override
-  public @Nullable String evaluate(EnumerationFormula pF) {
+  public @Nullable String evaluate(EnumerationFormula pF)
+      throws SolverException, InterruptedException {
     synchronized (sync) {
       return delegate.evaluate(pF);
     }
   }
 
   @Override
-  public @Nullable FloatingPointNumber evaluate(FloatingPointFormula pF) {
+  public @Nullable FloatingPointNumber evaluate(FloatingPointFormula pF)
+      throws SolverException, InterruptedException {
     synchronized (sync) {
       return delegate.evaluate(pF);
     }
   }
 
   @Override
-  public ImmutableList<ValueAssignment> asList() {
+  public ImmutableList<ValueAssignment> asList() throws SolverException, InterruptedException {
     synchronized (sync) {
       return delegate.asList();
     }
diff --git a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedModelWithContext.java b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedModelWithContext.java
index e260776fce..a4ddc7b97d 100644
--- a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedModelWithContext.java
+++ b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedModelWithContext.java
@@ -25,6 +25,7 @@
 import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
 import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula;
 import org.sosy_lab.java_smt.api.SolverContext;
+import org.sosy_lab.java_smt.api.SolverException;
 import org.sosy_lab.java_smt.api.StringFormula;
 
 class SynchronizedModelWithContext implements Model {
@@ -66,7 +67,8 @@ class SynchronizedModelWithContext implements Model {
   }
 
   @Override
-  public @Nullable Boolean evaluate(BooleanFormula pF) {
+  public @Nullable Boolean evaluate(BooleanFormula pF)
+      throws SolverException, InterruptedException {
     BooleanFormula f;
     synchronized (sync) {
       f = otherManager.translateFrom(pF, manager);
diff --git a/src/org/sosy_lab/java_smt/example/NQueens.java b/src/org/sosy_lab/java_smt/example/NQueens.java
index 353e010c32..372acacc9d 100644
--- a/src/org/sosy_lab/java_smt/example/NQueens.java
+++ b/src/org/sosy_lab/java_smt/example/NQueens.java
@@ -260,7 +260,8 @@ private List<BooleanFormula> diagonalRule(BooleanFormula[][] symbols) {
    * @param col the column index of the cell to check.
    * @return true if a queen is placed on the cell, false otherwise.
    */
-  private boolean getValue(BooleanFormula[][] symbols, Model model, int row, int col) {
+  private boolean getValue(BooleanFormula[][] symbols, Model model, int row, int col)
+      throws SolverException, InterruptedException {
     return Boolean.TRUE.equals(model.evaluate(symbols[row][col]));
   }
 
diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaModel.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaModel.java
index 722fcaf05f..6b4da40af7 100644
--- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaModel.java
+++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaModel.java
@@ -235,4 +235,12 @@ private ValueAssignment getUFAssignment(Term pTerm) {
     Preconditions.checkState(!prover.isClosed(), "Cannot use model after prover is closed");
     return bitwuzlaEnv.get_value(formula);
   }
+
+  // Direct copy of evaluateImpl() without exceptions
+  @Override
+  protected final Object evaluateImpl(Term f) {
+    Preconditions.checkState(!isClosed());
+    Term evaluatedF = evalImpl(f);
+    return evaluatedF == null ? null : creator.convertValue(f, evaluatedF);
+  }
 }
diff --git a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorNativeApiTest.java b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorNativeApiTest.java
index 6df6f5b30e..eb83b21111 100644
--- a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorNativeApiTest.java
+++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorNativeApiTest.java
@@ -153,7 +153,7 @@ public void dumpVariableTest() throws InvalidConfigurationException {
 
   @Test
   public void dumpVariableWithAssertionsOnStackTest()
-      throws InvalidConfigurationException, InterruptedException {
+      throws InvalidConfigurationException, InterruptedException, SolverException {
     ConfigurationBuilder config = Configuration.builder();
     try (BoolectorSolverContext context =
         BoolectorSolverContext.create(
diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4Model.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4Model.java
index 483e9a8acf..d9b6027826 100644
--- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4Model.java
+++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4Model.java
@@ -119,4 +119,12 @@ private ValueAssignment getAssignment(Expr pKeyTerm) {
   public ImmutableList<ValueAssignment> asList() {
     return model;
   }
+
+  // Direct copy of evaluateImpl() without exceptions
+  @Override
+  protected final Object evaluateImpl(Expr f) {
+    Preconditions.checkState(!isClosed());
+    Expr evaluatedF = evalImpl(f);
+    return evaluatedF == null ? null : creator.convertValue(f, evaluatedF);
+  }
 }
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 3998fc59ff..76e37d77a5 100644
--- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java
+++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java
@@ -144,7 +144,7 @@ private void assertFormula(BooleanFormula pF) {
 
   @SuppressWarnings("resource")
   @Override
-  public CVC4Model getModel() throws SolverException {
+  public CVC4Model getModel() {
     Preconditions.checkState(!closed);
     Preconditions.checkState(!changedSinceLastSatQuery);
     checkGenerateModels();
@@ -183,10 +183,16 @@ private void setChanged() {
   }
 
   @Override
-  public ImmutableList<ValueAssignment> getModelAssignments() throws SolverException {
+  public ImmutableList<ValueAssignment> getModelAssignments()
+      throws SolverException, InterruptedException {
     Preconditions.checkState(!closed);
     Preconditions.checkState(!changedSinceLastSatQuery);
-    return super.getModelAssignments();
+    try {
+      return super.getModelAssignments();
+    } catch (SolverException | InterruptedException e) {
+      // These can not be thrown in OpenSMT2 model, so we can safely ignore this
+      throw new AssertionError(e);
+    }
   }
 
   @Override
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 85cfb0a23c..9d77dbe804 100644
--- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java
+++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java
@@ -150,7 +150,7 @@ protected String addConstraint0(BooleanFormula pF) {
 
   @SuppressWarnings("resource")
   @Override
-  public CVC5Model getModel() throws SolverException {
+  public CVC5Model getModel() {
     Preconditions.checkState(!closed);
     Preconditions.checkState(!changedSinceLastSatQuery);
     checkGenerateModels();
@@ -185,10 +185,15 @@ protected void setChanged() {
   }
 
   @Override
-  public ImmutableList<ValueAssignment> getModelAssignments() throws SolverException {
+  public ImmutableList<ValueAssignment> getModelAssignments() {
     Preconditions.checkState(!closed);
     Preconditions.checkState(!changedSinceLastSatQuery);
-    return super.getModelAssignments();
+    try {
+      return super.getModelAssignments();
+    } catch (SolverException | InterruptedException e) {
+      // These can not be thrown in OpenSMT2 model, so we can safely ignore this
+      throw new AssertionError(e);
+    }
   }
 
   @Override
diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Model.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Model.java
index dc57d3c5cf..effe237494 100644
--- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Model.java
+++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Model.java
@@ -206,4 +206,12 @@ private ValueAssignment getAssignment(Term pKeyTerm) {
   public ImmutableList<ValueAssignment> asList() {
     return model;
   }
+
+  // Direct copy of evaluateImpl() without exceptions
+  @Override
+  protected final Object evaluateImpl(Term f) {
+    Preconditions.checkState(!isClosed());
+    Term evaluatedF = evalImpl(f);
+    return evaluatedF == null ? null : creator.convertValue(f, evaluatedF);
+  }
 }
diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5Model.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5Model.java
index e3dfdd1d98..a16c3a5995 100644
--- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5Model.java
+++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5Model.java
@@ -13,7 +13,7 @@
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_is_array_type;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_array_read;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_eq;
-import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_model_create_iterator;
+import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_model_create_iterator_with_solver_exception;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_model_eval;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_model_iterator_has_next;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_model_iterator_next;
@@ -30,6 +30,7 @@
 import java.util.List;
 import java.util.NoSuchElementException;
 import java.util.Set;
+import org.sosy_lab.java_smt.api.SolverException;
 import org.sosy_lab.java_smt.basicimpl.AbstractModel;
 
 class Mathsat5Model extends AbstractModel<Long, Long, Long> {
@@ -48,12 +49,12 @@ class Mathsat5Model extends AbstractModel<Long, Long, Long> {
   }
 
   @Override
-  public ImmutableList<ValueAssignment> asList() {
+  public ImmutableList<ValueAssignment> asList() throws SolverException, InterruptedException {
     Preconditions.checkState(!isClosed());
     Preconditions.checkState(!prover.isClosed(), "cannot use model after prover is closed");
     ImmutableList.Builder<ValueAssignment> assignments = ImmutableList.builder();
 
-    long modelIterator = msat_model_create_iterator(model);
+    long modelIterator = msat_model_create_iterator_with_solver_exception(model);
     while (msat_model_iterator_has_next(modelIterator)) {
       long[] key = new long[1];
       long[] value = new long[1];
@@ -71,7 +72,8 @@ public ImmutableList<ValueAssignment> asList() {
     return assignments.build();
   }
 
-  private ValueAssignment getAssignment(long key, long value) {
+  private ValueAssignment getAssignment(long key, long value)
+      throws SolverException, InterruptedException {
     List<Object> argumentInterpretation = new ArrayList<>();
     for (int i = 0; i < msat_term_arity(key); i++) {
       long arg = msat_term_get_arg(key, i);
@@ -89,7 +91,8 @@ private ValueAssignment getAssignment(long key, long value) {
 
   /** split an array-assignment into several assignments for all positions. */
   private Collection<ValueAssignment> getArrayAssignments(
-      long symbol, long key, long array, List<Object> upperIndices) {
+      long symbol, long key, long array, List<Object> upperIndices)
+      throws SolverException, InterruptedException {
     Collection<ValueAssignment> assignments = new ArrayList<>();
     Set<Long> indices = new HashSet<>();
     while (msat_term_is_array_write(creator.getEnv(), array)) {
diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApi.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApi.java
index f0862ddaf8..699429b083 100644
--- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApi.java
+++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApi.java
@@ -780,8 +780,27 @@ private static native int msat_all_sat(
 
   public static native void msat_destroy_model(long model);
 
+  /**
+   * Only to be used in tests. Use msat_model_create_iterator_with_sneaky_solver_exception()
+   * instead, to throw a better exception in case of failures.
+   */
   public static native long msat_model_create_iterator(long model);
 
+  /**
+   * This method returns the result of msat_model_create_iterator(), however it throws a
+   * IllegalArgumentException due to a problem, it throws a SolverException, reflecting the problem
+   * better.
+   */
+  static long msat_model_create_iterator_with_solver_exception(long model) throws SolverException {
+    try {
+      return msat_model_create_iterator(model);
+    } catch (IllegalArgumentException iae) {
+      // This is not a bug in our or user code, but a problem of MathSAT. The context can still be
+      // used.
+      throw new SolverException(iae.getMessage() + ", model not available");
+    }
+  }
+
   /**
    * Evaluates the input term in the given model.
    *
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 845cd0ae9f..863266d45a 100644
--- a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java
+++ b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java
@@ -146,10 +146,16 @@ protected void setChanged() {
   }
 
   @Override
-  public ImmutableList<ValueAssignment> getModelAssignments() throws SolverException {
+  public ImmutableList<ValueAssignment> getModelAssignments()
+      throws SolverException, InterruptedException {
     Preconditions.checkState(!closed);
     Preconditions.checkState(!changedSinceLastSatQuery);
-    return super.getModelAssignments();
+    try {
+      return super.getModelAssignments();
+    } catch (SolverException | InterruptedException e) {
+      // These can not be thrown in OpenSMT2 model, so we can safely ignore this
+      throw new AssertionError(e);
+    }
   }
 
   /**
diff --git a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolModel.java b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolModel.java
index 8194f78c14..c4b0dd9982 100644
--- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolModel.java
+++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolModel.java
@@ -8,6 +8,7 @@
 
 package org.sosy_lab.java_smt.solvers.smtinterpol;
 
+import com.google.common.base.Preconditions;
 import com.google.common.collect.ImmutableList;
 import com.google.common.collect.ImmutableSet;
 import de.uni_freiburg.informatik.ultimate.logic.ApplicationTerm;
@@ -184,4 +185,12 @@ public void close() {}
   protected Term evalImpl(Term formula) {
     return model.evaluate(formula);
   }
+
+  // Direct copy of evaluateImpl() without exceptions
+  @Override
+  protected final Object evaluateImpl(Term f) {
+    Preconditions.checkState(!isClosed());
+    Term evaluatedF = evalImpl(f);
+    return evaluatedF == null ? null : creator.convertValue(f, evaluatedF);
+  }
 }
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 7da2fbdbf5..1d8beabc62 100644
--- a/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java
+++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java
@@ -104,25 +104,25 @@ protected void logSolverStack() throws SolverException {
 
   @SuppressWarnings("resource")
   @Override
-  public Model getModel() throws SolverException {
+  public Model getModel() throws SolverException, InterruptedException {
     Preconditions.checkState(!closed);
     checkGenerateModels();
     return new CachingModel(getEvaluatorWithoutChecks());
   }
 
   @Override
-  protected Z3Model getEvaluatorWithoutChecks() throws SolverException {
+  protected Z3Model getEvaluatorWithoutChecks() throws SolverException, InterruptedException {
     return new Z3Model(this, z3context, getZ3Model(), creator);
   }
 
-  protected abstract long getZ3Model() throws SolverException;
+  protected abstract long getZ3Model() throws SolverException, InterruptedException;
 
   protected abstract void assertContraint(long constraint);
 
   protected abstract void assertContraintAndTrack(long constraint, long symbol);
 
   @Override
-  protected Void addConstraintImpl(BooleanFormula f) throws InterruptedException {
+  protected Void addConstraintImpl(BooleanFormula f) throws InterruptedException, SolverException {
     Preconditions.checkState(!closed);
     long e = creator.extractInfo(f);
     try {
@@ -135,7 +135,7 @@ protected Void addConstraintImpl(BooleanFormula f) throws InterruptedException {
         assertContraint(e);
       }
     } catch (Z3Exception exception) {
-      throw creator.handleZ3ExceptionAsRuntimeException(exception);
+      throw creator.handleZ3Exception(exception);
     }
     return null;
   }
diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java
index bde94b3e5f..b064f5593c 100644
--- a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java
+++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java
@@ -173,30 +173,6 @@ final SolverException handleZ3Exception(Z3Exception e)
     throw new SolverException("Z3 has thrown an exception", e);
   }
 
-  /**
-   * This method handles a Z3Exception, however it only throws a RuntimeException. This method is
-   * used in places where we cannot throw a checked exception in JavaSMT due to API restrictions.
-   *
-   * @param e the Z3Exception to handle
-   * @return nothing, always throw a RuntimeException
-   * @throws RuntimeException always thrown for the given Z3Exception
-   */
-  final RuntimeException handleZ3ExceptionAsRuntimeException(Z3Exception e) {
-    try {
-      throw handleZ3Exception(e);
-    } catch (InterruptedException ex) {
-      Thread.currentThread().interrupt();
-      throw sneakyThrow(e);
-    } catch (SolverException ex) {
-      throw sneakyThrow(e);
-    }
-  }
-
-  @SuppressWarnings("unchecked")
-  private static <E extends Throwable> RuntimeException sneakyThrow(Throwable e) throws E {
-    throw (E) e;
-  }
-
   @Override
   public Long makeVariable(Long type, String varName) {
     long z3context = getEnv();
diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3Model.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3Model.java
index 916a511345..1b31cf4cbd 100644
--- a/src/org/sosy_lab/java_smt/solvers/z3/Z3Model.java
+++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3Model.java
@@ -23,6 +23,7 @@
 import java.util.Set;
 import java.util.regex.Pattern;
 import org.checkerframework.checker.nullness.qual.Nullable;
+import org.sosy_lab.java_smt.api.SolverException;
 import org.sosy_lab.java_smt.basicimpl.AbstractModel;
 import org.sosy_lab.java_smt.basicimpl.AbstractProver;
 
@@ -43,7 +44,7 @@ final class Z3Model extends AbstractModel<Long, Long, Long> {
   }
 
   @Override
-  public ImmutableList<ValueAssignment> asList() {
+  public ImmutableList<ValueAssignment> asList() throws SolverException, InterruptedException {
     Preconditions.checkState(!isClosed());
     ImmutableList.Builder<ValueAssignment> out = ImmutableList.builder();
 
@@ -67,7 +68,7 @@ public ImmutableList<ValueAssignment> asList() {
         Native.decRef(z3context, funcDecl);
       }
     } catch (Z3Exception e) {
-      throw z3creator.handleZ3ExceptionAsRuntimeException(e);
+      throw z3creator.handleZ3Exception(e);
     }
 
     return out.build();
@@ -92,7 +93,8 @@ private boolean isInternalSymbol(long funcDecl) {
   /**
    * @return ValueAssignments for a constant declaration in the model
    */
-  private Collection<ValueAssignment> getConstAssignments(long keyDecl) {
+  private Collection<ValueAssignment> getConstAssignments(long keyDecl)
+      throws SolverException, InterruptedException {
     Preconditions.checkArgument(
         Native.getArity(z3context, keyDecl) == 0, "Declaration is not a constant");
 
@@ -146,7 +148,7 @@ private Collection<ValueAssignment> getConstAssignments(long keyDecl) {
 
   /** unrolls an constant array assignment. */
   private Collection<ValueAssignment> getConstantArrayAssignment(
-      long arraySymbol, long value, long decl) {
+      long arraySymbol, long value, long decl) throws SolverException, InterruptedException {
 
     long arrayFormula = Native.mkConst(z3context, arraySymbol, Native.getSort(z3context, value));
     Native.incRef(z3context, arrayFormula);
@@ -212,7 +214,8 @@ private Collection<ValueAssignment> getConstantArrayAssignment(
    * @return a list of assignments {@code a[1]=0; a[2]=0; a[5]=0}.
    */
   private Collection<ValueAssignment> getArrayAssignments(
-      long arraySymbol, long arrayFormula, long value, List<Object> upperIndices) {
+      long arraySymbol, long arrayFormula, long value, List<Object> upperIndices)
+      throws SolverException, InterruptedException {
     long evalDecl = Native.getAsArrayFuncDecl(z3context, value);
     Native.incRef(z3context, evalDecl);
     long interp = Native.modelGetFuncInterp(z3context, model, evalDecl);
@@ -382,13 +385,13 @@ public void close() {
 
   @Override
   @Nullable
-  protected Long evalImpl(Long formula) {
+  protected Long evalImpl(Long formula) throws SolverException, InterruptedException {
     LongPtr resultPtr = new LongPtr();
     boolean satisfiableModel;
     try {
       satisfiableModel = Native.modelEval(z3context, model, formula, false, resultPtr);
     } catch (Z3Exception e) {
-      throw z3creator.handleZ3ExceptionAsRuntimeException(e);
+      throw z3creator.handleZ3Exception(e);
     }
     Preconditions.checkState(satisfiableModel);
     if (resultPtr.value == 0) {
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 3c87cf7739..e50b39cc50 100644
--- a/src/org/sosy_lab/java_smt/solvers/z3/Z3OptimizationProver.java
+++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3OptimizationProver.java
@@ -101,12 +101,12 @@ public OptStatus check() throws InterruptedException, SolverException {
   }
 
   @Override
-  protected void pushImpl() {
+  protected void pushImpl() throws SolverException, InterruptedException {
     push0();
     try {
       Native.optimizePush(z3context, z3optSolver);
     } catch (Z3Exception exception) {
-      throw creator.handleZ3ExceptionAsRuntimeException(exception);
+      throw creator.handleZ3Exception(exception);
     }
   }
 
@@ -197,11 +197,11 @@ private Optional<Rational> round(int handle, Rational epsilon, RoundingFunction
   }
 
   @Override
-  protected long getZ3Model() {
+  protected long getZ3Model() throws SolverException, InterruptedException {
     try {
       return Native.optimizeGetModel(z3context, z3optSolver);
     } catch (Z3Exception e) {
-      throw creator.handleZ3ExceptionAsRuntimeException(e);
+      throw creator.handleZ3Exception(e);
     }
   }
 
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 5ec0eae466..4c8deefb1e 100644
--- a/src/org/sosy_lab/java_smt/solvers/z3/Z3TheoremProver.java
+++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3TheoremProver.java
@@ -57,12 +57,12 @@ class Z3TheoremProver extends Z3AbstractProver implements ProverEnvironment {
   }
 
   @Override
-  protected void pushImpl() {
+  protected void pushImpl() throws SolverException, InterruptedException {
     push0();
     try {
       Native.solverPush(z3context, z3solver);
     } catch (Z3Exception exception) {
-      throw creator.handleZ3ExceptionAsRuntimeException(exception);
+      throw creator.handleZ3Exception(exception);
     }
   }
 
@@ -138,11 +138,11 @@ protected long getUnsatCore0() {
   }
 
   @Override
-  protected long getZ3Model() {
+  protected long getZ3Model() throws SolverException, InterruptedException {
     try {
       return Native.solverGetModel(z3context, z3solver);
     } catch (Z3Exception e) {
-      throw creator.handleZ3ExceptionAsRuntimeException(e);
+      throw creator.handleZ3Exception(e);
     }
   }
 
diff --git a/src/org/sosy_lab/java_smt/test/ModelEvaluationTest.java b/src/org/sosy_lab/java_smt/test/ModelEvaluationTest.java
index 8974490f3d..5efda13889 100644
--- a/src/org/sosy_lab/java_smt/test/ModelEvaluationTest.java
+++ b/src/org/sosy_lab/java_smt/test/ModelEvaluationTest.java
@@ -236,7 +236,8 @@ private List<BooleanFormula> getConstraints() {
     return constraints;
   }
 
-  private BooleanFormula getNewConstraints(int i, Evaluator m) {
+  private BooleanFormula getNewConstraints(int i, Evaluator m)
+      throws SolverException, InterruptedException {
     BooleanFormula x = bmgr.makeVariable("x" + i);
     // prover.push(m.evaluate(x) ? bmgr.not(x) : x);
     return m.evaluate(x) ? x : bmgr.not(x);
diff --git a/src/org/sosy_lab/java_smt/test/ProverEnvironmentSubjectTest.java b/src/org/sosy_lab/java_smt/test/ProverEnvironmentSubjectTest.java
index 743ea4b7d4..383a53bacf 100644
--- a/src/org/sosy_lab/java_smt/test/ProverEnvironmentSubjectTest.java
+++ b/src/org/sosy_lab/java_smt/test/ProverEnvironmentSubjectTest.java
@@ -51,7 +51,7 @@ public void testIsSatisfiableYes() throws SolverException, InterruptedException
   }
 
   @Test
-  public void testIsSatisfiableNo() throws InterruptedException {
+  public void testIsSatisfiableNo() throws InterruptedException, SolverException {
     requireUnsatCore();
     try (ProverEnvironment env =
         context.newProverEnvironment(
@@ -71,7 +71,7 @@ public void testIsUnsatisfiableYes() throws SolverException, InterruptedExceptio
   }
 
   @Test
-  public void testIsUnsatisfiableNo() throws InterruptedException {
+  public void testIsUnsatisfiableNo() throws InterruptedException, SolverException {
     requireModel();
     try (ProverEnvironment env = context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) {
       env.push(simpleFormula);
diff --git a/src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java b/src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java
index 3b3029a7d1..16b854cd4c 100644
--- a/src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java
+++ b/src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java
@@ -406,7 +406,7 @@ public void testConcurrentOptimization() {
    */
   @Test
   public void testConcurrentIntegerStack()
-      throws InvalidConfigurationException, InterruptedException {
+      throws InvalidConfigurationException, InterruptedException, SolverException {
     requireIntegers();
     requireConcurrentMultipleStackSupport();
     SolverContext context = initSolver();
@@ -439,7 +439,7 @@ public void testConcurrentIntegerStack()
    */
   @Test
   public void testConcurrentBitvectorStack()
-      throws InvalidConfigurationException, InterruptedException {
+      throws InvalidConfigurationException, InterruptedException, SolverException {
     requireBitvectors();
     requireConcurrentMultipleStackSupport();
     SolverContext context = initSolver();
diff --git a/src/org/sosy_lab/java_smt/test/SolverContextTest.java b/src/org/sosy_lab/java_smt/test/SolverContextTest.java
index af349e5053..2b206fa03d 100644
--- a/src/org/sosy_lab/java_smt/test/SolverContextTest.java
+++ b/src/org/sosy_lab/java_smt/test/SolverContextTest.java
@@ -146,7 +146,7 @@ public void testCVC5WithValidOptions() throws InvalidConfigurationException {
   @Test(timeout = 5000)
   @SuppressWarnings({"try", "CheckReturnValue"})
   public void testCVC5WithValidOptionsTimeLimit()
-      throws InvalidConfigurationException, InterruptedException {
+      throws InvalidConfigurationException, InterruptedException, SolverException {
     assume().that(solverToUse()).isEqualTo(Solvers.CVC5);
 
     //  tlimit-per is time limit in ms of wall clock time per query
diff --git a/src/org/sosy_lab/java_smt/test/SolverStackTest0.java b/src/org/sosy_lab/java_smt/test/SolverStackTest0.java
index 6bbcdae4c8..74322eee55 100644
--- a/src/org/sosy_lab/java_smt/test/SolverStackTest0.java
+++ b/src/org/sosy_lab/java_smt/test/SolverStackTest0.java
@@ -194,7 +194,7 @@ public void stackTest() {
   }
 
   @Test
-  public void stackTest2() throws InterruptedException {
+  public void stackTest2() throws InterruptedException, SolverException {
     BasicProverEnvironment<?> stack = newEnvironmentForTest(context);
     stack.push();
     assertThat(stack.size()).isEqualTo(1);
@@ -203,7 +203,7 @@ public void stackTest2() throws InterruptedException {
   }
 
   @Test
-  public void stackTest3() throws InterruptedException {
+  public void stackTest3() throws InterruptedException, SolverException {
     BasicProverEnvironment<?> stack = newEnvironmentForTest(context);
     stack.push();
     assertThat(stack.size()).isEqualTo(1);
@@ -216,7 +216,7 @@ public void stackTest3() throws InterruptedException {
   }
 
   @Test
-  public void stackTest4() throws InterruptedException {
+  public void stackTest4() throws InterruptedException, SolverException {
     BasicProverEnvironment<?> stack = newEnvironmentForTest(context);
     stack.push();
     stack.push();
@@ -262,7 +262,7 @@ public void largerStackUsageTest() throws InterruptedException, SolverException
   }
 
   @Test
-  public void stackTest5() throws InterruptedException {
+  public void stackTest5() throws InterruptedException, SolverException {
     BasicProverEnvironment<?> stack = newEnvironmentForTest(context);
     stack.push();
     stack.pop();
@@ -508,7 +508,7 @@ public void multiStackTest() throws SolverException, InterruptedException {
   }
 
   @Test
-  public void avoidDualStacksIfNotSupported() throws InterruptedException {
+  public void avoidDualStacksIfNotSupported() throws InterruptedException, SolverException {
     assume()
         .withMessage("Solver does not support multiple stacks yet")
         .that(solver)
diff --git a/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java b/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java
index a08232a24a..f529528ae9 100644
--- a/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java
+++ b/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java
@@ -262,7 +262,8 @@ public <T> void localInterpolationTest() throws InterruptedException, SolverExce
 
   @SuppressWarnings({"unchecked", "resource"})
   @Test
-  public <T> void nonLocalInterpolationTest() throws InterruptedException, ExecutionException {
+  public <T> void nonLocalInterpolationTest()
+      throws InterruptedException, ExecutionException, SolverException {
     requireIntegers();
     requireInterpolation();
     assume().that(solverToUse()).isNotEqualTo(Solvers.CVC5);
diff --git a/src/org/sosy_lab/java_smt/test/TimeoutTest.java b/src/org/sosy_lab/java_smt/test/TimeoutTest.java
index 59d6d6a0c3..050848df92 100644
--- a/src/org/sosy_lab/java_smt/test/TimeoutTest.java
+++ b/src/org/sosy_lab/java_smt/test/TimeoutTest.java
@@ -24,6 +24,7 @@
 import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
 import org.sosy_lab.java_smt.api.BasicProverEnvironment;
 import org.sosy_lab.java_smt.api.BooleanFormula;
+import org.sosy_lab.java_smt.api.SolverException;
 import org.sosy_lab.java_smt.api.Tactic;
 import org.sosy_lab.java_smt.solvers.opensmt.Logics;
 
@@ -88,39 +89,39 @@ public void testTacticTimeout() {
   }
 
   @Test(timeout = TIMEOUT_MILLISECONDS)
-  public void testProverTimeoutInt() throws InterruptedException {
+  public void testProverTimeoutInt() throws InterruptedException, SolverException {
     requireIntegers();
     testBasicProverTimeoutInt(() -> context.newProverEnvironment());
   }
 
   @Test(timeout = TIMEOUT_MILLISECONDS)
-  public void testProverTimeoutBv() throws InterruptedException {
+  public void testProverTimeoutBv() throws InterruptedException, SolverException {
     requireBitvectors();
     testBasicProverTimeoutBv(() -> context.newProverEnvironment());
   }
 
   @Test(timeout = TIMEOUT_MILLISECONDS)
-  public void testInterpolationProverTimeout() throws InterruptedException {
+  public void testInterpolationProverTimeout() throws InterruptedException, SolverException {
     requireInterpolation();
     requireIntegers();
     testBasicProverTimeoutInt(() -> context.newProverEnvironmentWithInterpolation());
   }
 
   @Test(timeout = TIMEOUT_MILLISECONDS)
-  public void testOptimizationProverTimeout() throws InterruptedException {
+  public void testOptimizationProverTimeout() throws InterruptedException, SolverException {
     requireOptimization();
     requireIntegers();
     testBasicProverTimeoutInt(() -> context.newOptimizationProverEnvironment());
   }
 
   private void testBasicProverTimeoutInt(Supplier<BasicProverEnvironment<?>> proverConstructor)
-      throws InterruptedException {
+      throws InterruptedException, SolverException {
     HardIntegerFormulaGenerator gen = new HardIntegerFormulaGenerator(imgr, bmgr);
     testBasicProverTimeout(proverConstructor, gen.generate(200));
   }
 
   private void testBasicProverTimeoutBv(Supplier<BasicProverEnvironment<?>> proverConstructor)
-      throws InterruptedException {
+      throws InterruptedException, SolverException {
     HardBitvectorFormulaGenerator gen = new HardBitvectorFormulaGenerator(bvmgr, bmgr);
     testBasicProverTimeout(proverConstructor, gen.generate(200));
   }
@@ -128,7 +129,7 @@ private void testBasicProverTimeoutBv(Supplier<BasicProverEnvironment<?>> prover
   @SuppressWarnings("CheckReturnValue")
   private void testBasicProverTimeout(
       Supplier<BasicProverEnvironment<?>> proverConstructor, BooleanFormula instance)
-      throws InterruptedException {
+      throws InterruptedException, SolverException {
     Thread t =
         new Thread(
             () -> {