diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp
index 7d0d514cb..a8e02dd46 100644
--- a/src/storm/cli/cli.cpp
+++ b/src/storm/cli/cli.cpp
@@ -130,47 +130,23 @@ namespace storm {
         }
 
         void showTimeAndMemoryStatistics(uint64_t wallclockMilliseconds) {
-#ifndef WINDOWS
             struct rusage ru;
             getrusage(RUSAGE_SELF, &ru);
 
-            std::cout << "Performance statistics:" << std::endl;
-            std::cout << "  * peak memory usage: " << ru.ru_maxrss/1024/1024 << " mb" << std::endl;
-            std::cout << "  * CPU time: " << ru.ru_utime.tv_sec << "." << std::setw(3) << std::setfill('0') << ru.ru_utime.tv_usec/1000 << " seconds" << std::endl;
+            std::cout << std::endl << "Performance statistics:" << std::endl;
+#ifdef MACOS
+            // For Mac OS, this is returned in bytes.
+            uint64_t maximumResidentSizeInMegabytes = ru.ru_maxrss / 1024 / 1024;
+#endif
+#ifdef LINUX
+            // For Linux, this is returned in kilobytes.
+            uint64_t maximumResidentSizeInMegabytes = ru.ru_maxrss / 1024;
+#endif
+            std::cout << "  * peak memory usage: " << maximumResidentSizeInMegabytes << "MB" << std::endl;
+            std::cout << "  * CPU time: " << ru.ru_utime.tv_sec << "." << std::setw(3) << std::setfill('0') << ru.ru_utime.tv_usec/1000 << "s" << std::endl;
             if (wallclockMilliseconds != 0) {
-                std::cout << "  * wallclock time: " << (wallclockMilliseconds/1000) << "." << std::setw(3) << std::setfill('0') << (wallclockMilliseconds % 1000) << " seconds" << std::endl;
-            }
-#else
-            HANDLE hProcess = GetCurrentProcess ();
-            FILETIME ftCreation, ftExit, ftUser, ftKernel;
-            PROCESS_MEMORY_COUNTERS pmc;
-            if (GetProcessMemoryInfo( hProcess, &pmc, sizeof(pmc))) {
-                std::cout << "Memory Usage: " << std::endl;
-                std::cout << "\tPageFaultCount: " << pmc.PageFaultCount << std::endl;
-                std::cout << "\tPeakWorkingSetSize: " << pmc.PeakWorkingSetSize << std::endl;
-                std::cout << "\tWorkingSetSize: " << pmc.WorkingSetSize << std::endl;
-                std::cout << "\tQuotaPeakPagedPoolUsage: " << pmc.QuotaPeakPagedPoolUsage << std::endl;
-                std::cout << "\tQuotaPagedPoolUsage: " << pmc.QuotaPagedPoolUsage << std::endl;
-                std::cout << "\tQuotaPeakNonPagedPoolUsage: " << pmc.QuotaPeakNonPagedPoolUsage << std::endl;
-                std::cout << "\tQuotaNonPagedPoolUsage: " << pmc.QuotaNonPagedPoolUsage << std::endl;
-                std::cout << "\tPagefileUsage:" << pmc.PagefileUsage << std::endl;
-                std::cout << "\tPeakPagefileUsage: " << pmc.PeakPagefileUsage << std::endl;
+                std::cout << "  * wallclock time: " << (wallclockMilliseconds/1000) << "." << std::setw(3) << std::setfill('0') << (wallclockMilliseconds % 1000) << "s" << std::endl;
             }
-
-            GetProcessTimes (hProcess, &ftCreation, &ftExit, &ftKernel, &ftUser);
-
-            ULARGE_INTEGER uLargeInteger;
-            uLargeInteger.LowPart = ftKernel.dwLowDateTime;
-            uLargeInteger.HighPart = ftKernel.dwHighDateTime;
-            double kernelTime = static_cast<double>(uLargeInteger.QuadPart) / 10000.0; // 100 ns Resolution to milliseconds
-            uLargeInteger.LowPart = ftUser.dwLowDateTime;
-            uLargeInteger.HighPart = ftUser.dwHighDateTime;
-            double userTime = static_cast<double>(uLargeInteger.QuadPart) / 10000.0;
-
-            std::cout << "CPU Time: " << std::endl;
-            std::cout << "\tKernel Time: " << std::setprecision(5) << kernelTime << "ms" << std::endl;
-            std::cout << "\tUser Time: " << std::setprecision(5) << userTime << "ms" << std::endl;
-#endif
         }
 
         bool parseOptions(const int argc, const char* argv[]) {
diff --git a/src/storm/cli/entrypoints.h b/src/storm/cli/entrypoints.h
index 4097d0bc3..ce7d62227 100644
--- a/src/storm/cli/entrypoints.h
+++ b/src/storm/cli/entrypoints.h
@@ -81,11 +81,10 @@ namespace storm {
                 std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySparseModel(model, property.getFilter().getFormula(), onlyInitialStatesRelevant));
                 modelCheckingWatch.stop();
                 if (result) {
-                    STORM_PRINT_AND_LOG("Time for model checking: " << modelCheckingWatch << "." << std::endl);
                     STORM_PRINT_AND_LOG("Result (initial states): ");
                     result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
                     applyFilterFunctionAndOutput<ValueType>(result, property.getFilter().getFilterType());
-                    STORM_PRINT_AND_LOG(std::endl);
+                    STORM_PRINT_AND_LOG("Time for model checking: " << modelCheckingWatch << "." << std::endl);
                 } else {
                     STORM_PRINT_AND_LOG(" skipped, because the modelling formalism is currently unsupported." << std::endl);
                 }
@@ -104,11 +103,10 @@ namespace storm {
                 std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySparseModel(model, property.getFilter().getFormula(), onlyInitialStatesRelevant));
                 modelCheckingWatch.stop();
                 if (result) {
-                    STORM_PRINT_AND_LOG("Time for model checking: " << modelCheckingWatch << "." << std::endl);
                     STORM_PRINT_AND_LOG("Result (initial states): ");
                     result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
                     applyFilterFunctionAndOutput<storm::RationalFunction>(result, property.getFilter().getFilterType());
-                    STORM_PRINT_AND_LOG(std::endl);
+                    STORM_PRINT_AND_LOG("Time for model checking: " << modelCheckingWatch << "." << std::endl);
                 } else {
                     STORM_PRINT_AND_LOG(" skipped, because the modelling formalism is currently unsupported." << std::endl);
                 }
@@ -130,9 +128,9 @@ namespace storm {
                 std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySymbolicModelWithAbstractionRefinementEngine<DdType, ValueType>(model, property.getFilter().getFormula(), onlyInitialStatesRelevant));
                 modelCheckingWatch.stop();
                 if (result) {
-                    STORM_PRINT_AND_LOG("Time for model checking: " << modelCheckingWatch << "." << std::endl);
                     STORM_PRINT_AND_LOG("Result (initial states): ");
-                    STORM_PRINT_AND_LOG(*result << std::endl);
+                    STORM_PRINT_AND_LOG(*result);
+                    STORM_PRINT_AND_LOG("Time for model checking: " << modelCheckingWatch << "." << std::endl);
                 } else {
                     STORM_PRINT_AND_LOG(" skipped, because the modelling formalism is currently unsupported." << std::endl);
                 }
@@ -182,10 +180,9 @@ namespace storm {
                 }
 
                 if (result) {
-                    STORM_PRINT_AND_LOG("Time for model checking: " << modelCheckingWatch << "." << std::endl);
                     STORM_PRINT_AND_LOG("Result (initial states): ");
                     applyFilterFunctionAndOutput<ValueType>(result, property.getFilter().getFilterType());
-                    STORM_PRINT_AND_LOG(std::endl);
+                    STORM_PRINT_AND_LOG("Time for model checking: " << modelCheckingWatch << "." << std::endl);
                 } else {
                     STORM_PRINT_AND_LOG(" skipped, because the modelling formalism is currently unsupported." << std::endl);
                 }
@@ -210,11 +207,10 @@ namespace storm {
                 modelCheckingWatch.stop();
 
                 if (result) {
-                    STORM_PRINT_AND_LOG("Time for model checking: " << modelCheckingWatch << "." << std::endl);
                     STORM_PRINT_AND_LOG("Result (initial states): ");
                     result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(model->getReachableStates(), model->getInitialStates()));
                     applyFilterFunctionAndOutput<double>(result, property.getFilter().getFilterType());
-                    STORM_PRINT_AND_LOG(std::endl);
+                    STORM_PRINT_AND_LOG("Time for model checking: " << modelCheckingWatch << "." << std::endl);
                 } else {
                     STORM_PRINT_AND_LOG(" skipped, because the modelling formalism is currently unsupported." << std::endl);
                 }
@@ -231,11 +227,10 @@ namespace storm {
                 std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySymbolicModelWithDdEngine(model, property.getFilter().getFormula(), onlyInitialStatesRelevant));
                 modelCheckingWatch.stop();
                 if (result) {
-                    STORM_PRINT_AND_LOG("Time for model checking: " << modelCheckingWatch << "." << std::endl);
                     STORM_PRINT_AND_LOG("Result (initial states): ");
                     result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(model->getReachableStates(), model->getInitialStates()));
                     applyFilterFunctionAndOutput<double>(result, property.getFilter().getFilterType());
-                    STORM_PRINT_AND_LOG(std::endl);
+                    STORM_PRINT_AND_LOG("Time for model checking: " << modelCheckingWatch << "." << std::endl);
                 } else {
                     STORM_PRINT_AND_LOG(" skipped, because the modelling formalism is currently unsupported." << std::endl);
                 }
diff --git a/src/storm/utility/Stopwatch.cpp b/src/storm/utility/Stopwatch.cpp
index fd77c0d59..faefdb472 100644
--- a/src/storm/utility/Stopwatch.cpp
+++ b/src/storm/utility/Stopwatch.cpp
@@ -43,7 +43,7 @@ namespace storm {
         }
         
         std::ostream& operator<<(std::ostream& out, Stopwatch const& stopwatch) {
-            out << stopwatch.getTimeInSeconds() << "." << (stopwatch.getTimeInMilliseconds() % 1000) << "s";
+            out << stopwatch.getTimeInSeconds() << "." << std::setw(3) << std::setfill('0') << (stopwatch.getTimeInMilliseconds() % 1000) << "s";
             return out;
         }