Aug 12, 2013 at 7:41 PM
Z3 cannot be used by my (open source) language because someone might then use my language to code, say, an accounting system for their business. Is that correct?

(A commercial license, which would allow them to use the language which relies on Z3, costs $9,999.00.)

Aug 12, 2013 at 7:47 PM
The Isabelle team ( has a similar problem.
They re-distribute Z3 with their theorem prover. This is fine, and the Z3 license allows that.
Since they want to allow commercial users to use Isabelle, they have a "commercial" flag.
When the commercial flag is turned on, plugins such as Z3 are not used.
So, a Isabelle commercial user will not accidentally use Z3 for commercial purposes.