diff --git a/src/org/sosy_lab/java_smt/api/Model.java b/src/org/sosy_lab/java_smt/api/Model.java
index a50c2530bd..31c130fa40 100644
--- a/src/org/sosy_lab/java_smt/api/Model.java
+++ b/src/org/sosy_lab/java_smt/api/Model.java
@@ -11,10 +11,8 @@
 import com.google.common.base.Joiner;
 import com.google.common.base.Preconditions;
 import com.google.common.collect.ImmutableList;
-import java.util.Iterator;
 import java.util.List;
 import java.util.Objects;
-import org.sosy_lab.java_smt.api.Model.ValueAssignment;
 
 /**
  * This class provides a model with concrete evaluations for symbols and formulas from the
@@ -30,14 +28,13 @@
  *       environment.
  * </ul>
  */
-public interface Model extends Evaluator, Iterable<ValueAssignment>, AutoCloseable {
+public interface Model extends Evaluator, AutoCloseable {
 
   /**
-   * Iterate over all values present in the model. Note that iterating multiple times may be
-   * inefficient for some solvers, it is recommended to use {@link
-   * BasicProverEnvironment#getModelAssignments()} instead in this case.
+   * Build a list of assignments for all values present in the model. The list stays valid after
+   * closing the model.
    *
-   * <p>The iteration includes value assignments for...
+   * <p>The list includes value assignments for...
    *
    * <ul>
    *   <li>all relevant free variables of simple type. If a variable is irrelevant for
@@ -50,16 +47,6 @@ public interface Model extends Evaluator, Iterable<ValueAssignment>, AutoCloseab
    *       Please use a direct evaluation query to get the evaluation in such a case.
    * </ul>
    */
-  @Override
-  default Iterator<ValueAssignment> iterator() {
-    try {
-      return asList().iterator();
-    } catch (InterruptedException | SolverException e) {
-      throw new RuntimeException(e);
-    }
-  }
-
-  /** Build a list of assignments that stays valid after closing the model. */
   ImmutableList<ValueAssignment> asList() throws InterruptedException, SolverException;
 
   /**
@@ -77,7 +64,7 @@ default Iterator<ValueAssignment> iterator() {
 
   /**
    * Free resources associated with this model (existing {@link ValueAssignment} instances stay
-   * valid, but {@link #evaluate(Formula)} etc. and {@link #iterator()} must not be called again).
+   * valid, but {@link #evaluate(Formula)} etc. must not be called again).
    */
   @Override
   void close();
diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractModel.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractModel.java
index 1f6472808a..1096d1e768 100644
--- a/src/org/sosy_lab/java_smt/basicimpl/AbstractModel.java
+++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractModel.java
@@ -10,6 +10,7 @@
 
 import com.google.common.base.Joiner;
 import org.sosy_lab.java_smt.api.Model;
+import org.sosy_lab.java_smt.api.SolverException;
 
 @SuppressWarnings("ClassTypeParameterName")
 public abstract class AbstractModel<TFormulaInfo, TType, TEnv>
@@ -20,8 +21,21 @@ protected AbstractModel(
     super(prover, creator);
   }
 
+  @SuppressWarnings("unchecked")
+  private static <E extends Throwable> void sneakyThrow(Throwable e) throws E {
+    throw (E) e;
+  }
+
   @Override
   public String toString() {
-    return Joiner.on('\n').join(iterator());
+    try {
+      return Joiner.on('\n').join(asList());
+    } catch (InterruptedException ex) {
+      Thread.currentThread().interrupt();
+      sneakyThrow(ex);
+    } catch (SolverException ex) {
+      sneakyThrow(ex);
+    }
+    throw new AssertionError("unreachable code");
   }
 }
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 d0fde93964..fbe5c659e9 100644
--- a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java
+++ b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java
@@ -217,7 +217,7 @@ protected String getReasonFromSolverFeatures(
       return "Unknown reason.";
     } else {
       return String.format(
-          "Assertions use features %s that are not supported " + "by the specified logic %s.",
+          "Assertions use features %s that are not supported by the specified logic %s.",
           errors, creator.getLogic());
     }
   }
diff --git a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtModel.java b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtModel.java
index b49e05c92c..47f3afc36f 100644
--- a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtModel.java
+++ b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtModel.java
@@ -8,12 +8,14 @@
 
 package org.sosy_lab.java_smt.solvers.opensmt;
 
+import static org.sosy_lab.common.collect.Collections3.elementAndList;
+
 import com.google.common.base.Preconditions;
 import com.google.common.collect.ImmutableList;
 import com.google.common.collect.Lists;
 import java.util.ArrayList;
 import java.util.Collection;
-import java.util.HashMap;
+import java.util.LinkedHashMap;
 import java.util.List;
 import java.util.Map;
 import org.sosy_lab.java_smt.basicimpl.AbstractModel;
@@ -42,7 +44,15 @@ public class OpenSmtModel extends AbstractModel<PTRef, SRef, Logic> {
     osmtLogic = pCreator.getEnv();
     osmtModel = pProver.getOsmtSolver().getModel();
 
-    Map<String, PTRef> userDeclarations = new HashMap<>();
+    // We need to generate and save this at construction time as OpenSMT has no functionality to
+    // give a persistent reference to the model. If the SMT engine is used somewhere else, the
+    // values we get out of it might change!
+    model = generateModel(pCreator, pAssertedTerms);
+  }
+
+  private ImmutableList<ValueAssignment> generateModel(
+      OpenSmtFormulaCreator pCreator, Collection<PTRef> pAssertedTerms) {
+    Map<String, PTRef> userDeclarations = new LinkedHashMap<>();
     for (PTRef asserted : pAssertedTerms) {
       userDeclarations.putAll(creator.extractVariablesAndUFs(asserted, true));
     }
@@ -66,36 +76,30 @@ public class OpenSmtModel extends AbstractModel<PTRef, SRef, Logic> {
       if (numArgs == 0) {
         PTRef key = osmtLogic.mkVar(sort, osmtLogic.getSymName(ref));
         PTRef value = osmtModel.evaluate(key);
-
-        builder.add(
-            new ValueAssignment(
-                pCreator.encapsulate(key),
-                pCreator.encapsulate(value),
-                pCreator.encapsulateBoolean(osmtLogic.mkEq(key, value)),
-                osmtLogic.getSymName(ref),
-                pCreator.convertValue(value),
-                new ArrayList<>()));
+        builder.add(getValueAssignment(pCreator, key, value, ref, ImmutableList.of()));
       } else {
         TemplateFunction tf = osmtModel.getDefinition(ref);
 
         for (List<PTRef> path : unfold(numArgs, tf.getBody())) {
           List<PTRef> args = path.subList(0, numArgs);
-
           PTRef key = osmtLogic.insertTerm(ref, new VectorPTRef(args));
           PTRef value = path.get(numArgs);
-
-          builder.add(
-              new ValueAssignment(
-                  pCreator.encapsulate(key),
-                  pCreator.encapsulate(value),
-                  pCreator.encapsulateBoolean(osmtLogic.mkEq(key, value)),
-                  osmtLogic.getSymName(ref),
-                  pCreator.convertValue(value),
-                  Lists.transform(args, pCreator::convertValue)));
+          builder.add(getValueAssignment(pCreator, key, value, ref, args));
         }
       }
     }
-    model = builder.build();
+    return builder.build();
+  }
+
+  private ValueAssignment getValueAssignment(
+      OpenSmtFormulaCreator pCreator, PTRef key, PTRef value, SymRef ref, List<PTRef> args) {
+    return new ValueAssignment(
+        pCreator.encapsulate(key),
+        pCreator.encapsulate(value),
+        pCreator.encapsulateBoolean(osmtLogic.mkEq(key, value)),
+        osmtLogic.getSymName(ref),
+        pCreator.convertValue(value),
+        Lists.transform(args, pCreator::convertValue));
   }
 
   @Override
@@ -103,7 +107,7 @@ public PTRef evalImpl(PTRef f) {
     Preconditions.checkState(!isClosed());
     Map<String, PTRef> userDeclarations = creator.extractVariablesAndUFs(f, true);
 
-    // FIXME: rewrite to use checkCompatability from AbstractProver
+    // FIXME: rewrite to use checkCompatibility from AbstractProver
 
     for (PTRef term : userDeclarations.values()) {
       SRef sort = osmtLogic.getSortRef(term);
@@ -143,20 +147,14 @@ private List<List<PTRef>> unfold(int numArgs, PTRef body) {
       PTRef value = osmtLogic.isVar(sub00) ? sub01 : sub00;
 
       for (List<PTRef> nested : unfold(numArgs - 1, sub1)) {
-        List<PTRef> prefixed = new ArrayList<>();
-        prefixed.add(value);
-        prefixed.addAll(nested);
-
+        List<PTRef> prefixed = elementAndList(value, nested);
         unwrapped.add(prefixed);
       }
       unwrapped.addAll(unfold(numArgs, sub2));
     }
 
     if (numArgs == 0) {
-      List<PTRef> value = new ArrayList<>();
-      value.add(body);
-
-      unwrapped.add(value);
+      unwrapped.add(ImmutableList.of(body));
     }
     return unwrapped;
   }
diff --git a/src/org/sosy_lab/java_smt/test/BooleanFormulaSubject.java b/src/org/sosy_lab/java_smt/test/BooleanFormulaSubject.java
index b4caa38b3b..9568b137e7 100644
--- a/src/org/sosy_lab/java_smt/test/BooleanFormulaSubject.java
+++ b/src/org/sosy_lab/java_smt/test/BooleanFormulaSubject.java
@@ -146,7 +146,7 @@ void isSatisfiableAndHasModel(int maxSizeOfModel) throws SolverException, Interr
         // check whether the model exists and we can iterate over it.
         // We allow an empty model, but it must be available.
         try (Model m = prover.getModel()) {
-          for (ValueAssignment v : m) {
+          for (ValueAssignment v : m.asList()) {
             // ignore, we just check iteration
           }
         }
diff --git a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java
index ee82fb5fcd..7731458b27 100644
--- a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java
+++ b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java
@@ -954,7 +954,7 @@ public void fpModelContent() throws SolverException, InterruptedException {
         ValueAssignment nanAssignment =
             new ValueAssignment(nanVar, nan, nanEq, "nan", nanValue, ImmutableList.of());
 
-        assertThat(model).containsExactly(zeroAssignment, oneAssignment, nanAssignment);
+        assertThat(model.asList()).containsExactly(zeroAssignment, oneAssignment, nanAssignment);
       }
     }
   }
@@ -967,7 +967,7 @@ public void fpModelValue() throws SolverException, InterruptedException {
       assertThat(prover).isSatisfiable();
 
       try (Model model = prover.getModel()) {
-        assertThat(model).isEmpty();
+        assertThat(model.asList()).isEmpty();
 
         for (float f :
             new float[] {
diff --git a/src/org/sosy_lab/java_smt/test/ModelTest.java b/src/org/sosy_lab/java_smt/test/ModelTest.java
index 34db34585b..e4b1eec5cc 100644
--- a/src/org/sosy_lab/java_smt/test/ModelTest.java
+++ b/src/org/sosy_lab/java_smt/test/ModelTest.java
@@ -94,7 +94,7 @@ public void testEmpty() throws SolverException, InterruptedException {
       assertThat(prover).isSatisfiable();
 
       try (Model m = prover.getModel()) {
-        assertThat(m).isEmpty();
+        assertThat(m.asList()).isEmpty();
       }
 
       assertThat(prover.getModelAssignments()).isEmpty();
@@ -108,7 +108,7 @@ public void testOnlyTrue() throws SolverException, InterruptedException {
       assertThat(prover).isSatisfiable();
 
       try (Model m = prover.getModel()) {
-        assertThat(m).isEmpty();
+        assertThat(m.asList()).isEmpty();
       }
 
       assertThat(prover.getModelAssignments()).isEmpty();
@@ -412,7 +412,7 @@ public void testGetMultipleUFsWithInts() throws Exception {
       try (Model m = prover.getModel()) {
         assertThat(m.evaluate(app1)).isEqualTo(BigInteger.ONE);
         assertThat(m.evaluate(app2)).isEqualTo(BigInteger.valueOf(2));
-        assertThat(m).containsExactlyElementsIn(expectedModel);
+        assertThat(m.asList()).containsExactlyElementsIn(expectedModel);
       }
       assertThat(prover.getModelAssignments()).containsExactlyElementsIn(expectedModel);
     }
@@ -477,7 +477,7 @@ public void testGetMultipleUFsWithBvs() throws Exception {
       try (Model m = prover.getModel()) {
         assertThat(m.evaluate(app1)).isEqualTo(BigInteger.ONE);
         assertThat(m.evaluate(app2)).isEqualTo(BigInteger.valueOf(2));
-        assertThat(m).containsExactlyElementsIn(expectedModel);
+        assertThat(m.asList()).containsExactlyElementsIn(expectedModel);
       }
       assertThat(prover.getModelAssignments()).containsExactlyElementsIn(expectedModel);
     }
@@ -565,7 +565,7 @@ public void testGetMultipleUFsWithBvsWithMultipleArguments() throws Exception {
       try (Model m = prover.getModel()) {
         assertThat(m.evaluate(app1)).isEqualTo(BigInteger.ONE);
         assertThat(m.evaluate(app2)).isEqualTo(BigInteger.valueOf(2));
-        assertThat(m).containsExactlyElementsIn(expectedModel);
+        assertThat(m.asList()).containsExactlyElementsIn(expectedModel);
       }
       assertThat(prover.getModelAssignments()).containsExactlyElementsIn(expectedModel);
     }
@@ -618,10 +618,10 @@ public void testQuantifiedUF() throws SolverException, InterruptedException {
       assertThat(prover).isSatisfiable();
 
       try (Model m = prover.getModel()) {
-        for (@SuppressWarnings("unused") ValueAssignment assignment : m) {
+        for (@SuppressWarnings("unused") ValueAssignment assignment : m.asList()) {
           // Check that we can iterate through with no crashes.
         }
-        assertThat(m).contains(expectedValueAssignment);
+        assertThat(m.asList()).contains(expectedValueAssignment);
       }
     }
   }
@@ -673,10 +673,10 @@ public void testQuantifiedUF2() throws SolverException, InterruptedException {
       assertThat(prover).isSatisfiable();
 
       try (Model m = prover.getModel()) {
-        for (@SuppressWarnings("unused") ValueAssignment assignment : m) {
+        for (@SuppressWarnings("unused") ValueAssignment assignment : m.asList()) {
           // Check that we can iterate through with no crashes.
         }
-        assertThat(m).contains(expectedValueAssignment);
+        assertThat(m.asList()).contains(expectedValueAssignment);
       }
     }
   }
@@ -807,7 +807,7 @@ public void testPartialModels() throws SolverException, InterruptedException {
       assertThat(prover).isSatisfiable();
       try (Model m = prover.getModel()) {
         assertThat(m.evaluate(x)).isEqualTo(null);
-        assertThat(m).isEmpty();
+        assertThat(m.asList()).isEmpty();
       }
     }
   }
@@ -974,7 +974,7 @@ public void testNonVariableValues() throws SolverException, InterruptedException
       assertThat(prover).isSatisfiable();
 
       try (Model m = prover.getModel()) {
-        for (@SuppressWarnings("unused") ValueAssignment assignment : m) {
+        for (@SuppressWarnings("unused") ValueAssignment assignment : m.asList()) {
           // Check that we can iterate through with no crashes.
         }
         assertThat(m.evaluate(select1Store7in1)).isEqualTo(BigInteger.valueOf(7));
@@ -1029,7 +1029,7 @@ public void testNonVariableValues2() throws SolverException, InterruptedExceptio
       assertThat(prover).isSatisfiable();
 
       try (Model m = prover.getModel()) {
-        for (@SuppressWarnings("unused") ValueAssignment assignment : m) {
+        for (@SuppressWarnings("unused") ValueAssignment assignment : m.asList()) {
           // Check that we can iterate through with no crashes.
         }
         assertThat(m.evaluate(select1Store7in1)).isEqualTo(BigInteger.valueOf(7));
@@ -1058,7 +1058,7 @@ public void testGetIntArrays() throws SolverException, InterruptedException {
       assertThat(prover).isSatisfiable();
 
       try (Model m = prover.getModel()) {
-        for (@SuppressWarnings("unused") ValueAssignment assignment : m) {
+        for (@SuppressWarnings("unused") ValueAssignment assignment : m.asList()) {
           // Check that we can iterate through with no crashes.
         }
         assertThat(m.evaluate(selected)).isEqualTo(BigInteger.ONE);
@@ -1100,7 +1100,7 @@ public void testGetArrays2() throws SolverException, InterruptedException {
       assertThat(prover).isSatisfiable();
 
       try (Model m = prover.getModel()) {
-        for (@SuppressWarnings("unused") ValueAssignment assignment : m) {
+        for (@SuppressWarnings("unused") ValueAssignment assignment : m.asList()) {
           // Check that we can iterate through with no crashes.
         }
         assertThat(m.evaluate(amgr.select(updated, bvmgr.makeBitvector(8, 1))))
@@ -1498,7 +1498,7 @@ public void testGetArrays7() throws SolverException, InterruptedException {
       assertThat(prover).isSatisfiable();
 
       try (Model m = prover.getModel()) {
-        for (@SuppressWarnings("unused") ValueAssignment assignment : m) {
+        for (@SuppressWarnings("unused") ValueAssignment assignment : m.asList()) {
           // Check that we can iterate through with no crashes.
         }
         assertThat(m.evaluate(selected)).isEqualTo(BigInteger.ZERO);
@@ -1543,7 +1543,7 @@ public void testGetArrays8() throws SolverException, InterruptedException {
       assertThat(prover).isSatisfiable();
 
       try (Model m = prover.getModel()) {
-        for (@SuppressWarnings("unused") ValueAssignment assignment : m) {
+        for (@SuppressWarnings("unused") ValueAssignment assignment : m.asList()) {
           // Check that we can iterate through with no crashes.
         }
         assertThat(m.evaluate(selectStore)).isEqualTo(BigInteger.valueOf(7));
@@ -1594,7 +1594,7 @@ public void testGetArrays9() throws SolverException, InterruptedException {
       assertThat(prover).isSatisfiable();
 
       try (Model m = prover.getModel()) {
-        for (@SuppressWarnings("unused") ValueAssignment assignment : m) {
+        for (@SuppressWarnings("unused") ValueAssignment assignment : m.asList()) {
           // Check that we can iterate through with no crashes.
         }
         if (m.evaluate(selected1).equals(BigInteger.valueOf(-1))) {
@@ -1615,10 +1615,10 @@ private void testModelIterator(BooleanFormula f) throws SolverException, Interru
       assertThat(prover).isSatisfiable();
 
       try (Model m = prover.getModel()) {
-        for (@SuppressWarnings("unused") ValueAssignment assignment : m) {
+        for (@SuppressWarnings("unused") ValueAssignment assignment : m.asList()) {
           // Check that we can iterate through with no crashes.
         }
-        assertThat(prover.getModelAssignments()).containsExactlyElementsIn(m).inOrder();
+        assertThat(prover.getModelAssignments()).containsExactlyElementsIn(m.asList()).inOrder();
       }
     }
   }
@@ -1661,7 +1661,7 @@ private void testModelGetters(
       try (Model m = prover.getModel()) {
         assertThat(m.evaluate(variable)).isEqualTo(expectedValue);
 
-        for (ValueAssignment va : m) {
+        for (ValueAssignment va : m.asList()) {
           modelAssignments.add(va.getAssignmentAsFormula());
         }
 
@@ -1784,10 +1784,10 @@ private void checkModelIteration(BooleanFormula f, boolean useOptProver)
       prover.push(f);
       assertThat(prover.isUnsat()).isFalse();
       try (Model m = prover.getModel()) {
-        for (@SuppressWarnings("unused") ValueAssignment assignment : m) {
+        for (@SuppressWarnings("unused") ValueAssignment assignment : m.asList()) {
           // Check that we can iterate through with no crashes.
         }
-        assertThat(prover.getModelAssignments()).containsExactlyElementsIn(m).inOrder();
+        assertThat(prover.getModelAssignments()).containsExactlyElementsIn(m.asList()).inOrder();
 
         assignments = prover.getModelAssignments();
       }
@@ -1867,7 +1867,7 @@ public void quantifierTestShort() throws SolverException, InterruptedException {
       prover.push(qmgr.exists(ctr, body));
       assertThat(prover.isUnsat()).isFalse();
       try (Model m = prover.getModel()) {
-        for (ValueAssignment v : m) {
+        for (ValueAssignment v : m.asList()) {
           // a value-assignment might have a different name, but the value should be "0".
           assertThat(BigInteger.ZERO.equals(v.getValue())).isTrue();
         }
@@ -1878,7 +1878,7 @@ public void quantifierTestShort() throws SolverException, InterruptedException {
       prover.push(body);
       assertThat(prover.isUnsat()).isFalse();
       try (Model m = prover.getModel()) {
-        ValueAssignment v = m.iterator().next();
+        ValueAssignment v = m.asList().get(0);
         assertThat("x".equals(v.getName())).isTrue();
         assertThat(BigInteger.ZERO.equals(v.getValue())).isTrue();
       }
diff --git a/src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java b/src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java
index 2bdaa9bea8..c867d737ad 100644
--- a/src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java
+++ b/src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java
@@ -15,6 +15,7 @@
 import com.google.common.collect.ImmutableMap;
 import java.math.BigInteger;
 import java.util.ArrayList;
+import java.util.Arrays;
 import java.util.Collections;
 import java.util.List;
 import java.util.Locale;
@@ -729,9 +730,16 @@ private static void assertConcurrency(String testName, Run runnable) {
     } finally {
       threadPool.shutdownNow();
     }
-    assertWithMessage("Test %s failed with exception(s): %s", testName, exceptionsList)
-        .that(exceptionsList.isEmpty())
-        .isTrue();
+    var exceptionMessages =
+        exceptionsList.stream()
+            .map(
+                ex ->
+                    String.format(
+                        "%s (%s): %s",
+                        ex.getClass(), ex.getMessage(), Arrays.toString(ex.getStackTrace())));
+    assertWithMessage("Test %s failed with exception(s): %s", testName, exceptionMessages)
+        .that(exceptionsList)
+        .isEmpty();
   }
 
   /** just a small lambda-compatible interface. */
diff --git a/src/org/sosy_lab/java_smt/test/SolverStackTest0.java b/src/org/sosy_lab/java_smt/test/SolverStackTest0.java
index 364dc5ece4..ed2bdfe177 100644
--- a/src/org/sosy_lab/java_smt/test/SolverStackTest0.java
+++ b/src/org/sosy_lab/java_smt/test/SolverStackTest0.java
@@ -326,7 +326,7 @@ public void symbolsOnStackTest() throws InterruptedException, SolverException {
     stack.addConstraint(q1);
     assertThat(stack).isSatisfiable();
     Model m1 = stack.getModel();
-    assertThat(m1).isNotEmpty();
+    assertThat(m1.asList()).isNotEmpty();
     stack.pop();
     assertEquals(0, stack.size());
 
@@ -337,7 +337,7 @@ public void symbolsOnStackTest() throws InterruptedException, SolverException {
     stack.addConstraint(q1);
     assertThat(stack).isSatisfiable();
     Model m2 = stack.getModel();
-    assertThat(m2).isNotEmpty();
+    assertThat(m2.asList()).isNotEmpty();
     stack.pop();
     assertEquals(0, stack.size());
   }