Skip to content

Draft: Prepare Release 6.0.0 #495

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

Draft
wants to merge 3 commits into
base: master
Choose a base branch
from
Draft

Draft: Prepare Release 6.0.0 #495

wants to merge 3 commits into from

Conversation

baierd
Copy link
Contributor

@baierd baierd commented Jul 21, 2025

To prepare the release of 6.0.0 we should discuss all changes that we included and want to include, as well as update our README and info material to reflect the current state of JavaSMT.

TODO:

  • All breaking changes that we plan to do should be included in this PR. For example Cleanup usage of bound variables #491.
  • We need to discuss which changes currently under development are supposed to be finished for this release.
  • We need to update our info material to reflect the current version of JavaSMT. We should be clear about future developments (e.g. we want to update to Java 17 soon and 21 next year), as well as the current requirements and dependencies (i.e. what is needed to run or build our solvers).
  • We need to write a thorough release message with the many changes that piled up, as well as our plans for the future regarding Java versions etc.

@baierd baierd self-assigned this Jul 21, 2025
@baierd baierd marked this pull request as draft July 21, 2025 15:38
@kfriedberger
Copy link
Member

This issue is a good first step towards the next release. Thanks for making the steps transparent.

@baierd baierd added this to the Release 6.0.0 milestone Jul 29, 2025
@baierd
Copy link
Contributor Author

baierd commented Jul 31, 2025

Note: Version 6 will be the last mayor release for Java 11. We will move to Java 17 soon after and aim to adopt Java 21 in 2026.

Changelog (WIP):

  • Many API calls in the Model and ProverEnvironment now throw SolverException and InterruptedException, as some solvers can throw these exceptions when executing the changed operations. MathSAT5 now throws a SolverException in cases in which model generation fails when requesting a model, instead of the previous IllegalArgumentException. Warning: Model.iterator() may throw the checked exceptions SolverException and InterruptedException although these exceptions are not declared with throws due to API restrictions.
  • ProverEnvironment, InterpolatingProverEnvironment, and OptimizationProverEnvironment can now be created with an optional ShutdownNotifier, allowing the re-use of the creating SolverContext after the shutdown of the ProverEnvironment. This is currently supported for the following solvers: Bitwuzla, CVC4, MathSAT5, Z3, Yices2, and OpenSMT2.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Development

Successfully merging this pull request may close these issues.

2 participants