Skip to content
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

Add check to only compile clipping tests if Z3 is installed #410

Merged
merged 1 commit into from
Sep 11, 2023

Conversation

AlexBork
Copy link
Contributor

Add check to only compile clipping tests if Z3 is installed.

Fixes #408

@sjunges
Copy link
Contributor

sjunges commented Aug 28, 2023

Thanks for the quick action.

Two questions/remarks:

  • the changes seem to do more than handle the behavior when z3 is not installed. Can you make sure that the commit message or a comment here reflects that for future reference?
  • wouldnt it be more adequate to let storm::test::z3AtLeastVersion(x, y, z) return false if z3 is not installed, instead of skipping them?

@AlexBork
Copy link
Contributor Author

I reordered the tests a bit so that only one check is needed. The delta looks more complicated as there a couple of similar lines that were interpreted to not be changed, but functionally nothing besides the check changed.

Witht he solution, I followed how this is handeled for example in src/test/storm/modelchecker/multiobjective/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp. Generally, I think it's a good idea to let storm::test::z3AtLeastVersion(x, y, z) return false if z3 is not installed as that would reflect the intuitive meaning of the function. As other instances where this is used should also be guarded using the preprocessor directive, changing it should (hopefully) not create any problems. Let me know if you want me to implement that.

@sjunges
Copy link
Contributor

sjunges commented Aug 28, 2023

Ok, thanks for the explanations. I see that skipping makes sense, and contrary to what I thought, the test-z3-version method is only part of the test-utilities.

LGTM :-)

@tquatmann tquatmann merged commit 410ea45 into moves-rwth:master Sep 11, 2023
14 checks passed
@AlexBork AlexBork deleted the pomdp-test-z3-fix branch June 4, 2024 11:30
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

storm::test::z3AtLeastVersion not found on linux mint
3 participants