-
Notifications
You must be signed in to change notification settings - Fork 73
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Storm without SMT-Checker #282
Comments
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". |
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. |
In an email, we got:
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? |
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).
The text was updated successfully, but these errors were encountered: