Matthias Volk

I am also fine with removing 18.04. We should also update the [documentation](https://www.stormchecker.org/documentation/obtain-storm/build.html#supported-operating-systems).

That could very well be. We are capturing all signals which are sent to Storm and therefore probably also the ones for z3. Do you have an example which triggers...

In principle, Storm should work without an SMT solver (although we never really test it). The documentation strongly recommends having Z3 though: "not strictly required, but already needed for standard...

I agree with Tim that we should only use `STORM_PRINT` in the CLI code. That way, other libraries building upon Storm (such as stormpy) do not have any output from...

Good idea. That means moving them from `src/storm/utility/macros.h` to somewhere in `src/storm-cli-utilities`.

Maybe either use `STORM_LOG_INFO` here with the existing guard, or introduce another logging level `STORM_LOG_STATISTICS`? Depending on how much overhead we want to create, we could also introduce a statistics...

@trolando

Some notes: - Linking with carl could be easily disabled [here](https://github.com/moves-rwth/storm/blob/master/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp#L124) by adding `if (std::is_same::value)` - The main culprit is including `RationalFunctionAdapter.h` in `NumberTraits.h`. Disabling this seems to drastically decrease...

We can reproduce this issue in the current master branch. A minimal example is the following: ##### Sparse `storm --prism ~/prism-benchmarks/models/mdps/wlan/wlan1.nm --prop "Pmax=? [F col=COL]" -const "COL=1" -bisim` yields: ```...

I am also in favour of updating our dependencies. Just as a memo to myself: a newer version of modernjson also allows to simplify code (see [DFTJsonParser](https://github.com/moves-rwth/storm/blob/master/src/storm-dft/parser/DFTJsonParser.cpp#L72)).