diff --git a/include/vara/Solver/ConfigurationFactory.h b/include/vara/Solver/ConfigurationFactory.h
index 91e458721..a4b4d2f80 100644
--- a/include/vara/Solver/ConfigurationFactory.h
+++ b/include/vara/Solver/ConfigurationFactory.h
@@ -17,7 +17,7 @@ class ConfigurationIterable {
 public:
   class ConfigurationIterator {
   public:
-    using iterator_category = std::forward_iterator_tag;
+    using iterator_category = std::input_iterator_tag;
     using difference_type = std::ptrdiff_t;
     using value_type = std::unique_ptr<vara::feature::Configuration>;
     using pointer = std::unique_ptr<vara::feature::Configuration> *;
@@ -90,8 +90,34 @@ class ConfigurationFactory {
                 std::vector<std::unique_ptr<vara::feature::Configuration>>>
   getAllConfigs(feature::FeatureModel &Model,
                 const vara::solver::SolverType Type = SolverType::Z3) {
-    auto S = SolverFactory::initializeSolver(Model, Type);
-    return S->getAllValidConfigurations();
+    auto V = std::vector<std::unique_ptr<vara::feature::Configuration>>();
+    for (auto Config : ConfigurationFactory::getConfigIterator(Model, Type)) {
+      if (!Config) {
+        return Error(Config.getError());
+      }
+      V.emplace_back(Config.extractValue());
+    }
+    return V;
+  }
+
+  /// This method returns the number of configurations of the given feature
+  /// model.
+  /// Note that this method needs to enumerate all configurations first.
+  /// If you need to access the configurations afterwards, prefer to call
+  /// \c getAllConfigs and check the result's size.
+  ///
+  /// \param Model the given model containing the features and constraints
+  /// \param Type the type of solver to use
+  ///
+  /// \returns the number of configurations for the given model
+  static Result<SolverErrorCode, uint64_t>
+  getNumConfigs(feature::FeatureModel &Model,
+                const vara::solver::SolverType Type = SolverType::Z3) {
+    auto Configs = getAllConfigs(Model, Type);
+    if (!Configs) {
+      return Error(Configs.getError());
+    }
+    return Configs.extractValue().size();
   }
 
   /// This method returns not all but the specified amount of configurations.
diff --git a/include/vara/Solver/Error.h b/include/vara/Solver/Error.h
index 895f4ca52..60f78aad8 100644
--- a/include/vara/Solver/Error.h
+++ b/include/vara/Solver/Error.h
@@ -14,6 +14,7 @@ enum SolverErrorCode {
   ALREADY_PRESENT,
   NOT_ALL_CONSTRAINTS_PROCESSED,
   PARENT_NOT_PRESENT,
+  ILLEGAL_STATE,
 };
 
 } // namespace solver
@@ -52,6 +53,9 @@ class Error<vara::solver::SolverErrorCode> {
     case vara::solver::PARENT_NOT_PRESENT:
       OS << "Parent feature of a feature is not present.";
       break;
+    case vara::solver::ILLEGAL_STATE:
+      OS << "The solver is in an illegal state for this operation.";
+      break;
     }
     return OS;
   }
diff --git a/include/vara/Solver/Solver.h b/include/vara/Solver/Solver.h
index d5a73e3fc..5ef5950b1 100644
--- a/include/vara/Solver/Solver.h
+++ b/include/vara/Solver/Solver.h
@@ -117,15 +117,6 @@ class Solver {
   /// the current constraint system is solvable (\c true) or not (\c false).
   virtual Result<SolverErrorCode, bool> hasValidConfigurations() = 0;
 
-  /// Returns the number of valid configurations of the current constraint
-  /// system (i.e., its features and its constraints). In principle, this is a
-  /// #SAT call (i.e., enumerating all configurations).
-  ///
-  /// \returns an error if the number of valid configurations can not be
-  /// retried. This can be the case if there are still constraints left that
-  /// were not included into the solver because of missing variables.
-  virtual Result<SolverErrorCode, uint64_t> getNumberValidConfigurations() = 0;
-
   /// Returns the current configuration.
   ///
   /// \returns the current configuration found by the solver an error code in
@@ -140,16 +131,6 @@ class Solver {
   /// unsatisfiable).
   virtual Result<SolverErrorCode, std::unique_ptr<vara::feature::Configuration>>
   getNextConfiguration() = 0;
-
-  /// Returns all valid configurations. In comparison to \c
-  /// getNumberValidConfigurations, this method returns the configurations
-  /// instead of a number of configurations.
-  ///
-  /// \returns an error if an error occurs while retrieving the configurations.
-  /// Otherwise, it will return the configurations.
-  virtual Result<SolverErrorCode,
-                 std::vector<std::unique_ptr<vara::feature::Configuration>>>
-  getAllValidConfigurations() = 0;
 };
 
 } // namespace vara::solver
diff --git a/include/vara/Solver/Z3Solver.h b/include/vara/Solver/Z3Solver.h
index cd43e3a8b..9a5772b25 100644
--- a/include/vara/Solver/Z3Solver.h
+++ b/include/vara/Solver/Z3Solver.h
@@ -60,23 +60,16 @@ class Z3Solver : public Solver {
   Result<SolverErrorCode, std::unique_ptr<vara::feature::Configuration>>
   getCurrentConfiguration() override;
 
-  Result<SolverErrorCode, uint64_t> getNumberValidConfigurations() override;
-
   Result<SolverErrorCode, std::unique_ptr<vara::feature::Configuration>>
   getNextConfiguration() override;
 
-  Result<SolverErrorCode,
-         std::vector<std::unique_ptr<vara::feature::Configuration>>>
-  getAllValidConfigurations() override;
-
 private:
   // The Z3SolverConstraintVisitor is a friend class to access the solver and
   // the context.
   friend class Z3SolverConstraintVisitor;
 
-  /// Exclude the current configuration by adding it as a constraint
-  /// \return an error code in case of error.
-  Result<SolverErrorCode> excludeCurrentConfiguration();
+  /// Exclude the current configuration by adding it as a constraint.
+  void excludeCurrentConfiguration();
 
   /// Processes the constraints of the binary feature and ignores the 'optional'
   /// constraint if the feature is in an alternative group.
@@ -95,6 +88,9 @@ class Z3Solver : public Solver {
   /// The instance of the Z3 solver needed for caching the constraints and
   /// variables.
   std::unique_ptr<z3::solver> Solver;
+
+  /// The current model of the SAT solver.
+  std::optional<z3::model> CurrentModel;
 };
 
 /// \brief This class is a visitor to convert the constraints from the
diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp
index f28c9d4de..1df128ab2 100644
--- a/lib/Solver/Z3Solver.cpp
+++ b/lib/Solver/Z3Solver.cpp
@@ -169,6 +169,12 @@ Result<SolverErrorCode> Z3Solver::addMixedConstraint(
 }
 
 Result<SolverErrorCode, bool> Z3Solver::hasValidConfigurations() {
+  // If CurrentModel exists, we heave already modified the solver state, thus,
+  // the result of this function might be wrong.
+  if (CurrentModel) {
+    return Error(ILLEGAL_STATE);
+  }
+
   if (Solver->check() == z3::sat) {
     return Ok(true);
   }
@@ -177,38 +183,14 @@ Result<SolverErrorCode, bool> Z3Solver::hasValidConfigurations() {
 
 Result<SolverErrorCode, std::unique_ptr<vara::feature::Configuration>>
 Z3Solver::getNextConfiguration() {
-  // Add previous configuration as a constraint
+  if (Solver->check() == z3::unsat) {
+    return UNSAT;
+  }
+  CurrentModel = Solver->get_model();
   excludeCurrentConfiguration();
-
-  // Retrieve the next configuration
   return getCurrentConfiguration();
 }
 
-Result<SolverErrorCode, uint64_t> Z3Solver::getNumberValidConfigurations() {
-  Solver->push();
-  uint64_t Count = 0;
-  while (Solver->check() == z3::sat) {
-    excludeCurrentConfiguration();
-    Count++;
-  }
-  Solver->pop();
-  return Count;
-}
-
-Result<SolverErrorCode,
-       std::vector<std::unique_ptr<vara::feature::Configuration>>>
-Z3Solver::getAllValidConfigurations() {
-  Solver->push();
-  auto Vector = std::vector<std::unique_ptr<vara::feature::Configuration>>();
-  while (Solver->check() == z3::sat) {
-    auto Config = getCurrentConfiguration().extractValue();
-    Vector.insert(Vector.begin(), std::move(Config));
-    excludeCurrentConfiguration();
-  }
-  Solver->pop();
-  return Vector;
-}
-
 Result<SolverErrorCode>
 Z3Solver::setBinaryFeatureConstraints(const feature::BinaryFeature &Feature,
                                       bool IsInAlternativeGroup) {
@@ -226,43 +208,40 @@ Z3Solver::setBinaryFeatureConstraints(const feature::BinaryFeature &Feature,
   return Ok();
 }
 
-Result<SolverErrorCode> Z3Solver::excludeCurrentConfiguration() {
-  if (Solver->check() == z3::unsat) {
-    return UNSAT;
+void Z3Solver::excludeCurrentConfiguration() {
+  if (!CurrentModel) {
+    return;
   }
-  const z3::model M = Solver->get_model();
+
   z3::expr Expr = Context.bool_val(false);
-  for (auto Iterator = OptionToVariableMapping.begin();
-       Iterator != OptionToVariableMapping.end(); Iterator++) {
-    const z3::expr OptionExpr = *Iterator->getValue();
-    const z3::expr Value = M.eval(OptionExpr, true);
+  for (const auto &Entry : OptionToVariableMapping) {
+    const z3::expr OptionExpr = *Entry.getValue();
+    const z3::expr Value = CurrentModel->eval(OptionExpr, true);
     if (Value.is_bool()) {
       if (Value.is_true()) {
-        Expr = Expr || !*Iterator->getValue();
+        Expr = Expr || !OptionExpr;
       } else {
-        Expr = Expr || *Iterator->getValue();
+        Expr = Expr || OptionExpr;
       }
     } else {
-      Expr = Expr || (*Iterator->getValue() != Value);
+      Expr = Expr || (OptionExpr != Value);
     }
   }
   Solver->add(Expr);
-  return Ok();
 }
 
 Result<SolverErrorCode, std::unique_ptr<vara::feature::Configuration>>
 Z3Solver::getCurrentConfiguration() {
-  if (Solver->check() == z3::unsat) {
-    return UNSAT;
+  if (!CurrentModel) {
+    return getNextConfiguration();
   }
-  const z3::model M = Solver->get_model();
+
   auto Config = std::make_unique<vara::feature::Configuration>();
 
-  for (auto Iterator = OptionToVariableMapping.begin();
-       Iterator != OptionToVariableMapping.end(); Iterator++) {
-    const z3::expr OptionExpr = *Iterator->getValue();
-    const z3::expr Value = M.eval(OptionExpr, true);
-    Config->setConfigurationOption(Iterator->getKey(),
+  for (const auto &Entry : OptionToVariableMapping) {
+    const z3::expr OptionExpr = *Entry.getValue();
+    const z3::expr Value = CurrentModel->eval(OptionExpr, true);
+    Config->setConfigurationOption(Entry.getKey(),
                                    llvm::StringRef(Value.to_string()));
   }
   return Config;
diff --git a/unittests/Solver/ConfigurationFactory.cpp b/unittests/Solver/ConfigurationFactory.cpp
index 5170271fa..418afed41 100644
--- a/unittests/Solver/ConfigurationFactory.cpp
+++ b/unittests/Solver/ConfigurationFactory.cpp
@@ -2,6 +2,8 @@
 
 #include "vara/Feature/ConstraintBuilder.h"
 #include "vara/Feature/FeatureModelBuilder.h"
+
+#include "Utils/UnittestHelper.h"
 #include "gtest/gtest.h"
 
 namespace vara::solver {
@@ -51,6 +53,43 @@ TEST(ConfigurationFactory, GetAllConfigurations) {
   EXPECT_EQ(ConfigResult.extractValue().size(), 6 * 63);
 }
 
+TEST(ConfigurationFactory, GetAllConfigurations2) {
+  auto FM = feature::loadFeatureModel(
+      getTestResource("test_three_optional_features.xml"));
+  auto ConfigResult = ConfigurationFactory::getAllConfigs(*FM);
+  EXPECT_TRUE(ConfigResult);
+  auto Configs = ConfigResult.extractValue();
+
+  EXPECT_EQ(Configs.size(), 8);
+
+  auto ConfigsStrings = std::vector<string>();
+  for (auto &Config : Configs) {
+    ConfigsStrings.push_back(Config->dumpToString());
+  }
+
+  auto UniqueConfigs =
+      std::set<string>(ConfigsStrings.begin(), ConfigsStrings.end());
+  EXPECT_EQ(Configs.size(), UniqueConfigs.size());
+}
+
+TEST(ConfigurationFactory, GetAllConfigurations3) {
+  auto FM = feature::loadFeatureModel(getTestResource("test_msmr.xml"));
+  auto ConfigResult = ConfigurationFactory::getAllConfigs(*FM);
+  EXPECT_TRUE(ConfigResult);
+  auto Configs = ConfigResult.extractValue();
+
+  EXPECT_EQ(Configs.size(), 16);
+
+  auto ConfigsStrings = std::vector<string>();
+  for (auto &Config : Configs) {
+    ConfigsStrings.push_back(Config->dumpToString());
+  }
+
+  auto UniqueConfigs =
+      std::set<string>(ConfigsStrings.begin(), ConfigsStrings.end());
+  EXPECT_EQ(Configs.size(), UniqueConfigs.size());
+}
+
 TEST(ConfigurationFactory, GetNConfigurations) {
   auto FM = getFeatureModel();
   auto ConfigResult = ConfigurationFactory::getNConfigs(*FM, 100);
diff --git a/unittests/Solver/SolverFactory.cpp b/unittests/Solver/SolverFactory.cpp
index 574ce7a34..5f90e8701 100644
--- a/unittests/Solver/SolverFactory.cpp
+++ b/unittests/Solver/SolverFactory.cpp
@@ -2,15 +2,16 @@
 
 #include "vara/Feature/ConstraintBuilder.h"
 #include "vara/Feature/FeatureModelBuilder.h"
+#include "vara/Solver/ConfigurationFactory.h"
 #include "gtest/gtest.h"
 
 namespace vara::solver {
 
 TEST(SolverFactory, EmptyZ3SolverTest) {
   auto S = SolverFactory::initializeSolver(SolverType::Z3);
-  auto E = S->getNumberValidConfigurations();
-  EXPECT_TRUE(E);
-  EXPECT_EQ(E.extractValue(), 1);
+  auto I = ConfigurationIterable(std::move(S));
+  EXPECT_TRUE(*I.begin());
+  EXPECT_EQ(std::distance(I.begin(), I.end()), 1);
 }
 
 TEST(SolverFactory, GeneralZ3Test) {
@@ -51,9 +52,9 @@ TEST(SolverFactory, GeneralZ3Test) {
   auto FM = B.buildFeatureModel();
   auto S = SolverFactory::initializeSolver(*FM, SolverType::Z3);
 
-  auto E = S->getNumberValidConfigurations();
-  EXPECT_TRUE(E);
-  EXPECT_EQ(E.extractValue(), 6 * 63);
+  auto I = ConfigurationIterable(std::move(S));
+  EXPECT_TRUE(*I.begin());
+  EXPECT_EQ(std::distance(I.begin(), I.end()), 6 * 63);
 }
 
 } // namespace vara::solver
diff --git a/unittests/Solver/Z3Tests.cpp b/unittests/Solver/Z3Tests.cpp
index bd36af3b0..ccc4d32dd 100644
--- a/unittests/Solver/Z3Tests.cpp
+++ b/unittests/Solver/Z3Tests.cpp
@@ -3,6 +3,7 @@
 #include "z3++.h"
 
 #include "vara/Feature/FeatureModelBuilder.h"
+#include "vara/Solver/ConfigurationFactory.h"
 #include "gtest/gtest.h"
 
 namespace vara::solver {
@@ -54,10 +55,6 @@ TEST(Z3Solver, AddFeatureObjectTest) {
   V = S->hasValidConfigurations();
   EXPECT_TRUE(V);
   EXPECT_TRUE(V.extractValue());
-  // Enumerate the solutions
-  auto Enumerate = S->getNumberValidConfigurations();
-  EXPECT_TRUE(Enumerate);
-  EXPECT_EQ(2, Enumerate.extractValue());
 
   E = S->addFeature(*FM->getFeature("B"));
   EXPECT_TRUE(E);
@@ -68,37 +65,10 @@ TEST(Z3Solver, AddFeatureObjectTest) {
   EXPECT_FALSE(E);
   EXPECT_EQ(SolverErrorCode::ALREADY_PRESENT, E.getError());
 
-  // Enumerate the solutions
-  Enumerate = S->getNumberValidConfigurations();
-  EXPECT_TRUE(Enumerate);
-  EXPECT_EQ(6, Enumerate.extractValue());
-
   E = S->addFeature(*FM->getFeature("C"));
   EXPECT_TRUE(E);
   V = S->hasValidConfigurations();
   EXPECT_TRUE(V.extractValue());
-  Enumerate = S->getNumberValidConfigurations();
-  EXPECT_TRUE(Enumerate);
-  EXPECT_EQ(6, Enumerate.extractValue());
-}
-
-TEST(Z3Solver, TestAllValidConfigurations) {
-  std::unique_ptr<Z3Solver> S = Z3Solver::create();
-  vara::feature::FeatureModelBuilder B;
-  B.makeRoot("root");
-  B.makeFeature<vara::feature::BinaryFeature>("Foo", true);
-  B.addEdge("root", "Foo");
-  std::vector<int64_t> Values{0, 1};
-  B.makeFeature<vara::feature::NumericFeature>("Num1", Values);
-  auto FM = B.buildFeatureModel();
-
-  S->addFeature(*FM->getFeature("root"));
-  S->addFeature(*FM->getFeature("Foo"));
-  S->addFeature(*FM->getFeature("Num1"));
-
-  auto C = S->getAllValidConfigurations();
-  EXPECT_TRUE(C);
-  EXPECT_EQ(C.extractValue().size(), 4);
 }
 
 TEST(Z3Solver, TestGetNextConfiguration) {
@@ -115,7 +85,7 @@ TEST(Z3Solver, TestGetNextConfiguration) {
   S->addFeature(*FM->getFeature("Foo"));
   S->addFeature(*FM->getFeature("Num1"));
 
-  for (int Count = 0; Count < 3; Count++) {
+  for (int Count = 0; Count < 4; Count++) {
     auto C = S->getNextConfiguration();
     EXPECT_TRUE(C);
     auto Config = C.extractValue();
@@ -158,9 +128,9 @@ TEST(Z3Solver, AddImpliesConstraint) {
   S->addFeature(*FM->getFeature("a"));
   S->addFeature(*FM->getFeature("b"));
   S->addConstraint(*C);
-  auto E = S->getNumberValidConfigurations();
-  EXPECT_TRUE(E);
-  EXPECT_EQ(E.extractValue(), 6);
+  auto I = ConfigurationIterable(std::move(S));
+  EXPECT_TRUE(*I.begin());
+  EXPECT_EQ(std::distance(I.begin(), I.end()), 6);
 }
 
 TEST(Z3Solver, AddAlternative) {
@@ -203,9 +173,10 @@ TEST(Z3Solver, AddAlternative) {
   for (const auto &R : FM->relationships()) {
     S->addRelationship(*R);
   }
-  auto E = S->getNumberValidConfigurations();
-  EXPECT_TRUE(E);
-  EXPECT_EQ(E.extractValue(), 63);
+
+  auto I = ConfigurationIterable(std::move(S));
+  EXPECT_TRUE(*I.begin());
+  EXPECT_EQ(std::distance(I.begin(), I.end()), 63);
 }
 
 } // namespace vara::solver
diff --git a/unittests/resources/CMakeLists.txt b/unittests/resources/CMakeLists.txt
index a243fcb77..dbf71e528 100644
--- a/unittests/resources/CMakeLists.txt
+++ b/unittests/resources/CMakeLists.txt
@@ -32,6 +32,7 @@ set(FEATURE_LIB_TEST_FILES
     xml/test_hsqldb_num.xml
     xml/test_member_offset.xml
     xml/test_mixed_constraints.xml
+    xml/test_msmr.xml
     xml/test_numbers.xml
     xml/test_only_children.xml
     xml/test_only_parents.xml
@@ -39,6 +40,7 @@ set(FEATURE_LIB_TEST_FILES
     xml/test_output_string.xml
     xml/test_revision_range.xml
     xml/test_step_function.xml
+    xml/test_three_optional_features.xml
     xml/test_with_whitespaces.xml
     yml/dune_configs.yml
 )
diff --git a/unittests/resources/xml/test_msmr.xml b/unittests/resources/xml/test_msmr.xml
new file mode 100644
index 000000000..54d2c13c8
--- /dev/null
+++ b/unittests/resources/xml/test_msmr.xml
@@ -0,0 +1,48 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE vm SYSTEM "vm.dtd">
+<vm name="SingleLocalSingle" root="root">
+    <binaryOptions>
+        <configurationOption>
+            <name>root</name>
+            <parent></parent>
+            <optional>False</optional>
+        </configurationOption>
+        <configurationOption>
+            <name>Slow</name>
+            <outputString>--slow</outputString>
+            <parent>root</parent>
+            <optional>True</optional>
+        </configurationOption>
+        <configurationOption>
+            <name>Header</name>
+            <outputString>--header</outputString>
+            <parent>root</parent>
+            <optional>True</optional>
+        </configurationOption>
+        <configurationOption>
+            <name>Extern</name>
+            <outputString>--extern</outputString>
+            <parent>root</parent>
+            <optional>True</optional>
+            <locations>
+                <sourceRange category="necessary">
+                    <path>src/MultiSharedMultipleRegions/FeatureHeader.cpp</path>
+                    <start>
+                        <line>3</line>
+                        <column>6</column>
+                    </start>
+                    <end>
+                        <line>3</line>
+                        <column>18</column>
+                    </end>
+                </sourceRange>
+            </locations>
+        </configurationOption>
+        <configurationOption>
+            <name>Cpp</name>
+            <outputString>--cpp</outputString>
+            <parent>root</parent>
+            <optional>True</optional>
+        </configurationOption>
+    </binaryOptions>
+</vm>
diff --git a/unittests/resources/xml/test_three_optional_features.xml b/unittests/resources/xml/test_three_optional_features.xml
new file mode 100644
index 000000000..d18ea984f
--- /dev/null
+++ b/unittests/resources/xml/test_three_optional_features.xml
@@ -0,0 +1,29 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE vm SYSTEM "vm.dtd">
+<vm name="SingleLocalSingle" root="root">
+  <binaryOptions>
+    <configurationOption>
+      <name>root</name>
+      <parent></parent>
+      <optional>False</optional>
+    </configurationOption>
+    <configurationOption>
+      <name>A</name>
+      <outputString>A</outputString>
+      <parent>root</parent>
+      <optional>True</optional>
+    </configurationOption>
+    <configurationOption>
+      <name>B</name>
+      <outputString>B</outputString>
+      <parent>root</parent>
+      <optional>True</optional>
+    </configurationOption>
+    <configurationOption>
+      <name>C</name>
+      <outputString>C</outputString>
+      <parent>root</parent>
+      <optional>True</optional>
+    </configurationOption>
+  </binaryOptions>
+</vm>