# New Blog Post: Some Silly Z3 Scripts I Wrote

DevFeed: [New Blog Post: Some Silly Z3 Scripts I Wrote](<https://devfeed.tech/articles/new-blog-post-some-silly-z3-scripts-i-wrote-25496.md>)

Original publisher: [Read original article](<https://buttondown.com/hillelwayne/archive/new-blog-post-some-silly-z3-scripts-i-wrote/>)

Author: Hillel Wayne

Published: 2026-02-23T16:49:10Z

Content type: article

Language: en

Sources: [Newsletter feed for Hillel Wayne's Newsletter](<https://devfeed.tech/sources/newsletter-feed-for-hillel-wayne-s-newsletter.md>)

Topics: [Code](<https://devfeed.tech/topics/code.md>), [Math and Logic](<https://devfeed.tech/topics/math-and-logic.md>), [Script](<https://devfeed.tech/topics/script.md>)

Tags: [blog-post](<https://devfeed.tech/tags/blog-post.md>), [code](<https://devfeed.tech/tags/code.md>), [idea](<https://devfeed.tech/tags/idea.md>)

## AI overview

The author announces a new blog post containing Z3 scripts and discusses its mathematical examples, including total operations, arrays, quantifiers, and an unsuccessful attempt to encode Goldbach's conjecture as an SMT problem.

## Source excerpt

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. 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.