Question about LICENSE

[hernanponcedeleon]

We are about to finish the migration from Z3 java API to JavaSMT in Dartagnan (which is licensed under the
MIT License) and I have some doubts what is requires in terms of licenses. There are two different scenarios

1. Dartagnan git repository. The dependency to JavaSMT (and the corresponding solver dependencies) is handled via maven. If I understand it correctly, nothing needs to be done for this case in terms of licenses (please correct me if I'm wrong). We will obviously mentioned that Dartagnan depends on JavaSMT in the README.
2. Sv-comp. When we prepare the archive of the verifier, we need to distribute several JavaSMT dependencies (*.jar and *.so). I guess here we need to include JavaSMT LICENSE (Apache 2.0) and all the licenses listed in the LICENSES folder. Am I right?

[PhilippWendler]

The answer in general is the same for all libraries one uses:

1. Yes. As long as you do not redistribute work of others, most open-source licenses do not impose any requirements on you.
2. In principle, yes. Most open-source licenses require you to bundle the full license text and all existing copyright notices, so you must make sure that this is fulfilled for all works that you ship.

For JavaSMT, the latter means:

• The full license texts for everything that is in the JavaSMT repo are in LICENSES/. Not all licenses in this folder are used for the actual source of JavaSMT, though, so not all of them might need to be bundled. I think that actually only Apache-2.0 applies to the source and needs to be bundled with a JavaSM JAR file, but @kfriedberger needs to confirm this. (This should actually be documented more clearly. And if more than Apache-2.0 is needed, then the metadata in places like the Ivy repository is incorrect and needs to be fixed, and we also would need to bundle the respective license texts in the JAR file as we do with the Apache license.)
• LICENSES/ does not cover the license of the solver(s) you use, because we do not ship these in the JavaSMT repo. You need to make sure to fulfill the solver licenses on your own.

[kfriedberger]

JavaSMT is under Apache-2.0.

The JavaSMT bindings for interacting with Yices2 is additionally under GPL-3.0. We have separated the code for Yices interaction into a dependency library for our Ivy and Maven repository (Yices is not yet available in Maven, see #221). If Yices2 is not used, Apache-2.0 is still sufficient.

For any dependency library (solvers and other Java libraries), you need to take care on your own.

[hernanponcedeleon]

Great. Thanks for the clarification.