From c4a7a6521234b084a79556e01ba8be7476f91ae0 Mon Sep 17 00:00:00 2001
From: BaierD <daniel.baier@sosy.ifi.lmu.de>
Date: Tue, 29 Jul 2025 16:07:40 +0200
Subject: [PATCH 01/19] Add warning for sneaky SolverExceptions in Model
 JavaDoc

---
 src/org/sosy_lab/java_smt/api/Model.java | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/src/org/sosy_lab/java_smt/api/Model.java b/src/org/sosy_lab/java_smt/api/Model.java
index 27a5e7a9b1..b4c772a04f 100644
--- a/src/org/sosy_lab/java_smt/api/Model.java
+++ b/src/org/sosy_lab/java_smt/api/Model.java
@@ -49,13 +49,21 @@ 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 might throw an unchecked {@link SolverException} as an extension of {@link
+   * Throwable}.
    */
   @Override
   default Iterator<ValueAssignment> iterator() {
     return asList().iterator();
   }
 
-  /** Build a list of assignments that stays valid after closing the model. */
+  /**
+   * Build a list of assignments that stays valid after closing the model.
+   *
+   * <p>Warning: this might throw an unchecked {@link SolverException} as an extension of {@link
+   * Throwable}.
+   */
   ImmutableList<ValueAssignment> asList();
 
   /**

From b7da958d4c315cc0d5fe3da72b3121b2a5a4d81c Mon Sep 17 00:00:00 2001
From: BaierD <daniel.baier@sosy.ifi.lmu.de>
Date: Tue, 29 Jul 2025 16:08:20 +0200
Subject: [PATCH 02/19] Throw sneaky SolverExceptions in Mathsat Model instead
 of confusing IllegalArgumentException for msat_model_create_iterator()

---
 .../solvers/mathsat5/Mathsat5Model.java       |  4 ++--
 .../solvers/mathsat5/Mathsat5NativeApi.java   | 24 +++++++++++++++++++
 2 files changed, 26 insertions(+), 2 deletions(-)

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..3b7266262c 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_sneaky_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;
@@ -53,7 +53,7 @@ public ImmutableList<ValueAssignment> asList() {
     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_sneaky_solver_exception(model);
     while (msat_model_iterator_has_next(modelIterator)) {
       long[] key = new long[1];
       long[] value = new long[1];
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..45e7a0129b 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,32 @@ 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. This method is used in places where we cannot throw a checked exception in JavaSMT due
+   * to API restrictions.
+   */
+  static long msat_model_create_iterator_with_sneaky_solver_exception(long model) {
+    try {
+      return msat_model_create_iterator(model);
+    } catch (IllegalArgumentException iae) {
+      // This is not a bug in our code, but a problem of MathSAT. The context can still be used.
+      throw sneakyThrow(new SolverException(iae.getMessage() + ", model" + " not available"));
+    }
+  }
+
+  @SuppressWarnings("unchecked")
+  private static <E extends Throwable> RuntimeException sneakyThrow(Throwable e) throws E {
+    throw (E) e;
+  }
+
   /**
    * Evaluates the input term in the given model.
    *

From 50094eb4458feea3ede5798e076dff02c0dc93d9 Mon Sep 17 00:00:00 2001
From: BaierD <daniel.baier@sosy.ifi.lmu.de>
Date: Tue, 29 Jul 2025 16:17:59 +0200
Subject: [PATCH 03/19] Add more sneaky throw warnings to API that may throw a
 SolverException as Throwable (due to Z3)

---
 .../java_smt/api/BasicProverEnvironment.java  | 10 ++++++-
 src/org/sosy_lab/java_smt/api/Evaluator.java  | 27 +++++++++++++++++++
 2 files changed, 36 insertions(+), 1 deletion(-)

diff --git a/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java b/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java
index dd086f6728..75903650b4 100644
--- a/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java
+++ b/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java
@@ -29,6 +29,9 @@ public interface BasicProverEnvironment<T> extends AutoCloseable {
    * Push a backtracking point and add a formula to the current stack, asserting it. The return
    * value may be used to identify this formula later on in a query (this depends on the subtype of
    * the environment).
+   *
+   * <p>Warning: this might throw an unchecked {@link SolverException} as an extension of {@link
+   * Throwable}.
    */
   @Nullable
   @CanIgnoreReturnValue
@@ -43,7 +46,12 @@ default T push(BooleanFormula f) throws InterruptedException {
    */
   void pop();
 
-  /** Add a constraint to the latest backtracking point. */
+  /**
+   * Add a constraint to the latest backtracking point.
+   *
+   * <p>Warning: this might throw an unchecked {@link SolverException} as an extension of {@link
+   * Throwable}.
+   */
   @Nullable
   @CanIgnoreReturnValue
   T addConstraint(BooleanFormula constraint) throws InterruptedException;
diff --git a/src/org/sosy_lab/java_smt/api/Evaluator.java b/src/org/sosy_lab/java_smt/api/Evaluator.java
index 03ca8b00a0..44d0f37173 100644
--- a/src/org/sosy_lab/java_smt/api/Evaluator.java
+++ b/src/org/sosy_lab/java_smt/api/Evaluator.java
@@ -43,6 +43,9 @@ public interface Evaluator extends AutoCloseable {
    * will replace all symbols from the formula with their model values and then simplify the formula
    * into a simple formula, e.g., consisting only of a numeral expression.
    *
+   * <p>Warning: this might throw an unchecked {@link SolverException} as an extension of {@link
+   * Throwable}.
+   *
    * @param formula Input formula to be evaluated.
    * @return evaluation of the given formula or <code>null</code> if the solver does not provide a
    *     better evaluation.
@@ -58,6 +61,9 @@ public interface Evaluator extends AutoCloseable {
    *
    * <p>The formula does not need to be a variable, we also allow complex expression.
    *
+   * <p>Warning: this might throw an unchecked {@link SolverException} as an extension of {@link
+   * Throwable}.
+   *
    * @param formula Input formula
    * @return Either of: - Number (Rational/Double/BigInteger/Long/Integer) - Boolean
    * @throws IllegalArgumentException if a formula has unexpected type, e.g. Array.
@@ -68,6 +74,9 @@ public interface Evaluator extends AutoCloseable {
    * Type-safe evaluation for integer formulas.
    *
    * <p>The formula does not need to be a variable, we also allow complex expression.
+   *
+   * <p>Warning: this might throw an unchecked {@link SolverException} as an extension of {@link
+   * Throwable}.
    */
   @Nullable BigInteger evaluate(IntegerFormula formula);
 
@@ -75,6 +84,9 @@ public interface Evaluator extends AutoCloseable {
    * Type-safe evaluation for rational formulas.
    *
    * <p>The formula does not need to be a variable, we also allow complex expression.
+   *
+   * <p>Warning: this might throw an unchecked {@link SolverException} as an extension of {@link
+   * Throwable}.
    */
   @Nullable Rational evaluate(RationalFormula formula);
 
@@ -82,6 +94,9 @@ public interface Evaluator extends AutoCloseable {
    * Type-safe evaluation for boolean formulas.
    *
    * <p>The formula does not need to be a variable, we also allow complex expression.
+   *
+   * <p>Warning: this might throw an unchecked {@link SolverException} as an extension of {@link
+   * Throwable}.
    */
   @Nullable Boolean evaluate(BooleanFormula formula);
 
@@ -89,6 +104,9 @@ public interface Evaluator extends AutoCloseable {
    * Type-safe evaluation for bitvector formulas.
    *
    * <p>The formula does not need to be a variable, we also allow complex expression.
+   *
+   * <p>Warning: this might throw an unchecked {@link SolverException} as an extension of {@link
+   * Throwable}.
    */
   @Nullable BigInteger evaluate(BitvectorFormula formula);
 
@@ -96,6 +114,9 @@ public interface Evaluator extends AutoCloseable {
    * Type-safe evaluation for string formulas.
    *
    * <p>The formula does not need to be a variable, we also allow complex expression.
+   *
+   * <p>Warning: this might throw an unchecked {@link SolverException} as an extension of {@link
+   * Throwable}.
    */
   @Nullable String evaluate(StringFormula formula);
 
@@ -103,6 +124,9 @@ public interface Evaluator extends AutoCloseable {
    * Type-safe evaluation for enumeration formulas.
    *
    * <p>The formula does not need to be a variable, we also allow complex expression.
+   *
+   * <p>Warning: this might throw an unchecked {@link SolverException} as an extension of {@link
+   * Throwable}.
    */
   @Nullable String evaluate(EnumerationFormula formula);
 
@@ -110,6 +134,9 @@ public interface Evaluator extends AutoCloseable {
    * Type-safe evaluation for floating-point formulas.
    *
    * <p>The formula does not need to be a variable, we also allow complex expression.
+   *
+   * <p>Warning: this might throw an unchecked {@link SolverException} as an extension of {@link
+   * Throwable}.
    */
   @Nullable FloatingPointNumber evaluate(FloatingPointFormula formula);
 

From 89837d5407139345870aec020e2ca1d8b9c7350e Mon Sep 17 00:00:00 2001
From: BaierD <daniel.baier@sosy.ifi.lmu.de>
Date: Wed, 30 Jul 2025 16:04:18 +0200
Subject: [PATCH 04/19] Remove sneaky throw of SolverException from Mathsat
 native call

---
 .../solvers/mathsat5/Mathsat5NativeApi.java       | 15 +++++----------
 1 file changed, 5 insertions(+), 10 deletions(-)

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 45e7a0129b..699429b083 100644
--- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApi.java
+++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApi.java
@@ -789,23 +789,18 @@ private static native int msat_all_sat(
   /**
    * 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. This method is used in places where we cannot throw a checked exception in JavaSMT due
-   * to API restrictions.
+   * better.
    */
-  static long msat_model_create_iterator_with_sneaky_solver_exception(long model) {
+  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 code, but a problem of MathSAT. The context can still be used.
-      throw sneakyThrow(new SolverException(iae.getMessage() + ", model" + " not available"));
+      // 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");
     }
   }
 
-  @SuppressWarnings("unchecked")
-  private static <E extends Throwable> RuntimeException sneakyThrow(Throwable e) throws E {
-    throw (E) e;
-  }
-
   /**
    * Evaluates the input term in the given model.
    *

From dbbdc318e20c67762de2aae7e6fa300188b6ce2d Mon Sep 17 00:00:00 2001
From: BaierD <daniel.baier@sosy.ifi.lmu.de>
Date: Wed, 30 Jul 2025 16:05:48 +0200
Subject: [PATCH 05/19] Remove sneaky throw of SolverException from Z3 model
 and add InterruptedException to it

---
 .../java_smt/solvers/z3/Z3AbstractProver.java   |  6 +++---
 .../sosy_lab/java_smt/solvers/z3/Z3Model.java   | 17 ++++++++++-------
 .../java_smt/solvers/z3/Z3TheoremProver.java    |  4 ++--
 3 files changed, 15 insertions(+), 12 deletions(-)

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..10cdd2f6dc 100644
--- a/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java
+++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java
@@ -104,18 +104,18 @@ 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);
 
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/Z3TheoremProver.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3TheoremProver.java
index 5ec0eae466..5b1f4720d7 100644
--- a/src/org/sosy_lab/java_smt/solvers/z3/Z3TheoremProver.java
+++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3TheoremProver.java
@@ -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);
     }
   }
 

From b0e7b444420926f59c71b531607b5352936953a2 Mon Sep 17 00:00:00 2001
From: BaierD <daniel.baier@sosy.ifi.lmu.de>
Date: Wed, 30 Jul 2025 16:06:28 +0200
Subject: [PATCH 06/19] Add SolverException and InterruptedException to many
 calls related to the Model

---
 .../java_smt/api/BasicProverEnvironment.java  |  7 +++--
 src/org/sosy_lab/java_smt/api/Evaluator.java  | 28 +++++++++---------
 src/org/sosy_lab/java_smt/api/Model.java      | 17 ++++++++---
 .../api/OptimizationProverEnvironment.java    |  2 +-
 .../java_smt/basicimpl/AbstractEvaluator.java | 26 ++++++++++-------
 .../java_smt/basicimpl/CachingModel.java      | 29 ++++++++++++-------
 .../BasicProverWithAssumptionsWrapper.java    |  5 ++--
 .../DebuggingBasicProverEnvironment.java      |  2 +-
 .../delegate/debugging/DebuggingModel.java    | 29 ++++++++++++-------
 .../LoggingBasicProverEnvironment.java        |  5 ++--
 .../StatisticsBasicProverEnvironment.java     |  2 +-
 .../delegate/statistics/StatisticsModel.java  | 28 +++++++++++-------
 .../SynchronizedBasicProverEnvironment.java   |  2 +-
 ...izedBasicProverEnvironmentWithContext.java |  2 +-
 .../synchronize/SynchronizedModel.java        | 28 +++++++++++-------
 .../SynchronizedModelWithContext.java         |  4 ++-
 .../sosy_lab/java_smt/example/NQueens.java    |  3 +-
 .../solvers/bitwuzla/BitwuzlaModel.java       |  9 ++++--
 .../java_smt/solvers/cvc4/CVC4Model.java      | 13 ++++++---
 .../solvers/cvc4/CVC4TheoremProver.java       |  5 ++--
 .../solvers/cvc5/CVC5AbstractProver.java      |  5 ++--
 .../java_smt/solvers/cvc5/CVC5Model.java      | 16 ++++++----
 .../solvers/mathsat5/Mathsat5Model.java       | 13 +++++----
 .../opensmt/OpenSmtAbstractProver.java        |  3 +-
 .../solvers/smtinterpol/SmtInterpolModel.java | 12 +++++---
 .../java_smt/test/ModelEvaluationTest.java    |  3 +-
 26 files changed, 187 insertions(+), 111 deletions(-)

diff --git a/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java b/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java
index 75903650b4..58f13f099d 100644
--- a/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java
+++ b/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java
@@ -95,7 +95,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
@@ -103,7 +103,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();
   }
 
@@ -115,7 +115,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 44d0f37173..6ea3f2e31a 100644
--- a/src/org/sosy_lab/java_smt/api/Evaluator.java
+++ b/src/org/sosy_lab/java_smt/api/Evaluator.java
@@ -43,14 +43,11 @@ public interface Evaluator extends AutoCloseable {
    * will replace all symbols from the formula with their model values and then simplify the formula
    * into a simple formula, e.g., consisting only of a numeral expression.
    *
-   * <p>Warning: this might throw an unchecked {@link SolverException} as an extension of {@link
-   * Throwable}.
-   *
    * @param formula Input formula to be evaluated.
    * @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.
@@ -61,14 +58,11 @@ public interface Evaluator extends AutoCloseable {
    *
    * <p>The formula does not need to be a variable, we also allow complex expression.
    *
-   * <p>Warning: this might throw an unchecked {@link SolverException} as an extension of {@link
-   * Throwable}.
-   *
    * @param formula Input formula
    * @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.
@@ -78,7 +72,8 @@ public interface Evaluator extends AutoCloseable {
    * <p>Warning: this might throw an unchecked {@link SolverException} as an extension of {@link
    * Throwable}.
    */
-  @Nullable BigInteger evaluate(IntegerFormula formula);
+  @Nullable BigInteger evaluate(IntegerFormula formula)
+      throws SolverException, InterruptedException;
 
   /**
    * Type-safe evaluation for rational formulas.
@@ -88,7 +83,7 @@ public interface Evaluator extends AutoCloseable {
    * <p>Warning: this might throw an unchecked {@link SolverException} as an extension of {@link
    * Throwable}.
    */
-  @Nullable Rational evaluate(RationalFormula formula);
+  @Nullable Rational evaluate(RationalFormula formula) throws SolverException, InterruptedException;
 
   /**
    * Type-safe evaluation for boolean formulas.
@@ -98,7 +93,7 @@ public interface Evaluator extends AutoCloseable {
    * <p>Warning: this might throw an unchecked {@link SolverException} as an extension of {@link
    * Throwable}.
    */
-  @Nullable Boolean evaluate(BooleanFormula formula);
+  @Nullable Boolean evaluate(BooleanFormula formula) throws SolverException, InterruptedException;
 
   /**
    * Type-safe evaluation for bitvector formulas.
@@ -108,7 +103,8 @@ public interface Evaluator extends AutoCloseable {
    * <p>Warning: this might throw an unchecked {@link SolverException} as an extension of {@link
    * Throwable}.
    */
-  @Nullable BigInteger evaluate(BitvectorFormula formula);
+  @Nullable BigInteger evaluate(BitvectorFormula formula)
+      throws SolverException, InterruptedException;
 
   /**
    * Type-safe evaluation for string formulas.
@@ -118,7 +114,7 @@ public interface Evaluator extends AutoCloseable {
    * <p>Warning: this might throw an unchecked {@link SolverException} as an extension of {@link
    * Throwable}.
    */
-  @Nullable String evaluate(StringFormula formula);
+  @Nullable String evaluate(StringFormula formula) throws SolverException, InterruptedException;
 
   /**
    * Type-safe evaluation for enumeration formulas.
@@ -128,7 +124,8 @@ public interface Evaluator extends AutoCloseable {
    * <p>Warning: this might throw an unchecked {@link SolverException} as an extension of {@link
    * Throwable}.
    */
-  @Nullable String evaluate(EnumerationFormula formula);
+  @Nullable String evaluate(EnumerationFormula formula)
+      throws SolverException, InterruptedException;
 
   /**
    * Type-safe evaluation for floating-point formulas.
@@ -138,7 +135,8 @@ public interface Evaluator extends AutoCloseable {
    * <p>Warning: this might throw an unchecked {@link SolverException} as an extension of {@link
    * Throwable}.
    */
-  @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 b4c772a04f..8b4ac5fa3b 100644
--- a/src/org/sosy_lab/java_smt/api/Model.java
+++ b/src/org/sosy_lab/java_smt/api/Model.java
@@ -50,12 +50,21 @@ public interface Model extends Evaluator, Iterable<ValueAssignment>, AutoCloseab
    *       Please use a direct evaluation query to get the evaluation in such a case.
    * </ul>
    *
-   * <p>Warning: this might throw an unchecked {@link SolverException} as an extension of {@link
-   * Throwable}.
+   * <p>Warning: this might throw {@link SolverException} or {@link InterruptedException} as {@link
+   * RuntimeException} as checked exceptions are not supported by this method.
    */
   @Override
   default Iterator<ValueAssignment> iterator() {
-    return asList().iterator();
+    try {
+      return asList().iterator();
+    } catch (SolverException | InterruptedException pE) {
+      throw sneakyThrow(pE);
+    }
+  }
+
+  @SuppressWarnings("unchecked")
+  private static <E extends Throwable> RuntimeException sneakyThrow(Throwable e) throws E {
+    throw (E) e;
   }
 
   /**
@@ -64,7 +73,7 @@ default Iterator<ValueAssignment> iterator() {
    * <p>Warning: this might throw an unchecked {@link SolverException} as an extension of {@link
    * Throwable}.
    */
-  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..53432744a1 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 final 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/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..3afcbe0a41 100644
--- a/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/BasicProverWithAssumptionsWrapper.java
+++ b/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/BasicProverWithAssumptionsWrapper.java
@@ -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..33e2ef8756 100644
--- a/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingBasicProverEnvironment.java
+++ b/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingBasicProverEnvironment.java
@@ -72,7 +72,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..78cb934251 100644
--- a/src/org/sosy_lab/java_smt/delegate/logging/LoggingBasicProverEnvironment.java
+++ b/src/org/sosy_lab/java_smt/delegate/logging/LoggingBasicProverEnvironment.java
@@ -87,14 +87,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..1d5c7ece0f 100644
--- a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsBasicProverEnvironment.java
+++ b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsBasicProverEnvironment.java
@@ -81,7 +81,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..fa79246d01 100644
--- a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironment.java
+++ b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironment.java
@@ -76,7 +76,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..4fecf91550 100644
--- a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironmentWithContext.java
+++ b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironmentWithContext.java
@@ -91,7 +91,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..7c031e0833 100644
--- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaModel.java
+++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaModel.java
@@ -19,6 +19,7 @@
 import java.util.List;
 import java.util.Set;
 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.solvers.bitwuzla.api.Bitwuzla;
 import org.sosy_lab.java_smt.solvers.bitwuzla.api.Kind;
@@ -50,7 +51,7 @@ protected BitwuzlaModel(
 
   /** Build a list of assignments that stays valid after closing the model. */
   @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");
     ImmutableSet.Builder<ValueAssignment> variablesBuilder = ImmutableSet.builder();
@@ -108,13 +109,15 @@ private ValueAssignment getSimpleAssignment(Term pTerm) {
         argumentInterpretation);
   }
 
-  private Collection<ValueAssignment> getArrayAssignment(Term pTerm) {
+  private Collection<ValueAssignment> getArrayAssignment(Term pTerm)
+      throws SolverException, InterruptedException {
     return getArrayAssignments(pTerm, ImmutableList.of());
   }
 
   // TODO: check this in detail. I think this might be incomplete.
   // We should add more Model tests in general. As most are parsing and int based!
-  private Collection<ValueAssignment> getArrayAssignments(Term pTerm, List<Object> upperIndices) {
+  private Collection<ValueAssignment> getArrayAssignments(Term pTerm, List<Object> upperIndices)
+      throws SolverException, InterruptedException {
     // Array children for store are structured in the following way:
     // {starting array, index, value} in "we add value at index to array"
     // Selections are structured: {starting array, index}
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..ca99cc5c72 100644
--- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4Model.java
+++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4Model.java
@@ -21,6 +21,7 @@
 import java.util.List;
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.Formula;
+import org.sosy_lab.java_smt.api.SolverException;
 import org.sosy_lab.java_smt.basicimpl.AbstractModel;
 
 public class CVC4Model extends AbstractModel<Expr, Type, ExprManager> {
@@ -34,7 +35,8 @@ public class CVC4Model extends AbstractModel<Expr, Type, ExprManager> {
       CVC4TheoremProver pProver,
       CVC4FormulaCreator pCreator,
       SmtEngine pSmtEngine,
-      Collection<Expr> pAssertedExpressions) {
+      Collection<Expr> pAssertedExpressions)
+      throws SolverException, InterruptedException {
     super(pProver, pCreator);
     smtEngine = pSmtEngine;
     prover = pProver;
@@ -60,7 +62,8 @@ private Expr getValue(Expr f) {
     return prover.exportExpr(smtEngine.getValue(prover.importExpr(f)));
   }
 
-  private ImmutableList<ValueAssignment> generateModel() {
+  private ImmutableList<ValueAssignment> generateModel()
+      throws SolverException, InterruptedException {
     ImmutableSet.Builder<ValueAssignment> builder = ImmutableSet.builder();
     // Using creator.extractVariablesAndUFs we wouldn't get accurate information anymore as we
     // translate all bound vars back to their free counterparts in the visitor!
@@ -72,7 +75,8 @@ private ImmutableList<ValueAssignment> generateModel() {
   }
 
   // TODO this method is highly recursive and should be rewritten with a proper visitor
-  private void recursiveAssignmentFinder(ImmutableSet.Builder<ValueAssignment> builder, Expr expr) {
+  private void recursiveAssignmentFinder(ImmutableSet.Builder<ValueAssignment> builder, Expr expr)
+      throws SolverException, InterruptedException {
     if (expr.isConst() || expr.isNull()) {
       // We don't care about consts.
       return;
@@ -95,7 +99,8 @@ private void recursiveAssignmentFinder(ImmutableSet.Builder<ValueAssignment> bui
     }
   }
 
-  private ValueAssignment getAssignment(Expr pKeyTerm) {
+  private ValueAssignment getAssignment(Expr pKeyTerm)
+      throws SolverException, InterruptedException {
     List<Object> argumentInterpretation = new ArrayList<>();
     for (Expr param : pKeyTerm) {
       argumentInterpretation.add(evaluateImpl(param));
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..a6c41002ee 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() throws SolverException, InterruptedException {
     Preconditions.checkState(!closed);
     Preconditions.checkState(!changedSinceLastSatQuery);
     checkGenerateModels();
@@ -183,7 +183,8 @@ 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();
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..782a738f93 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() throws SolverException, InterruptedException {
     Preconditions.checkState(!closed);
     Preconditions.checkState(!changedSinceLastSatQuery);
     checkGenerateModels();
@@ -185,7 +185,8 @@ 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();
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..6c2b39d93e 100644
--- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Model.java
+++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Model.java
@@ -21,6 +21,7 @@
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.Formula;
 import org.sosy_lab.java_smt.api.FormulaManager;
+import org.sosy_lab.java_smt.api.SolverException;
 import org.sosy_lab.java_smt.basicimpl.AbstractModel;
 
 public class CVC5Model extends AbstractModel<Term, Sort, TermManager> {
@@ -37,7 +38,8 @@ public class CVC5Model extends AbstractModel<Term, Sort, TermManager> {
       CVC5AbstractProver<?> pProver,
       FormulaManager pMgr,
       CVC5FormulaCreator pCreator,
-      Collection<Term> pAssertedExpressions) {
+      Collection<Term> pAssertedExpressions)
+      throws SolverException, InterruptedException {
     super(pProver, pCreator);
     termManager = pCreator.getEnv();
     solver = pProver.solver;
@@ -56,7 +58,8 @@ public Term evalImpl(Term f) {
     return solver.getValue(f);
   }
 
-  private ImmutableList<ValueAssignment> generateModel() {
+  private ImmutableList<ValueAssignment> generateModel()
+      throws SolverException, InterruptedException {
     ImmutableSet.Builder<ValueAssignment> builder = ImmutableSet.builder();
     // Using creator.extractVariablesAndUFs we wouldn't get accurate information anymore as we
     // translate all bound vars back to their free counterparts in the visitor!
@@ -68,7 +71,8 @@ private ImmutableList<ValueAssignment> generateModel() {
   }
 
   // TODO this method is highly recursive and should be rewritten with a proper visitor
-  private void recursiveAssignmentFinder(ImmutableSet.Builder<ValueAssignment> builder, Term expr) {
+  private void recursiveAssignmentFinder(ImmutableSet.Builder<ValueAssignment> builder, Term expr)
+      throws SolverException, InterruptedException {
     try {
       Sort sort = expr.getSort();
       Kind kind = expr.getKind();
@@ -109,7 +113,8 @@ private void recursiveAssignmentFinder(ImmutableSet.Builder<ValueAssignment> bui
     }
   }
 
-  private ValueAssignment getAssignmentForUf(Term pKeyTerm) {
+  private ValueAssignment getAssignmentForUf(Term pKeyTerm)
+      throws SolverException, InterruptedException {
     // Ufs consist of arguments + 1 child, the first child is the function definition as a lambda
     // and the result, while the remaining children are the arguments. Note: we can't evaluate bound
     // variables!
@@ -169,7 +174,8 @@ private ValueAssignment getAssignmentForUf(Term pKeyTerm) {
         keyFormula, valueFormula, equation, nameStr, value, argumentInterpretationBuilder.build());
   }
 
-  private ValueAssignment getAssignment(Term pKeyTerm) {
+  private ValueAssignment getAssignment(Term pKeyTerm)
+      throws SolverException, InterruptedException {
     ImmutableList.Builder<Object> argumentInterpretationBuilder = ImmutableList.builder();
     for (int i = 0; i < pKeyTerm.getNumChildren(); i++) {
       try {
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 3b7266262c..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_with_sneaky_solver_exception;
+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_with_sneaky_solver_exception(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/opensmt/OpenSmtAbstractProver.java b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java
index 845cd0ae9f..49d5893e16 100644
--- a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java
+++ b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java
@@ -146,7 +146,8 @@ 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();
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..7e6bfbb30b 100644
--- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolModel.java
+++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolModel.java
@@ -22,6 +22,7 @@
 import java.util.LinkedHashSet;
 import java.util.List;
 import java.util.Set;
+import org.sosy_lab.java_smt.api.SolverException;
 import org.sosy_lab.java_smt.basicimpl.AbstractModel;
 import org.sosy_lab.java_smt.basicimpl.AbstractProver;
 import org.sosy_lab.java_smt.basicimpl.FormulaCreator;
@@ -44,7 +45,7 @@ class SmtInterpolModel extends AbstractModel<Term, Sort, Script> {
   }
 
   @Override
-  public ImmutableList<ValueAssignment> asList() {
+  public ImmutableList<ValueAssignment> asList() throws SolverException, InterruptedException {
 
     Set<FunctionSymbol> usedSymbols = new LinkedHashSet<>();
     for (Term assertedTerm : assertedTerms) {
@@ -95,7 +96,8 @@ private static String unescape(String s) {
    * @param upperIndices indices for multi-dimensional arrays
    */
   private Collection<ValueAssignment> getArrayAssignment(
-      String symbol, Term key, Term array, List<Object> upperIndices) {
+      String symbol, Term key, Term array, List<Object> upperIndices)
+      throws SolverException, InterruptedException {
     assert array.getSort().isArraySort();
     Collection<ValueAssignment> assignments = new ArrayList<>();
     Term evaluation = model.evaluate(array);
@@ -137,7 +139,8 @@ private Collection<ValueAssignment> getArrayAssignment(
   }
 
   /** Get all modeled assignments for the UF. */
-  private Collection<ValueAssignment> getUFAssignments(FunctionSymbol symbol) {
+  private Collection<ValueAssignment> getUFAssignments(FunctionSymbol symbol)
+      throws SolverException, InterruptedException {
     final Collection<ValueAssignment> assignments = new ArrayList<>();
     final String name = unescape(symbol.getApplicationString());
 
@@ -156,7 +159,8 @@ private Collection<ValueAssignment> getUFAssignments(FunctionSymbol symbol) {
     return assignments;
   }
 
-  private ValueAssignment getAssignment(String key, ApplicationTerm term) {
+  private ValueAssignment getAssignment(String key, ApplicationTerm term)
+      throws SolverException, InterruptedException {
     Term value = model.evaluate(term);
     List<Object> argumentInterpretation = new ArrayList<>();
     for (Term param : term.getParameters()) {
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);

From 0ca8d4f723b415fb00354a3ab368fa919f1b1929 Mon Sep 17 00:00:00 2001
From: BaierD <daniel.baier@sosy.ifi.lmu.de>
Date: Wed, 30 Jul 2025 16:08:35 +0200
Subject: [PATCH 07/19] Remove sneaky throws for Z3 specific code entirely

---
 .../java_smt/basicimpl/AbstractProver.java    |  5 ++--
 .../java_smt/solvers/z3/Z3AbstractProver.java |  4 ++--
 .../java_smt/solvers/z3/Z3FormulaCreator.java | 24 -------------------
 .../solvers/z3/Z3OptimizationProver.java      |  8 +++----
 .../java_smt/solvers/z3/Z3TheoremProver.java  |  4 ++--
 5 files changed, 11 insertions(+), 34 deletions(-)

diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java
index 07dbbbb5d6..9262143157 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> {
 
@@ -94,7 +95,7 @@ public final void push() throws InterruptedException {
     assertedFormulas.add(LinkedHashMultimap.create());
   }
 
-  protected abstract void pushImpl() throws InterruptedException;
+  protected abstract void pushImpl() throws InterruptedException, SolverException;
 
   @Override
   public final void pop() {
@@ -116,7 +117,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/solvers/z3/Z3AbstractProver.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java
index 10cdd2f6dc..1d8beabc62 100644
--- a/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java
+++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java
@@ -122,7 +122,7 @@ protected Z3Model getEvaluatorWithoutChecks() throws SolverException, Interrupte
   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/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 5b1f4720d7..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);
     }
   }
 

From cd51b02102ae5d0f2b24868caeb88385475bf128 Mon Sep 17 00:00:00 2001
From: BaierD <daniel.baier@sosy.ifi.lmu.de>
Date: Wed, 30 Jul 2025 16:33:24 +0200
Subject: [PATCH 08/19] Add Solver- and InterruptedException to push() and
 addConstraint() API

---
 .../java_smt/api/BasicProverEnvironment.java      |  6 +++---
 .../java_smt/basicimpl/AbstractProver.java        |  5 +++--
 .../BasicProverWithAssumptionsWrapper.java        |  4 ++--
 .../DebuggingBasicProverEnvironment.java          |  5 +++--
 .../logging/LoggingBasicProverEnvironment.java    |  7 ++++---
 .../StatisticsBasicProverEnvironment.java         |  5 +++--
 .../SynchronizedBasicProverEnvironment.java       |  5 +++--
 ...hronizedBasicProverEnvironmentWithContext.java |  5 +++--
 .../solvers/boolector/BoolectorNativeApiTest.java |  2 +-
 .../test/ProverEnvironmentSubjectTest.java        |  4 ++--
 .../java_smt/test/SolverConcurrencyTest.java      |  4 ++--
 .../sosy_lab/java_smt/test/SolverContextTest.java |  2 +-
 .../sosy_lab/java_smt/test/SolverStackTest0.java  | 10 +++++-----
 .../java_smt/test/SolverThreadLocalityTest.java   |  3 ++-
 src/org/sosy_lab/java_smt/test/TimeoutTest.java   | 15 ++++++++-------
 15 files changed, 45 insertions(+), 37 deletions(-)

diff --git a/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java b/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java
index 58f13f099d..a71a31eeca 100644
--- a/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java
+++ b/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java
@@ -35,7 +35,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);
   }
@@ -54,7 +54,7 @@ default T push(BooleanFormula f) throws InterruptedException {
    */
   @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
@@ -63,7 +63,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.
diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java
index 9262143157..e6d81c1f53 100644
--- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java
+++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java
@@ -89,7 +89,7 @@ public int size() {
   }
 
   @Override
-  public final void push() throws InterruptedException {
+  public final void push() throws InterruptedException, SolverException {
     checkState(!closed);
     pushImpl();
     assertedFormulas.add(LinkedHashMultimap.create());
@@ -109,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);
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 3afcbe0a41..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();
   }
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 33e2ef8756..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();
   }
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 78cb934251..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();
   }
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 1d5c7ece0f..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();
   }
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 fa79246d01..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();
     }
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 4fecf91550..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();
   }
 
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/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(
             () -> {

From 898832d35851d3d4539846f0a32da899f30d3e5c Mon Sep 17 00:00:00 2001
From: BaierD <daniel.baier@sosy.ifi.lmu.de>
Date: Wed, 30 Jul 2025 16:39:42 +0200
Subject: [PATCH 09/19] Remove warnings about sneaky throws where they can't
 happen anymore

---
 .../java_smt/api/BasicProverEnvironment.java  |  6 -----
 src/org/sosy_lab/java_smt/api/Evaluator.java  | 27 +++++--------------
 src/org/sosy_lab/java_smt/api/Model.java      |  3 ---
 3 files changed, 6 insertions(+), 30 deletions(-)

diff --git a/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java b/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java
index a71a31eeca..459bd0ac6e 100644
--- a/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java
+++ b/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java
@@ -29,9 +29,6 @@ public interface BasicProverEnvironment<T> extends AutoCloseable {
    * Push a backtracking point and add a formula to the current stack, asserting it. The return
    * value may be used to identify this formula later on in a query (this depends on the subtype of
    * the environment).
-   *
-   * <p>Warning: this might throw an unchecked {@link SolverException} as an extension of {@link
-   * Throwable}.
    */
   @Nullable
   @CanIgnoreReturnValue
@@ -48,9 +45,6 @@ default T push(BooleanFormula f) throws InterruptedException, SolverException {
 
   /**
    * Add a constraint to the latest backtracking point.
-   *
-   * <p>Warning: this might throw an unchecked {@link SolverException} as an extension of {@link
-   * Throwable}.
    */
   @Nullable
   @CanIgnoreReturnValue
diff --git a/src/org/sosy_lab/java_smt/api/Evaluator.java b/src/org/sosy_lab/java_smt/api/Evaluator.java
index 6ea3f2e31a..5bd94038d5 100644
--- a/src/org/sosy_lab/java_smt/api/Evaluator.java
+++ b/src/org/sosy_lab/java_smt/api/Evaluator.java
@@ -68,9 +68,6 @@ public interface Evaluator extends AutoCloseable {
    * Type-safe evaluation for integer formulas.
    *
    * <p>The formula does not need to be a variable, we also allow complex expression.
-   *
-   * <p>Warning: this might throw an unchecked {@link SolverException} as an extension of {@link
-   * Throwable}.
    */
   @Nullable BigInteger evaluate(IntegerFormula formula)
       throws SolverException, InterruptedException;
@@ -79,9 +76,7 @@ public interface Evaluator extends AutoCloseable {
    * Type-safe evaluation for rational formulas.
    *
    * <p>The formula does not need to be a variable, we also allow complex expression.
-   *
-   * <p>Warning: this might throw an unchecked {@link SolverException} as an extension of {@link
-   * Throwable}.
+
    */
   @Nullable Rational evaluate(RationalFormula formula) throws SolverException, InterruptedException;
 
@@ -89,9 +84,7 @@ public interface Evaluator extends AutoCloseable {
    * Type-safe evaluation for boolean formulas.
    *
    * <p>The formula does not need to be a variable, we also allow complex expression.
-   *
-   * <p>Warning: this might throw an unchecked {@link SolverException} as an extension of {@link
-   * Throwable}.
+
    */
   @Nullable Boolean evaluate(BooleanFormula formula) throws SolverException, InterruptedException;
 
@@ -99,9 +92,7 @@ public interface Evaluator extends AutoCloseable {
    * Type-safe evaluation for bitvector formulas.
    *
    * <p>The formula does not need to be a variable, we also allow complex expression.
-   *
-   * <p>Warning: this might throw an unchecked {@link SolverException} as an extension of {@link
-   * Throwable}.
+
    */
   @Nullable BigInteger evaluate(BitvectorFormula formula)
       throws SolverException, InterruptedException;
@@ -110,9 +101,7 @@ public interface Evaluator extends AutoCloseable {
    * Type-safe evaluation for string formulas.
    *
    * <p>The formula does not need to be a variable, we also allow complex expression.
-   *
-   * <p>Warning: this might throw an unchecked {@link SolverException} as an extension of {@link
-   * Throwable}.
+
    */
   @Nullable String evaluate(StringFormula formula) throws SolverException, InterruptedException;
 
@@ -120,9 +109,7 @@ public interface Evaluator extends AutoCloseable {
    * Type-safe evaluation for enumeration formulas.
    *
    * <p>The formula does not need to be a variable, we also allow complex expression.
-   *
-   * <p>Warning: this might throw an unchecked {@link SolverException} as an extension of {@link
-   * Throwable}.
+
    */
   @Nullable String evaluate(EnumerationFormula formula)
       throws SolverException, InterruptedException;
@@ -131,9 +118,7 @@ public interface Evaluator extends AutoCloseable {
    * Type-safe evaluation for floating-point formulas.
    *
    * <p>The formula does not need to be a variable, we also allow complex expression.
-   *
-   * <p>Warning: this might throw an unchecked {@link SolverException} as an extension of {@link
-   * Throwable}.
+
    */
   @Nullable FloatingPointNumber evaluate(FloatingPointFormula formula)
       throws SolverException, InterruptedException;
diff --git a/src/org/sosy_lab/java_smt/api/Model.java b/src/org/sosy_lab/java_smt/api/Model.java
index 8b4ac5fa3b..ad070de12c 100644
--- a/src/org/sosy_lab/java_smt/api/Model.java
+++ b/src/org/sosy_lab/java_smt/api/Model.java
@@ -69,9 +69,6 @@ private static <E extends Throwable> RuntimeException sneakyThrow(Throwable e) t
 
   /**
    * Build a list of assignments that stays valid after closing the model.
-   *
-   * <p>Warning: this might throw an unchecked {@link SolverException} as an extension of {@link
-   * Throwable}.
    */
   ImmutableList<ValueAssignment> asList() throws SolverException, InterruptedException;
 

From c9003997ea55e707f64bce084c8c113f16357202 Mon Sep 17 00:00:00 2001
From: BaierD <daniel.baier@sosy.ifi.lmu.de>
Date: Wed, 30 Jul 2025 16:40:19 +0200
Subject: [PATCH 10/19] Format: remove warnings about sneaky throws where they
 can't happen anymore

---
 src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java | 4 +---
 src/org/sosy_lab/java_smt/api/Evaluator.java              | 6 ------
 src/org/sosy_lab/java_smt/api/Model.java                  | 4 +---
 3 files changed, 2 insertions(+), 12 deletions(-)

diff --git a/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java b/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java
index 459bd0ac6e..d832794937 100644
--- a/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java
+++ b/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java
@@ -43,9 +43,7 @@ default T push(BooleanFormula f) throws InterruptedException, SolverException {
    */
   void pop();
 
-  /**
-   * Add a constraint to the latest backtracking point.
-   */
+  /** Add a constraint to the latest backtracking point. */
   @Nullable
   @CanIgnoreReturnValue
   T addConstraint(BooleanFormula constraint) throws InterruptedException, SolverException;
diff --git a/src/org/sosy_lab/java_smt/api/Evaluator.java b/src/org/sosy_lab/java_smt/api/Evaluator.java
index 5bd94038d5..7fa0199467 100644
--- a/src/org/sosy_lab/java_smt/api/Evaluator.java
+++ b/src/org/sosy_lab/java_smt/api/Evaluator.java
@@ -76,7 +76,6 @@ public interface Evaluator extends AutoCloseable {
    * 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) throws SolverException, InterruptedException;
 
@@ -84,7 +83,6 @@ public interface Evaluator extends AutoCloseable {
    * 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) throws SolverException, InterruptedException;
 
@@ -92,7 +90,6 @@ public interface Evaluator extends AutoCloseable {
    * 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)
       throws SolverException, InterruptedException;
@@ -101,7 +98,6 @@ public interface Evaluator extends AutoCloseable {
    * 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) throws SolverException, InterruptedException;
 
@@ -109,7 +105,6 @@ public interface Evaluator extends AutoCloseable {
    * 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)
       throws SolverException, InterruptedException;
@@ -118,7 +113,6 @@ public interface Evaluator extends AutoCloseable {
    * 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)
       throws SolverException, InterruptedException;
diff --git a/src/org/sosy_lab/java_smt/api/Model.java b/src/org/sosy_lab/java_smt/api/Model.java
index ad070de12c..cb9e4c1297 100644
--- a/src/org/sosy_lab/java_smt/api/Model.java
+++ b/src/org/sosy_lab/java_smt/api/Model.java
@@ -67,9 +67,7 @@ private static <E extends Throwable> RuntimeException sneakyThrow(Throwable e) t
     throw (E) e;
   }
 
-  /**
-   * Build a list of assignments that stays valid after closing the model.
-   */
+  /** Build a list of assignments that stays valid after closing the model. */
   ImmutableList<ValueAssignment> asList() throws SolverException, InterruptedException;
 
   /**

From 216641051a1bbd1ade305edbb95d2a1d308399c8 Mon Sep 17 00:00:00 2001
From: BaierD <daniel.baier@sosy.ifi.lmu.de>
Date: Wed, 30 Jul 2025 17:13:32 +0200
Subject: [PATCH 11/19] Rename exception variable to fit naming schema

---
 src/org/sosy_lab/java_smt/api/Model.java | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/org/sosy_lab/java_smt/api/Model.java b/src/org/sosy_lab/java_smt/api/Model.java
index cb9e4c1297..68e8c792c3 100644
--- a/src/org/sosy_lab/java_smt/api/Model.java
+++ b/src/org/sosy_lab/java_smt/api/Model.java
@@ -57,8 +57,8 @@ public interface Model extends Evaluator, Iterable<ValueAssignment>, AutoCloseab
   default Iterator<ValueAssignment> iterator() {
     try {
       return asList().iterator();
-    } catch (SolverException | InterruptedException pE) {
-      throw sneakyThrow(pE);
+    } catch (SolverException | InterruptedException ex) {
+      throw sneakyThrow(ex);
     }
   }
 

From 64b21b3b8b766b07e54ebd0bd525e797057b0688 Mon Sep 17 00:00:00 2001
From: BaierD <daniel.baier@sosy.ifi.lmu.de>
Date: Wed, 30 Jul 2025 17:18:48 +0200
Subject: [PATCH 12/19] Improve warning for sneaky throws in model iterator()
 as suggested by Philipp

---
 src/org/sosy_lab/java_smt/api/Model.java | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/org/sosy_lab/java_smt/api/Model.java b/src/org/sosy_lab/java_smt/api/Model.java
index 68e8c792c3..816fbdad7a 100644
--- a/src/org/sosy_lab/java_smt/api/Model.java
+++ b/src/org/sosy_lab/java_smt/api/Model.java
@@ -50,8 +50,9 @@ public interface Model extends Evaluator, Iterable<ValueAssignment>, AutoCloseab
    *       Please use a direct evaluation query to get the evaluation in such a case.
    * </ul>
    *
-   * <p>Warning: this might throw {@link SolverException} or {@link InterruptedException} as {@link
-   * RuntimeException} as checked exceptions are not supported by this method.
+   * <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() {

From 0769c11efefd0588c4a95d2b1a96770e30ab0d00 Mon Sep 17 00:00:00 2001
From: BaierD <daniel.baier@sosy.ifi.lmu.de>
Date: Fri, 8 Aug 2025 10:44:15 +0200
Subject: [PATCH 13/19] Allow AbstractEvaluator.evaluateImpl to be overridden
 so that it can be used without exceptions and implement for Bitwuzla

---
 .../java_smt/basicimpl/AbstractEvaluator.java   |  2 +-
 .../solvers/bitwuzla/BitwuzlaModel.java         | 17 +++++++++++------
 2 files changed, 12 insertions(+), 7 deletions(-)

diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractEvaluator.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractEvaluator.java
index 53432744a1..fde81062e1 100644
--- a/src/org/sosy_lab/java_smt/basicimpl/AbstractEvaluator.java
+++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractEvaluator.java
@@ -126,7 +126,7 @@ protected abstract TFormulaInfo evalImpl(TFormulaInfo formula)
    * 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) throws SolverException, InterruptedException {
+  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/solvers/bitwuzla/BitwuzlaModel.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaModel.java
index 7c031e0833..6b4da40af7 100644
--- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaModel.java
+++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaModel.java
@@ -19,7 +19,6 @@
 import java.util.List;
 import java.util.Set;
 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.solvers.bitwuzla.api.Bitwuzla;
 import org.sosy_lab.java_smt.solvers.bitwuzla.api.Kind;
@@ -51,7 +50,7 @@ protected BitwuzlaModel(
 
   /** Build a list of assignments that stays valid after closing the model. */
   @Override
-  public ImmutableList<ValueAssignment> asList() throws SolverException, InterruptedException {
+  public ImmutableList<ValueAssignment> asList() {
     Preconditions.checkState(!isClosed());
     Preconditions.checkState(!prover.isClosed(), "Cannot use model after prover is closed");
     ImmutableSet.Builder<ValueAssignment> variablesBuilder = ImmutableSet.builder();
@@ -109,15 +108,13 @@ private ValueAssignment getSimpleAssignment(Term pTerm) {
         argumentInterpretation);
   }
 
-  private Collection<ValueAssignment> getArrayAssignment(Term pTerm)
-      throws SolverException, InterruptedException {
+  private Collection<ValueAssignment> getArrayAssignment(Term pTerm) {
     return getArrayAssignments(pTerm, ImmutableList.of());
   }
 
   // TODO: check this in detail. I think this might be incomplete.
   // We should add more Model tests in general. As most are parsing and int based!
-  private Collection<ValueAssignment> getArrayAssignments(Term pTerm, List<Object> upperIndices)
-      throws SolverException, InterruptedException {
+  private Collection<ValueAssignment> getArrayAssignments(Term pTerm, List<Object> upperIndices) {
     // Array children for store are structured in the following way:
     // {starting array, index, value} in "we add value at index to array"
     // Selections are structured: {starting array, index}
@@ -238,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);
+  }
 }

From aa370f6bdbf8a5fbda16ba0ae9b312682fffc66d Mon Sep 17 00:00:00 2001
From: BaierD <daniel.baier@sosy.ifi.lmu.de>
Date: Fri, 8 Aug 2025 10:54:45 +0200
Subject: [PATCH 14/19] Remove exceptions in the model of SMTInterpol where not
 necessary

---
 .../solvers/smtinterpol/SmtInterpolModel.java | 21 ++++++++++++-------
 1 file changed, 13 insertions(+), 8 deletions(-)

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 7e6bfbb30b..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;
@@ -22,7 +23,6 @@
 import java.util.LinkedHashSet;
 import java.util.List;
 import java.util.Set;
-import org.sosy_lab.java_smt.api.SolverException;
 import org.sosy_lab.java_smt.basicimpl.AbstractModel;
 import org.sosy_lab.java_smt.basicimpl.AbstractProver;
 import org.sosy_lab.java_smt.basicimpl.FormulaCreator;
@@ -45,7 +45,7 @@ class SmtInterpolModel extends AbstractModel<Term, Sort, Script> {
   }
 
   @Override
-  public ImmutableList<ValueAssignment> asList() throws SolverException, InterruptedException {
+  public ImmutableList<ValueAssignment> asList() {
 
     Set<FunctionSymbol> usedSymbols = new LinkedHashSet<>();
     for (Term assertedTerm : assertedTerms) {
@@ -96,8 +96,7 @@ private static String unescape(String s) {
    * @param upperIndices indices for multi-dimensional arrays
    */
   private Collection<ValueAssignment> getArrayAssignment(
-      String symbol, Term key, Term array, List<Object> upperIndices)
-      throws SolverException, InterruptedException {
+      String symbol, Term key, Term array, List<Object> upperIndices) {
     assert array.getSort().isArraySort();
     Collection<ValueAssignment> assignments = new ArrayList<>();
     Term evaluation = model.evaluate(array);
@@ -139,8 +138,7 @@ private Collection<ValueAssignment> getArrayAssignment(
   }
 
   /** Get all modeled assignments for the UF. */
-  private Collection<ValueAssignment> getUFAssignments(FunctionSymbol symbol)
-      throws SolverException, InterruptedException {
+  private Collection<ValueAssignment> getUFAssignments(FunctionSymbol symbol) {
     final Collection<ValueAssignment> assignments = new ArrayList<>();
     final String name = unescape(symbol.getApplicationString());
 
@@ -159,8 +157,7 @@ private Collection<ValueAssignment> getUFAssignments(FunctionSymbol symbol)
     return assignments;
   }
 
-  private ValueAssignment getAssignment(String key, ApplicationTerm term)
-      throws SolverException, InterruptedException {
+  private ValueAssignment getAssignment(String key, ApplicationTerm term) {
     Term value = model.evaluate(term);
     List<Object> argumentInterpretation = new ArrayList<>();
     for (Term param : term.getParameters()) {
@@ -188,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);
+  }
 }

From 582e19dd7cbfa14066652afa493e38f37915f21b Mon Sep 17 00:00:00 2001
From: BaierD <daniel.baier@sosy.ifi.lmu.de>
Date: Fri, 8 Aug 2025 10:59:38 +0200
Subject: [PATCH 15/19] Remove exceptions in OpenSMT2s getModelAssignments() by
 catching them, but since they can not be thrown this is not a problem

---
 .../java_smt/solvers/opensmt/OpenSmtAbstractProver.java    | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

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 49d5893e16..863266d45a 100644
--- a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java
+++ b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java
@@ -150,7 +150,12 @@ 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);
+    }
   }
 
   /**

From 0e97ab8e597706147cd7a43b4602b9dc1e9c1a73 Mon Sep 17 00:00:00 2001
From: BaierD <daniel.baier@sosy.ifi.lmu.de>
Date: Fri, 8 Aug 2025 11:16:55 +0200
Subject: [PATCH 16/19] Remove exceptions in CVC4s getModelAssignments() by
 catching them, but since they can not be thrown this is not a problem

---
 .../java_smt/solvers/cvc4/CVC4TheoremProver.java         | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

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 a6c41002ee..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, InterruptedException {
+  public CVC4Model getModel() {
     Preconditions.checkState(!closed);
     Preconditions.checkState(!changedSinceLastSatQuery);
     checkGenerateModels();
@@ -187,7 +187,12 @@ 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

From b2fb7427fb5d38798d48b021d4f8bb2636ee7a5c Mon Sep 17 00:00:00 2001
From: BaierD <daniel.baier@sosy.ifi.lmu.de>
Date: Fri, 8 Aug 2025 11:17:00 +0200
Subject: [PATCH 17/19] Remove exceptions in CVC5s getModelAssignments() by
 catching them, but since they can not be thrown this is not a problem

---
 .../java_smt/solvers/cvc5/CVC5AbstractProver.java    | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

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 782a738f93..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, InterruptedException {
+  public CVC5Model getModel() {
     Preconditions.checkState(!closed);
     Preconditions.checkState(!changedSinceLastSatQuery);
     checkGenerateModels();
@@ -185,11 +185,15 @@ protected void setChanged() {
   }
 
   @Override
-  public ImmutableList<ValueAssignment> getModelAssignments()
-      throws SolverException, InterruptedException {
+  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

From 5afc4ae342db286350b7a738f80c325f679e18a5 Mon Sep 17 00:00:00 2001
From: BaierD <daniel.baier@sosy.ifi.lmu.de>
Date: Fri, 8 Aug 2025 11:17:26 +0200
Subject: [PATCH 18/19] Remove exceptions in CVC5s model methods as they are
 never thrown

---
 .../java_smt/solvers/cvc5/CVC5Model.java      | 24 ++++++++++---------
 1 file changed, 13 insertions(+), 11 deletions(-)

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 6c2b39d93e..effe237494 100644
--- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Model.java
+++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Model.java
@@ -21,7 +21,6 @@
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.Formula;
 import org.sosy_lab.java_smt.api.FormulaManager;
-import org.sosy_lab.java_smt.api.SolverException;
 import org.sosy_lab.java_smt.basicimpl.AbstractModel;
 
 public class CVC5Model extends AbstractModel<Term, Sort, TermManager> {
@@ -38,8 +37,7 @@ public class CVC5Model extends AbstractModel<Term, Sort, TermManager> {
       CVC5AbstractProver<?> pProver,
       FormulaManager pMgr,
       CVC5FormulaCreator pCreator,
-      Collection<Term> pAssertedExpressions)
-      throws SolverException, InterruptedException {
+      Collection<Term> pAssertedExpressions) {
     super(pProver, pCreator);
     termManager = pCreator.getEnv();
     solver = pProver.solver;
@@ -58,8 +56,7 @@ public Term evalImpl(Term f) {
     return solver.getValue(f);
   }
 
-  private ImmutableList<ValueAssignment> generateModel()
-      throws SolverException, InterruptedException {
+  private ImmutableList<ValueAssignment> generateModel() {
     ImmutableSet.Builder<ValueAssignment> builder = ImmutableSet.builder();
     // Using creator.extractVariablesAndUFs we wouldn't get accurate information anymore as we
     // translate all bound vars back to their free counterparts in the visitor!
@@ -71,8 +68,7 @@ private ImmutableList<ValueAssignment> generateModel()
   }
 
   // TODO this method is highly recursive and should be rewritten with a proper visitor
-  private void recursiveAssignmentFinder(ImmutableSet.Builder<ValueAssignment> builder, Term expr)
-      throws SolverException, InterruptedException {
+  private void recursiveAssignmentFinder(ImmutableSet.Builder<ValueAssignment> builder, Term expr) {
     try {
       Sort sort = expr.getSort();
       Kind kind = expr.getKind();
@@ -113,8 +109,7 @@ private void recursiveAssignmentFinder(ImmutableSet.Builder<ValueAssignment> bui
     }
   }
 
-  private ValueAssignment getAssignmentForUf(Term pKeyTerm)
-      throws SolverException, InterruptedException {
+  private ValueAssignment getAssignmentForUf(Term pKeyTerm) {
     // Ufs consist of arguments + 1 child, the first child is the function definition as a lambda
     // and the result, while the remaining children are the arguments. Note: we can't evaluate bound
     // variables!
@@ -174,8 +169,7 @@ private ValueAssignment getAssignmentForUf(Term pKeyTerm)
         keyFormula, valueFormula, equation, nameStr, value, argumentInterpretationBuilder.build());
   }
 
-  private ValueAssignment getAssignment(Term pKeyTerm)
-      throws SolverException, InterruptedException {
+  private ValueAssignment getAssignment(Term pKeyTerm) {
     ImmutableList.Builder<Object> argumentInterpretationBuilder = ImmutableList.builder();
     for (int i = 0; i < pKeyTerm.getNumChildren(); i++) {
       try {
@@ -212,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);
+  }
 }

From ed7a40a306ff2d89f32154bea6157536b8631ad9 Mon Sep 17 00:00:00 2001
From: BaierD <daniel.baier@sosy.ifi.lmu.de>
Date: Fri, 8 Aug 2025 11:17:30 +0200
Subject: [PATCH 19/19] Remove exceptions in CVC4s model methods as they are
 never thrown

---
 .../java_smt/solvers/cvc4/CVC4Model.java      | 21 +++++++++++--------
 1 file changed, 12 insertions(+), 9 deletions(-)

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 ca99cc5c72..d9b6027826 100644
--- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4Model.java
+++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4Model.java
@@ -21,7 +21,6 @@
 import java.util.List;
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.Formula;
-import org.sosy_lab.java_smt.api.SolverException;
 import org.sosy_lab.java_smt.basicimpl.AbstractModel;
 
 public class CVC4Model extends AbstractModel<Expr, Type, ExprManager> {
@@ -35,8 +34,7 @@ public class CVC4Model extends AbstractModel<Expr, Type, ExprManager> {
       CVC4TheoremProver pProver,
       CVC4FormulaCreator pCreator,
       SmtEngine pSmtEngine,
-      Collection<Expr> pAssertedExpressions)
-      throws SolverException, InterruptedException {
+      Collection<Expr> pAssertedExpressions) {
     super(pProver, pCreator);
     smtEngine = pSmtEngine;
     prover = pProver;
@@ -62,8 +60,7 @@ private Expr getValue(Expr f) {
     return prover.exportExpr(smtEngine.getValue(prover.importExpr(f)));
   }
 
-  private ImmutableList<ValueAssignment> generateModel()
-      throws SolverException, InterruptedException {
+  private ImmutableList<ValueAssignment> generateModel() {
     ImmutableSet.Builder<ValueAssignment> builder = ImmutableSet.builder();
     // Using creator.extractVariablesAndUFs we wouldn't get accurate information anymore as we
     // translate all bound vars back to their free counterparts in the visitor!
@@ -75,8 +72,7 @@ private ImmutableList<ValueAssignment> generateModel()
   }
 
   // TODO this method is highly recursive and should be rewritten with a proper visitor
-  private void recursiveAssignmentFinder(ImmutableSet.Builder<ValueAssignment> builder, Expr expr)
-      throws SolverException, InterruptedException {
+  private void recursiveAssignmentFinder(ImmutableSet.Builder<ValueAssignment> builder, Expr expr) {
     if (expr.isConst() || expr.isNull()) {
       // We don't care about consts.
       return;
@@ -99,8 +95,7 @@ private void recursiveAssignmentFinder(ImmutableSet.Builder<ValueAssignment> bui
     }
   }
 
-  private ValueAssignment getAssignment(Expr pKeyTerm)
-      throws SolverException, InterruptedException {
+  private ValueAssignment getAssignment(Expr pKeyTerm) {
     List<Object> argumentInterpretation = new ArrayList<>();
     for (Expr param : pKeyTerm) {
       argumentInterpretation.add(evaluateImpl(param));
@@ -124,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);
+  }
 }