Storm without SMT-Checker

[sjunges]

From some conversation, I think there may be an issue when installing storm without an SMT solver.

This can certainly be fixed, but it made me wonder whether we still want to have this as an optional setting. In terms of bringing down configurations, it may be nice to make a SMT solver a requirement (currently, Z3, I guess).

[volkm]

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 tasks like PRISM/JANI model building". For the DFT parts, an SMT solver should not really be required. So still keeping it optional would be preferable?

[sjunges]

I understand that some parts can be done without an SMT solver, but I dont think installing an SMT solver is a big hurdle. On other hand, I can understand if you want to keep the dft part easy.

In that case, can we add such a config to CI? Maybe not to the CI checks that run on every check, but still, I dont think any of the developers is testing for these cases.

[sjunges]

In an email, we got:

BTW, in "general dependencies" you mention z3 as "recommended" but to build
BeliefExplorationPomdpModelCheckerTest.cpp
z3 is indeed required. It throws an error, not just a warning ;-)

this can of course also be fixed by fixing this test.

[AlexBork]

In an email, we got:

BTW, in "general dependencies" you mention z3 as "recommended" but to build
BeliefExplorationPomdpModelCheckerTest.cpp
z3 is indeed required. It throws an error, not just a warning ;-)

this can of course also be fixed by fixing this test.

I have not been able to reproduce the error using the main branch when disabling Z3 support on my machine. The tests where this is relevant in BeliefExplorationPomdpModelCheckerTest.cpp should not be compiled when Z3 is not available. Any idea if anything else might cause it?