The Z3 theorem prover is now open source

This is great news! When I was at MSR I heard the rumor that they wanted to <i>sell</i> Z3, not open-source it!<p>Some context, as not everybody may have heard about it.<p>Z3 is an SMT [1] solver. Since SMT generalizes SAT, it is clearly NP-hard, so a number of heuristics are needed. In particular, Z3 won several SMT speed competitions, so it has been for long the fastest SMT solver.<p>You can play with it online using its Lisp-like native language [2] or using the Python bindings [3]<p>The reason SMT is important is that several static analysis tools work by encoding the program constraints (such as pre/post conditions, invariants, ...) into a big formula. The satisfiability of this formula determines the correctness of the program, and sometimes assignments can be translated back to counterexamples to program correctness.<p>[1] <a href="http://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories" rel="nofollow">http://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories</a><p>[2] <a href="http://rise4fun.com/Z3/bit-count" rel="nofollow">http://rise4fun.com/Z3/bit-count</a><p>[3] <a href="http://rise4fun.com/Z3Py/nonlinear" rel="nofollow">http://rise4fun.com/Z3Py/nonlinear</a>

The limitation to non-commercial use means it's not quite 'open source' in the common meaning established by the Open Source Initiative. (Discrimination against a 'field of endeavor', such as business use, is not allowable under their definition.)

Non-commercial only. There are several similar projects some of which are <i>really</i> open source: <a href="http://smtlib.cs.uiowa.edu/solvers.html" rel="nofollow">http://smtlib.cs.uiowa.edu/solvers.html</a>

I think one of the problems with it not being true open source is that they are selling a commercial version @ the microsoft store for 14,950. I suspect this is why they choose this license.<p>I'd be interested if they would provide different terms for the source for the people that bought the commercial version, or if you would just be stuck with the binaries.<p>Here is the link to buy the commercial version: <a href="http://www.microsoftstore.com/store/msstore/pd/Microsoft-Research-Z3-Theorem-Prover/productID.242666500" rel="nofollow">http://www.microsoftstore.com/store/msstore/pd/Microsoft-Res...</a>

It seemed really exciting until I realized that it is only available for non-commercial purposes.

That's excellent (good to learn from, shame it's only non commercial; it's a step forward though)! I was accidentally checking rise4fun for open source just last week. I hope they open source more; unfortunately the project I'm most curious about at the moment (quickcode) will not be open sourced as it is officially part of Excel now.

As a plain old programmer, would a tool like this be useful to me? How can I use a theorem prover to improve my code, or make it easier to write my code on a day to day basis? I've heard that Z3 is used for demonstrating security properties, how would I apply this to ensure my own systems are secure?

Wish someone would update the topic here, since it's not open source as per the generally understood definition ... (as the article's source has updated / corrected on his blog)

Anyone able to find a link to the code? I have been looking around but I can only seem to find the binaries.

People bitching about MS misusing the term "open-source" are, IMO, ungrateful SOBs who have never attempted to implement a non-trivial algorithm based on nothing but a stack of academic papers.<p>For me, the greatest value in having the source is to <i>learn</i> from it, not to hijack it.

Could this be used to tes ZED models?

From the license text:<p>&#62; Microsoft is granted back, without any restrictions or limitations, a non-exclusive, perpetual, irrevocable, royalty-free, assignable and sub-licensable license, to reproduce, publicly perform or display, install, use, modify, post, distribute, make and have made, sell and transfer your modifications to and/or derivative works of the Software source code or data, for any purpose.<p>The above I can understand. MSFT claims ownership of any modifications you make to its software. Be aware.<p>&#62; [A]ny feedback about the Software provided by you to us is voluntarily given, and Microsoft shall be free to use the feedback as it sees fit without obligation or restriction of any kind, even if the feedback is designated by you as confidential.<p>This I don't get. Why would MSFT want to publish confidential feedback?<p>&#62; That if you breach this MSR-LA or if you sue anyone over patents that you think may apply to or read on the Software or anyone's use of the Software, this MSR-LA (and your license and rights obtained herein) terminate automatically. Upon any such termination, you shall destroy all of your copies of the Software immediately. Sections 3, 4, 5, 6, 7, 8, 11 and 12 of this MSR-LA shall survive any termination of this MSR-LA.<p>This part I certainly understand. "Sue us and you can't use our toys anymore."<p>&#62; That the patent rights, if any, granted to you in this MSR-LA only apply to the Software, not to any derivative works you make.<p>This, again, is unsurprising, but good to keep in mind.