13 Pull requests merged by 6 people

• Parallel solving

  #7771 merged Aug 11, 2025

• Parallel solving

  #7769 merged Aug 10, 2025

• Finest factors

  #7768 merged Aug 8, 2025

• 4015

  #7761 merged Aug 7, 2025

• fix #7603: race condition in Ctrl-C handling

  #7755 merged Aug 6, 2025

• Parallel solving

  #7759 merged Aug 6, 2025

• Parallel solving

  #7758 merged Aug 5, 2025

• Add support for Algebraic Datatypes in JavaScript/TypeScript bindings

  #7734 merged Aug 5, 2025

• Parallel solving

  #7756 merged Aug 4, 2025

• fixed-size min-heap for tracking top-k literals

  #7752 merged Jul 29, 2025

• Better error message for FreshConst

  #7748 merged Jul 27, 2025

• very basic setup for new parallel solving

  #7741 merged Jul 23, 2025

• debug : Add support for selecting LLDB via invoke on macOS

  #7726 merged Jul 12, 2025

1 Pull request opened by 1 person

• Add .github/copilot-instructions.md with comprehensive Z3 development guide

  #7766 opened Aug 8, 2025

37 Issues closed by 3 people

• slow check-sat with Array Int (Option (Set Int))

  #7770 closed Aug 10, 2025

• Failed to find the min value of a simple parabola

  #7767 closed Aug 9, 2025

• remove z3str3 theory solver and dependencies that are only used by z3str3

  #7763 closed Aug 8, 2025

• Memory leaks about smt.string_solver

  #7342 closed Aug 8, 2025

• Unsoundness issue with smt.string_solver=z3str3

  #6159 closed Aug 8, 2025

• [consolidate] (smt.string_solver=z3str3) Refutation Soundness issue on String Theory

  #6144 closed Aug 8, 2025

• (smt.string_solver=z3str3) Invalid model issue

  #6080 closed Aug 8, 2025

• Unexpected behaviour for z3_str3_4.8.14

  #5873 closed Aug 8, 2025

• (smt.string_solver=z3str3) str.is_digit function issue

  #6134 closed Aug 8, 2025

• A timeout test case for z3str3

  #5266 closed Aug 8, 2025

• Non-Terminating Z3Str3 from z3-4.8.9-x64-ubuntu-16.04

  #5673 closed Aug 8, 2025

• A QF_S test case make z3 unable to return results

  #5196 closed Aug 8, 2025

• performance regression problems

  #4591 closed Aug 8, 2025

• (z3str3, smt.phase_selection=1) Soundness bug on QF_S formula with str.at and str.substr

  #4417 closed Aug 8, 2025

• (z3str3) Soundness bug on QF_S formula with re.comp str.to_re

  #4410 closed Aug 8, 2025

• (z3str3, dom-simplify, ctx-solver-simplify, smt.str.fixed_length_refinement) Assertion violation at ../src/smt/theory_str_mc.cpp Line: 1162

  #4353 closed Aug 8, 2025

• z3str3 invalid model on QF_S formula with distinct str.replace

  #3077 closed Aug 8, 2025

• z3str3 invalid model on QF_SLIA formula

  #3069 closed Aug 8, 2025

• [String] Different satisfiability result with and without smt.string_solver=z3str3

  #1379 closed Aug 8, 2025

• Possible bug in z3str3 (?)

  #1678 closed Aug 8, 2025

• [String] A difficult problem or a bug

  #1367 closed Aug 8, 2025

• Incorrect result from z3str3

  #7754 closed Aug 8, 2025

• Z3 Context Thread Safety Question

  #7760 closed Aug 7, 2025

• Crashes in a multithreaded program on Ctrl-C

  #7603 closed Aug 6, 2025

• regression test regression on Mac

  #7757 closed Aug 5, 2025

• Add support for Algebraic Datatypes in js bindings

  #7621 closed Aug 5, 2025

• Better error message for FreshConst

  #7749 closed Aug 5, 2025

• Performance regression in 4.15.1 for bitvector rotations

  #7750 closed Jul 28, 2025

• get-value sometimes returns a quantified expression

  #7743 closed Jul 26, 2025

• Common Subexpression prevents efficient solving

  #7739 closed Jul 26, 2025

• Unexpected unknown Result When Using 'elim-uncnstr' in Z3

  #7742 closed Jul 26, 2025

• Incorrect SAT result for string query

  #7745 closed Jul 26, 2025

• ASSERTION VIOLATION

  #7736 closed Jul 15, 2025

• Why is there a generic parameter in `Constructor<R>` class in Z3 Java API?

  #7731 closed Jul 12, 2025

• Question about Z3's Parallel Mode Trigger Conditions for Floating-Point Problems

  #7727 closed Jul 12, 2025

• Z3 crashed CPython when proof is missing

  #7725 closed Jul 12, 2025

• zip archive that contains sources should have SHA signatures on nightly and release builds

  #7728 closed Jul 12, 2025

6 Issues opened by 6 people

• ✨Set up Copilot instructions

  #7765 opened Aug 8, 2025

• Simple divisibility problem diverges

  #7753 opened Aug 1, 2025

• PyPi doesn't seem to have the most recent release 4.15.2

  #7746 opened Jul 25, 2025

• Z3 Rust Guide

  #7744 opened Jul 25, 2025

• Assert stuck indefinitely when using recursive functions

  #7738 opened Jul 17, 2025

• Memory and time blow-up with z3 4.15.2

  #7735 opened Jul 15, 2025

4 Unresolved conversations

Sometimes conversations happen on old items that aren’t yet closed. Here is a list of all the Issues and Pull Requests with unresolved conversations.

• Spacer returns `sat` instead of expected `unsat`, and fails model validation on a specific input

  #7730 commented on Jul 12, 2025 • 0 new comments

• JS (High-level) - Eventual memory corruption

  #7723 commented on Jul 12, 2025 • 0 new comments

• Z3 4.8.14 concludes input file is `unsat`, but loops forever on 4.15.1

  #7700 commented on Jul 14, 2025 • 0 new comments

• regression with arith.solver=6

  #7502 commented on Jul 16, 2025 • 0 new comments