New Blog Post: Some Silly Z3 Scripts I Wrote

# New Blog Post: Some Silly Z3 Scripts I Wrote Source: [https://buttondown.com/hillelwayne/archive/new-blog-post-some-silly-z3-scripts-i-wrote](https://buttondown.com/hillelwayne/archive/new-blog-post-some-silly-z3-scripts-i-wrote) Now that I'm not spending all my time on Logic for Programmers, I have time to update my website again\! So here's the first blog post in five months:[Some Silly Z3 Scripts I Wrote](https://www.hillelwayne.com/post/z3-examples/)\. Normally I'd also put a link to the Patreon notes but I've decided I don't like publishing gated content and am going to wind that whole thing down\. So some quick notes about this post: - Part of the point is admittedly to hype up the eventual release of LfP\. I want to start marketing the book, but don't want the marketing material to be devoid of interest, so tangentially\-related\-but\-independent blog posts are a good place to start\. - The post discusses the concept of "chaff", the enormous quantity of material \(both code samples and prose\) that didn't make it into the book\. The book is about 50,000 words… and considerably shorter than the total volume of chaff\! I don't*think*most of it can be turned into useful public posts, but I'm not entirely opposed to the idea\. Maybe some of the old chapters could be made into something? - Coming up with a conditioned mathematical property to prove was a struggle\. I had two candidates:`a == b \* c =\> a / b == c`, which would have required a long tangent on how division must be total in Z3, and`a \!= 0 =\> some b: b \* a == 1`, which would have required introducing a quantifier \(SMT is real weird about quantifiers\)\. Division by zero has already caused me enough grief so I went with the latter\. This did mean I had to reintroduce "operations must be total" when talking about arrays\. - I have no idea why the array example returns`2`for the max profit and not`99999999`\. I'm guessing there's some short circuiting logic in the optimizer when the problem is ill\-defined? - One example I could not get working, which is unfortunate, was a demonstration of how SMT solvers are undecidable via encoding Goldbach's conjecture as an SMT problem\. Anything with multiple nested quantifiers is a pain\. *If you're reading this on the web, you can subscribe[here](https://buttondown.com/hillelwayne)\. Updates are once a week\. My main website is[here](https://www.hillelwayne.com/)\.* *My new book,*Logic for Programmers*, is now in early access\! Get it[here](https://leanpub.com/logic/)\.*