Hacker GitHub

← All repos

Z3Prover/z3

View on GitHub ↗ ★ 12,873 C++

The Z3 Theorem Prover

48 mentions on Hacker News by 42 people: 14 stories, 34 comments · first 2015-03-26 · latest 2026-04-18

Mentions per year 48 mentions · busiest year 2019 (7)
20082026
AllStoriesComments NewestTopOldest
  1. It's reference-counted at the boundaries. See https://github.com/Z3Prover/z3/blob/daf2506b6002149d531cb6c9...
    comment by invl · 2026-04-18 · in A Dumb Introduction to Z3 (2025)
  2. ▲ 5
    Show HN: Sigil – A new programming language for AI agents
    story by inerte · 2026-04-05 · 5 comments
  3. ▲ 35
    The Z3 Theorem Prover
    story by benoitg · 2025-12-10 · 2 comments
  4. …verification, and optimization.” https://www.microsoft.com/en-us/research/project/z3-3/ See also: https://github.com/Z3Prover/z3
    comment by gbacon · 2025-11-17 · in Z3 API in Python: From Sudoku to N-Queens in Under 20 Lines (2015)
  5. …- which is different from the program drawing insights from organically accumulated data. [1] https://github.com/Z3Prover/z3?tab=readme-ov-file [2] https://microsoft.github.io/z3guide/programming/Z3%20Python%... [3]…
    comment by abhgh · 2025-10-12 · in Let's Take Esoteric Programming Languages Seriously
  6. For what it's worth, the way 14MV does hints is probably by just throwing the board into Z3 ( https://github.com/Z3Prover/z3 ) or some other constraint solver. Microsoft has already done all the hard work for you.
    comment by npinsker · 2025-07-09 · in Making Explainable Minesweeper
  7. ▲ 3
    Z3 Theorem Prover
    story by klaussilveira · 2025-06-23 · 0 comments
  8. …with a .NET language, there is also this very useful file with examples of how to use the bindings: https://github.com/Z3Prover/z3/blob/master/examples/dotnet/P... The examples are in C#, but easy to adapt to other languages. I found them…
    comment by constructum · 2024-12-06 · in Accidentally writing a SAT solver
  9. ▲ 2
    Z3 Theorem Prover
    story by okl · 2024-10-18 · 0 comments
  10. ▲ 213
    Show HN: Allocate poker chips optimally with mixed-integer nonlinear programming
    story by jstrieb · 2024-06-04 · 69 comments
  11. https://github.com/Z3Prover/z3 Here is an actual description: https://z3prover.github.io/papers/programmingz3.html#sec-int...
    comment by phi-go · 2024-02-21 · in Planner programming blows my mind
  12. …under development and people were using linear search and not hash tables to do their lookups. Also https://github.com/Z3Prover/z3 Note “the semantic web” is both an advance and a retreat in that OWL is a subset of first order logic which…
    comment by PaulHoule · 2023-12-26 · in Ask HN: What is the current state of "logical" AI?
  13. …in the language[5]. [1] https://www.microsoft.com/en-us/research/project/code-contra... [2] https://github.com/Z3Prover/z3 [3] https://github.com/microsoft/CodeContracts [4] https://github.com/dafny-lang/dafny [5]…
    comment by Genbox · 2023-10-27 · in Lean4 helped Terence Tao discover a small bug in his recent paper
  14. …functionality, although, it uses the [0]Z3Prover tool with a nim frontend [1]DrNim for proving. [0] https://github.com/Z3Prover/z3 [1] https://nim-lang.github.io/Nim/drnim.html
    comment by janAkali · 2023-06-29 · in Programming languages going above and beyond
  15. …these problems without a capable and expressive solver. [0] https://github.com/potassco/clingo [1] https://github.com/Z3Prover/z3 [2] https://arxiv.org/abs/2210.08404 , https://dl.acm.org/doi/abs/10.5555/3571885.3571931 [3]…
    comment by tgamblin · 2023-05-26 · in Modern SAT solvers: fast, neat and underused (2018)
  16. …more robust (provided its the type you're after) than someones 700 LoC JavaScript implementation. https://github.com/Z3Prover/z3
    comment by girvo · 2022-09-15 · in The Little Prover
  17. …2: https://alloytools.org/ 3: https://www.gnu.org/software/octave/index 4: https://github.com/z3prover/z3
    comment by gjadi · 2022-06-07 · in Ask HN: When you code at work, how do you code in your time off?
  18. …a first-level standard[5]. [1] https://www.microsoft.com/en-us/research/project/code-contra... [2] https://github.com/Z3Prover/z3 [3] https://github.com/dotnet/runtime/issues/20006 [4] https://docs.microsoft.com/en-us/dotnet/csharp/nullable…
    comment by Genbox · 2022-05-29 · in Make formal verification and provably correct software practical and mainstream
  19. …by the other. [1] https://github.com/Ericsson/codechecker [2] https://clang-analyzer.llvm.org/ [3] https://github.com/Z3Prover/z3
    comment by yaantc · 2022-04-20 · in IKOS: Static analyzer for C/C++ based on the theory of Abstract Interpretation
  20. …// Start by getting Z3, a theorem prover from Microsoft, via nuget. See https://github.com/Z3Prover/z3 using Microsoft.Z3; using System; // get a solution ulong Solution(Context ctx, BoolExpr f, BitVecExpr seed) { Solver s = ctx.M
    comment by ChrisLomont · 2021-10-18 · in Cracking Random Number Generators Using Machine Learning
  21. …?)[3] if you are confused on how exactly to best approach Isabelle/HOL in your case. [0]: https://github.com/Z3Prover/z3 [1]: https://lamport.azurewebsites.net/tla/tla.html [2]: https://htdp.org/2021-5-4/Book/index.html [3]: [edit:…
    comment by namibj · 2021-10-16 · in Functional Algorithms, Verified
  22. …Z3 online version or another SMT solver that can be used online? Rise4fun is gone for good :-( https://github.com/Z3Prover/z3/issues/5472
    comment by zimmski · 2021-09-23 · in How to solve logic puzzles with SMT solvers
  23. …Examples include Google OR-tools, Microsoft Z3, etc. https://developers.google.com/optimization https://github.com/Z3Prover/z3
    comment by asah · 2021-07-20 · in Using Prolog for Sudoku Variants
  24. ▲ 1
    Z3
    story by tosh · 2021-02-13 · 0 comments
  25. You might like a Satisfiability Modulo Theories (SMT) solver such as Z3. https://github.com/Z3Prover/z3 It has bindings for other languages and is able to make some rather sophisticated arithmetical and logical deductions in an often…
    comment by schoen · 2020-02-05 · in Learn X in Y minutes Where X=Prolog
  26. This? https://github.com/z3prover/z3 What is secret about it?
    comment by ganzuul · 2020-02-03 · in A scalable photonic computer solving the subset sum problem
  27. Had to look up z3 https://github.com/Z3Prover/z3
    comment by philshem · 2019-11-15 · in Which answer in this list is the correct answer to this question? (2017)
  28. …a6))))))) And the model also becomes unsatisfiable. So 5 only seems to be the correct answer. [0] https://github.com/Z3Prover/z3 [1] https://rise4fun.com/Z3/1DMW
    comment by grubb · 2019-11-15 · in Which answer in this list is the correct answer to this question? (2017)
  29. I have used the Z3 solver( https://github.com/Z3Prover/z3 ) to optimize a job scheduling problem. Roughly, I have ~20k jobs, defined by N tasks (~1-50). A job is complete only if M tasks (typically 2-3) per job are done. Every task takes…
    comment by silly_giraffe · 2019-09-29 · in Modern SAT solvers: fast, neat and underused
  30. ▲ 137
    The Z3 Theorem Prover
    story by ____Sash---701_ · 2019-06-01 · 29 comments
  31. …synthesis: https://medium.com/@vidiborskiy/software-writes-software-pro... [3] Z3 Theorem Prover: https://github.com/Z3Prover/z3 [4] Solidity AST: https://github.com/ethereum/solidity/blob/develop/libsolidit... [5] Solidity smart…
    comment by saurabh20n · 2019-03-01 · in Ask HN: Who is hiring? (March 2019)
  32. Found these links helpful: https://en.m.wikipedia.org/wiki/Satisfiability_modulo_theori... https://github.com/Z3Prover/z3/wiki/Slides Appears to be useful for static analysis and verification of a program.
    comment by patsplat · 2019-02-06 · in Programming the Z3 SMT solver
  33. …synthesis: https://medium.com/@vidiborskiy/software-writes-software-pro... [3] Z3 Theorem Prover: https://github.com/Z3Prover/z3 [4] Solidity AST: https://github.com/ethereum/solidity/blob/develop/libsolidit... [5] Solidity smart…
    comment by saurabh20n · 2019-02-01 · in Ask HN: Who is hiring? (February 2019)
  34. …https://fstar-lang.org/tutorial - see e.g. section 3 "First proofs about functions on integers" [4] https://github.com/Z3Prover/z3
    comment by tomp · 2018-12-18 · in Dependent Haskell
  35. …last year, so an SMT solver is validating all your S3 security policies for public access!) [3]: https://github.com/Z3Prover/z3
    comment by KirinDave · 2018-11-09 · in Optimal Shard Placement in a Petabyte Scale Elasticsearch Cluster
  36. ▲ 3
    Z3
    story by tosh · 2018-10-30 · 0 comments
  37. ▲ 6
    Z3
    story by tosh · 2018-08-17 · 0 comments
  38. ▲ 1
    Z3
    story by tosh · 2018-05-22 · 0 comments
  39. ▲ 3
    Microsoft: The Z3 Theorem Prover
    story by tosh · 2017-05-18 · 0 comments
  40. …as simple as `pip install` and requires a lengthy build/compilation. Well worth the effort, though. https://github.com/Z3Prover/z3 https://github.com/Z3Prover/z3/issues/288
    comment by Cieplak · 2017-05-18 · in Transform Data by Example [video]
  41. what about this? https://github.com/Z3Prover/z3 Is it comparable with prolog or just a subset of prolog?
    comment by est · 2017-04-06 · in The Power of Prolog
  42. …more concrete. Feel free to shoot me an email if you like to talk more about formal methods :) [0]: https://github.com/Z3Prover/z3 [1]: http://www.event-b.org/
    comment by aban · 2016-11-19 · in Why Don't Computer Scientists Learn Math?
  43. Other people are already flooding you with counterexamples, but I'll add to the pileup: Z3 ( https://github.com/Z3Prover/z3 ) is the Satisfiability Modulo Theories (SMT) solver to use. It is such a quality piece of software and it's…
    comment by ulber · 2016-09-15 · in Microsoft is now the leading company for open source contributions on GitHub
  44. ▲ 2
    Show HN: The Z3 theorem can now be built using CMake
    story by delcypher · 2016-03-07 · 0 comments
  45. …One of the driver validation tools makes use of the Z3 theorem prover as its verification engine https://github.com/z3prover/z3/wiki http://research.microsoft.com/en-us/um/redmond/projects/z3/s... https://msdn.microsoft.com/en-us/library/wi…
    comment by pjmlp · 2015-09-30 · in Critique of Microkernel Architectures – Is Linus Right? (2004) [pdf]
  46. …expressed in predicate logic accepted by Z3. You can do all sorts of neat stuff then; check out https://github.com/Z3Prover/z3/wiki/Publications Some general examples: * Does firewall 1 accept a subset of the packets accepted by firewall…
    comment by ahelwer · 2015-05-18 · in Solving a Crackme using Z3: Theorem Prover
  47. ▲ 1
    Change of Z3 license
    story by pascal_cuoq · 2015-03-26 · 0 comments
  48. ▲ 304
    The Z3 Theorem Prover released under MIT license
    story by dahlia · 2015-03-26 · 66 comments