diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp
index c21ce6ef7..d3e92fd1b 100644
--- a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp
+++ b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp
@@ -525,8 +525,6 @@ namespace storm {
                 }
             }
 
-            STORM_LOG_DEBUG("No. states: " << model->getNumberOfStates());
-            STORM_LOG_DEBUG("No. transitions: " << model->getNumberOfTransitions());
             if (model->getNumberOfStates() <= 15) {
                 STORM_LOG_TRACE("Transition matrix: " << std::endl << model->getTransitionMatrix());
             } else {
diff --git a/src/storm-dft/generator/DftNextStateGenerator.cpp b/src/storm-dft/generator/DftNextStateGenerator.cpp
index 9e9aa7056..245a448ef 100644
--- a/src/storm-dft/generator/DftNextStateGenerator.cpp
+++ b/src/storm-dft/generator/DftNextStateGenerator.cpp
@@ -45,7 +45,7 @@ namespace storm {
         
         template<typename ValueType, typename StateType>
         StateBehavior<ValueType, StateType> DftNextStateGenerator<ValueType, StateType>::expand(StateToIdCallback const& stateToIdCallback) {
-            STORM_LOG_TRACE("Explore state: " << mDft.getStateString(state));
+            STORM_LOG_DEBUG("Explore state: " << mDft.getStateString(state));
 
             // Prepare the result, in case we return early.
             StateBehavior<ValueType, StateType> result;
diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
index 805d54b6b..7f11d1caa 100644
--- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
+++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
@@ -194,9 +194,6 @@ namespace storm {
                     typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::LabelOptions labeloptions(properties);
                     builder.buildModel(labeloptions, 0, 0.0);
                     std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.getModel();
-                    //model->printModelInformationToStream(std::cout);
-                    STORM_LOG_INFO("No. states (Explored): " << model->getNumberOfStates());
-                    STORM_LOG_INFO("No. transitions (Explored): " << model->getNumberOfTransitions());
                     explorationTimer.stop();
 
                     STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Ctmc), storm::exceptions::NotSupportedException, "Parallel composition only applicable for CTMCs");
@@ -219,8 +216,8 @@ namespace storm {
                     composedModel =  storm::performDeterministicSparseBisimulationMinimization<storm::models::sparse::Ctmc<ValueType>>(composedModel, properties, storm::storage::BisimulationType::Weak)->template as<storm::models::sparse::Ctmc<ValueType>>();
                     bisimulationTimer.stop();
 
-                    STORM_LOG_INFO("No. states (Composed): " << composedModel->getNumberOfStates());
-                    STORM_LOG_INFO("No. transitions (Composed): " << composedModel->getNumberOfTransitions());
+                    STORM_LOG_DEBUG("No. states (Composed): " << composedModel->getNumberOfStates());
+                    STORM_LOG_DEBUG("No. transitions (Composed): " << composedModel->getNumberOfTransitions());
                     if (composedModel->getNumberOfStates() <= 15) {
                         STORM_LOG_TRACE("Transition matrix: " << std::endl << composedModel->getTransitionMatrix());
                     } else {
@@ -228,6 +225,7 @@ namespace storm {
                     }
 
                 }
+                composedModel->printModelInformationToStream(std::cout);
                 return composedModel;
             } else {
                 // No composition was possible
@@ -249,9 +247,7 @@ namespace storm {
                 typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::LabelOptions labeloptions(properties);
                 builder.buildModel(labeloptions, 0, 0.0);
                 std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.getModel();
-                //model->printModelInformationToStream(std::cout);
-                STORM_LOG_INFO("No. states (Explored): " << model->getNumberOfStates());
-                STORM_LOG_INFO("No. transitions (Explored): " << model->getNumberOfTransitions());
+                model->printModelInformationToStream(std::cout);
                 explorationTimer.stop();
                 STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Ctmc), storm::exceptions::NotSupportedException, "Parallel composition only applicable for CTMCs");
                 return model->template as<storm::models::sparse::Ctmc<ValueType>>();
@@ -308,8 +304,7 @@ namespace storm {
                     STORM_LOG_INFO("Getting model for lower bound...");
                     model = builder.getModelApproximation(probabilityFormula ? false : true);
                     // We only output the info from the lower bound as the info for the upper bound is the same
-                    STORM_LOG_INFO("No. states: " << model->getNumberOfStates());
-                    STORM_LOG_INFO("No. transitions: " << model->getNumberOfTransitions());
+                    model->printModelInformationToStream(std::cout);
                     buildingTimer.stop();
 
                     // Check lower bounds
@@ -356,9 +351,7 @@ namespace storm {
                     typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions;
                     model = builder.buildModel(labeloptions);
                 }
-                //model->printModelInformationToStream(std::cout);
-                STORM_LOG_INFO("No. states (Explored): " << model->getNumberOfStates());
-                STORM_LOG_INFO("No. transitions (Explored): " << model->getNumberOfTransitions());
+                model->printModelInformationToStream(std::cout);
                 explorationTimer.stop();
 
                 // Model checking
diff --git a/src/storm/utility/storm.h b/src/storm/utility/storm.h
index 3aca0dbe2..ada4ea0d1 100644
--- a/src/storm/utility/storm.h
+++ b/src/storm/utility/storm.h
@@ -192,6 +192,10 @@ namespace storm {
         storm::storage::DeterministicModelBisimulationDecomposition<ModelType> bisimulationDecomposition(*model, options);
         bisimulationDecomposition.computeBisimulationDecomposition();
         model = bisimulationDecomposition.getQuotient();
+
+        // Print some information about the model after the bisimulation
+        model->printModelInformationToStream(std::cout);
+
         STORM_LOG_INFO("Bisimulation done. ");
         return model;
     }
@@ -208,6 +212,10 @@ namespace storm {
         storm::storage::NondeterministicModelBisimulationDecomposition<ModelType> bisimulationDecomposition(*model, options);
         bisimulationDecomposition.computeBisimulationDecomposition();
         model = bisimulationDecomposition.getQuotient();
+
+        // Print some information about the model after the bisimulation
+        model->printModelInformationToStream(std::cout);
+
         STORM_LOG_INFO("Bisimulation done.");
         return model;
     }