Issues

• fp.roundToIntegral rounds the FP(2,3) subnormal 1/4 to 1 in nearest modes

  Z3Prover/z3#11139 · Filter by author vera-rubin opened on Oct 11, 2026

• [code-simplifier] Use existing match_equiv helper instead of repeating its definition

  agentic-workflowsautomationcode-qualityrefactoring
  Z3Prover/z3#11138 · Filter by author github-actions opened on Oct 11, 2026

• MBQI cannot refute hypotheses over function (array) variables: counterexample arrays become lambdas the array theory gives up on

  Z3Prover/z3#11093 · Filter by author etiennejf opened on Oct 7, 2026
  1

• Interest in native QF_FF support, with independently checked certificates

  Z3Prover/z3#10994 · Filter by author RSoulatIOHK opened on Oct 1, 2026
  4

• Performance regression 4.13.3 -> 4.15.0 and later: quantified UF+LIA query 43x slower (then unsolvable) with smt.case_split 3

  Z3Prover/z3#10863 · Filter by author gebner opened on Sep 19, 2026
  

• Could we have a new release on nuget.org?

  Z3Prover/z3#10711 · Filter by author HowardvanRooijen opened on Sep 1, 2026
  2

• Consolidated invalid model bugs

  Z3Prover/z3#9319 · Filter by author lmaltsis opened on Apr 16, 2026
  12

• Is there a way to combine QF_BV and QF_IDL?

  Z3Prover/z3#8940 · Filter by author ThomasHaas opened on Mar 11, 2026
  7

• Incorrect model with :produce-proofs true involving String Theory and UF

  Z3Prover/z3#8194 · Filter by author wingsyuyi-satori opened on Jan 14, 2026
  4

  

• Unsat only with unnecessary asserts, else unknown

  Floats
  Z3Prover/z3#8052 · Filter by author ThomasMayerl opened on Nov 28, 2025
  

• Infinite loop/performance regression in Z3 4.15.3

  Z3Prover/z3#7991 · Filter by author rod-chapman opened on Oct 18, 2025
  15

• Observe both compute and memory regression when upgrade to 4.15.3 from 4.14.1

  string
  Z3Prover/z3#7800 · Filter by author smoy opened on Aug 19, 2025
  2

• Memory and time blow-up with z3 4.15.2

  Z3Prover/z3#7735 · Filter by author rod-chapman opened on Jul 15, 2025
  5

• Performance regression when using Fixedpoint solver (from 4.13.2 to 4.14.1)

  Horn
  Z3Prover/z3#7632 · Filter by author KihongHeo opened on Apr 24, 2025
  2

  

• PartialOrder hangs when reasoning about bottom element

  Z3Prover/z3#7592 · Filter by author fritzo opened on Mar 20, 2025
  1

• Slow unsat multiplication overflow solving

  Z3Prover/z3#7526 · Filter by author alph6 opened on Jan 23, 2025
  3

• Spacer: Timeout with simple array example

  Horn
  Z3Prover/z3#7425 · Filter by author mmsbrggr opened on Oct 18, 2024
  5

• Alternative solutions for z3-solver without using SharedArrayBuffer or COOP/COEP headers

  Z3Prover/z3#7238 · Filter by author MargeKh opened on May 29, 2024
  1

  

• TransitiveClosure + Quantifiers extremely slow

  Z3Prover/z3#7167 · Filter by author tzlils opened on Mar 16, 2024
  1

• [consolidated] hang on small instances (string, bit-vector)

  Z3Prover/z3#7164 · Filter by author zhendongsu opened on Mar 14, 2024
  11

• Unknown when working with String Sequences

  string
  Z3Prover/z3#7151 · Filter by author manojlds opened on Mar 6, 2024

• Finite sets

  Z3Prover/z3#6788 · Filter by author shazqadeer opened on Jun 27, 2023
  3

• Performance regression issue on string

  string
  Z3Prover/z3#6668 · Filter by author merlinsun opened on Apr 3, 2023

• Issues with models of Horn clauses

  Horn
  Z3Prover/z3#5920 · Filter by author NikolajBjorner opened on Mar 23, 2022
  4

• Performance regression from 4.8.7.0 to 4.8.8.0 and all later versions.

  string
  Z3Prover/z3#5763 · Filter by author vrthra opened on Jan 10, 2022