From ee3c08a085ddc07433c67a2333b4d921a8377ca6 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Tue, 14 Jan 2020 12:52:24 +0100
Subject: [PATCH] Set floating-point precision to 10 digits for file export

---
 src/storm/utility/file.h | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/storm/utility/file.h b/src/storm/utility/file.h
index c089eb45a..f5ba06f4a 100644
--- a/src/storm/utility/file.h
+++ b/src/storm/utility/file.h
@@ -22,6 +22,7 @@ namespace storm {
                 filestream.open(filepath);
             }
             STORM_LOG_THROW(filestream, storm::exceptions::FileIoException , "Could not open file " << filepath << ".");
+            filestream.precision(10);
             if (!silent) {
                 STORM_PRINT_AND_LOG("Write to file " << filepath << "." << std::endl);
             }