This project is read-only.

Implications of licencing agreement?

Mar 16, 2015 at 6:37 AM
If I use the Z3 engine to optimize my theorems, does Microsoft have any proprietary interest in the simplified theorem, or does it remain as my creation?
Mar 21, 2015 at 6:42 PM
I don't think we would have any claim on the resulting creation, but for commercial use you do need a Z3 license. If necessary we can put you in touch with your licensing experts; do get in touch with one of use personally for that.
Mar 23, 2015 at 2:29 AM
I have a specific question with regard to z3 license. With respect to dynamic binding to z3 as a library, does z3's lincese behave as GPL or LGPL ? Can I release code which includes call to z3 library APIs as BSD/MIT lincense ?
Apr 1, 2015 at 9:29 PM
Edited Apr 1, 2015 at 9:30 PM
Sorry for taking a bit of time on this. As you may have seen already, a few days ago we properly open-sourced Z3 on an MIT license. So, from now on pretty much all of those things are possible. Note that the project is also moving over to github which will be the new hub for Z3 and all related things.