Search results

[Conventions] Refactor theory_bv to use structured bindings for disequality watch pairs

automated

code-quality

Status: Open.

#8408 In Z3Prover/z3;

· github-actions opened on Jan 28, 2026

[Conventions] Refactor SAT components to use structured bindings for literal and expression pairs

automated

code-quality

Status: Open.

#8407 In Z3Prover/z3;

· github-actions opened on Jan 28, 2026

[Conventions] Refactor dyn_ack to use structured bindings for app pairs and triples

automated

code-quality

Status: Open.

#8406 In Z3Prover/z3;

· github-actions opened on Jan 28, 2026

Soundness issue in Real (seemingly unrelated to Float)

Status: Open.

#8397 In Z3Prover/z3;

· wintered opened on Jan 27, 2026

[Conventions] Refactor sat_solver to use structured bindings for priority and literal pairs

automated

code-quality

Status: Open.

#8396 In Z3Prover/z3;

· github-actions opened on Jan 27, 2026

[Conventions] Refactor euf_completion to use structured bindings for closure and proof pairs

automated

code-quality

Status: Open.

#8395 In Z3Prover/z3;

· github-actions opened on Jan 27, 2026

[Conventions] Refactor bound_manager to use structured bindings for limit pairs

automated

code-quality

Status: Open.

#8394 In Z3Prover/z3;

· github-actions opened on Jan 27, 2026

[Conventions] Refactor theory_array_base to use structured bindings for enode pairs

automated

code-quality

Status: Open.

#8393 In Z3Prover/z3;

· github-actions opened on Jan 27, 2026

[Conventions] Refactor der.cpp to use structured bindings for expression/index pairs

automated

code-quality

Status: Open.

#8392 In Z3Prover/z3;

· github-actions opened on Jan 27, 2026

Z3 segfaults instead of erroring out when passing the wrong type parameters to Z3.Datatype.mk_sort_ref_p

Status: Open.

#8376 In Z3Prover/z3;

· mben-romdhane opened on Jan 27, 2026

Expose an API function to allow defining polymorphic recursive datatypes

Status: Open.

#8375 In Z3Prover/z3;

· mben-romdhane opened on Jan 27, 2026

[Conventions] Refactor factor_rewriter to use structured bindings for expr/sign pairs

automated

code-quality

Status: Open.

#8370 In Z3Prover/z3;

· github-actions opened on Jan 27, 2026