MicrosoftがZ3のオンラインガイドを公開、ブラウザ上でSMTソルバーを試せる

私はZ3がとても気に入っている。犯罪的と言っていいほど過小評価され、使われてもいないと思う。数年前に私が使った、かなり面白い用途を紹介しよう：

https://www.oranlooney.com/post/playfair/#known-plaintext-at...

上記のドキュメントに載っているおもちゃのような例より少し複雑で、Z3の実世界でのユースケースの一つ——暗号に対するレッドチーミング——をほのめかしている。

とはいえ、上にリンクされたドキュメントが、Z3の普及を助けるという意味で本当に役に立っているかというと、そうでもない気がする。