Search results

[zipt-review] ZIPT Code Review: Recursive traversal and missing loop-merging in euf_sgraph/euf_seq_plugin (c3 branch)

automated

code-quality

string-solver

Status: Open.

#9237 In Z3Prover/z3;

· github-actions opened on Apr 6, 2026

Rec fun redefinition assertion failure

Status: Open.

#9234 In Z3Prover/z3;

· aleksisch opened on Apr 5, 2026

[tactic-to-simplifier] Convert tactic 'normalize-bounds' to a simplifier

enhancement

refactoring

tactic-to-simplifier

Status: Open.

#9231 In Z3Prover/z3;

· github-actions opened on Apr 4, 2026

[tactic-to-simplifier] Convert tactic 'nnf' to a simplifier

enhancement

refactoring

tactic-to-simplifier

Status: Open.

#9229 In Z3Prover/z3;

· github-actions opened on Apr 4, 2026

[tactic-to-simplifier] Convert tactic 'fpa2bv' to a simplifier

enhancement

refactoring

tactic-to-simplifier

Status: Open.

#9230 In Z3Prover/z3;

· github-actions opened on Apr 4, 2026

Some invalidation logic is missing.

Status: Open.

#9227 In Z3Prover/z3;

· MAKMED1337 opened on Apr 4, 2026

[aw] Ostrich Benchmark: Z3 c3 branch vs ZIPT failed

agentic-workflows

Status: Open.

#9226 In Z3Prover/z3;

· github-actions opened on Apr 4, 2026

[aw] ZIPT String Solver Benchmark failed

agentic-workflows

Status: Open.

#9225 In Z3Prover/z3;

· github-actions opened on Apr 4, 2026

[aw] Clang Static Analyzer (CSA) Report failed

agentic-workflows

Status: Open.

#9224 In Z3Prover/z3;

· github-actions opened on Apr 4, 2026

push/pop scopes affect performance of subsequent proofs

Status: Open.

#9220 In Z3Prover/z3;

· davedets opened on Apr 3, 2026

Regression in a constant-folding example

Status: Open.

#9171 In Z3Prover/z3;

· LeventErkok opened on Mar 30, 2026

Zero-divisor rem collapses to mod, causing false UNSAT

Status: Open.

#9140 In Z3Prover/z3;

· christos-spearbit opened on Mar 26, 2026