All issues

Search results

feat: Add FiniteSet sort and operations (Z3 5.0)

Status: Open.

Feature

#576 In prove-rs/z3.rs;

· toolCHAINZ opened on Jul 25, 2026

Z3 5.0.0 is not the default gh-release release

Status: Open.

#569 In prove-rs/z3.rs;

· ChaiTRex opened on Jul 17, 2026

fix: BV::fresh_const args

Status: Open.

#561 In prove-rs/z3.rs;

· toolCHAINZ opened on Jun 8, 2026

A more direct binding for z3

Status: Open.

#560 In prove-rs/z3.rs;

· HuStmpHrrr opened on Apr 20, 2026

feat: Expose global parameter descriptors

Status: Open.

Feature

#548 In prove-rs/z3.rs;

· toolCHAINZ opened on Mar 21, 2026

feat: Add function-level substitution API (substitute_funs)

Status: Open.

Feature

#547 In prove-rs/z3.rs;

· toolCHAINZ opened on Mar 21, 2026

feat: Add AST introspection APIs (depth, is_ground, quantifier ids)

Status: Open.

Feature

#546 In prove-rs/z3.rs;

· toolCHAINZ opened on Mar 21, 2026

feat: Add QE model projection with witness

Status: Open.

Feature

#545 In prove-rs/z3.rs;

· toolCHAINZ opened on Mar 21, 2026

feat: Add extended Optimize APIs (model callback, initial values)

Status: Open.

Feature

#544 In prove-rs/z3.rs;

· toolCHAINZ opened on Mar 21, 2026

feat: Add array sort arity and multi-dimensional domain introspection

Status: Open.

Feature

#543 In prove-rs/z3.rs;

· toolCHAINZ opened on Mar 21, 2026

feat: Add missing arithmetic and expression APIs (abs, divides, real_int64, binary string, bit2bool, fpa_is_numeral)

Status: Open.

Feature

#542 In prove-rs/z3.rs;

· toolCHAINZ opened on Mar 21, 2026

feat: Add algebraic number polynomial and root-index extraction APIs

Status: Open.

Feature

#541 In prove-rs/z3.rs;

· toolCHAINZ opened on Mar 21, 2026