# Z3 SMT solver

Hacker Approved page: https://hackerapproved.com/p/z3/

15 people recommended Z3 SMT solver in Hacker News comments, 7 had mixed feelings and 2 criticized it, November 2025 to October 2026. It was recommended in 5 of 12 months, in 7 threads. It meets the Hacker Approved badge rule.

**Verdict:** Free, mature SMT solver that people find convenient and well optimized for constraint problems, though it is slow on some boolean problems and struggles with larger ones.

Summary written by Claude from 21 comments. It was written before the November 2026 recount, and 19 of those comments still count.

## Why people recommend it

- Convenient API and language bindings (3 comments in the sample): "I really like Z3, and I like the convenience of Z3" ([source](https://news.ycombinator.com/item?id=46008672)) "There's a C++ wrapper that works pretty well." ([source](https://news.ycombinator.com/item?id=47818342)) "Z3 is just used for it's convenient API." ([source](https://news.ycombinator.com/item?id=49567265))
- Mature, well-tested, heavily optimized engine (2 comments in the sample): "z3 is also just so thoroughly optimized that even if your formulation of the constraints is inefficient it is faster." ([source](https://news.ycombinator.com/item?id=49566250)) "Z3 is very mature and the Rust bindings are pretty good" ([source](https://news.ycombinator.com/item?id=47815520))
- Handy for puzzles and invariants (2 comments in the sample): "comes in very handy in at least one challenge every year in Advent of Code" ([source](https://news.ycombinator.com/item?id=49575581)) "the loop invariant Z3 can't infer on its own" ([source](https://news.ycombinator.com/item?id=48760277))

## What people warn about

- Slow on boolean and some formulations (3 comments in the sample): "Z3 is capable (it’s an SMT solver, not just SAT), but it’s not very fast at boolean  satifiability" ([source](https://news.ycombinator.com/item?id=47437937)) "If they blend the two and throw the whole thing into Z3 it’ll work but it’ll be needlessly slow." ([source](https://news.ycombinator.com/item?id=47957407)) "pretty slow compared to just checking if a test case passes" ([source](https://news.ycombinator.com/item?id=47676885))

## What people recommend instead

- [Gurobi](https://hackerapproved.com/p/gurobi/): 5 recommend, 1 mixed, 0 criticize

## The badge

A product earns the Hacker Approved badge when at least 10 people recommend it, recommenders outnumber critics at least 2 to 1 (mixed feelings count toward neither side), it was recommended in at least 4 of the 12 months and in at least 5 different threads, and no single thread supplies more than half of the people who recommend it. Health and money products are never badged.

## Cite as

Hacker Approved, "Z3 SMT solver", https://hackerapproved.com/p/z3/ (15 recommend, 7 mixed, 2 criticize; Hacker News comments, November 2025 to October 2026).

Counts updated 2 Nov 2026, with data through October 31, 2026.