Search results

Parallel Solving

Status: Open.

#347 In prove-rs/z3.rs;

· lolpro11 opened on May 16, 2025

Question: Lifetimes on <code>translate</code>

Status: Open.

#346 In prove-rs/z3.rs;

· toolCHAINZ opened on Apr 14, 2025

<code>NotExist("/opt/homebrew/Cellar/z3/4.13.0/include/z3.h")</code> error on macos

Status: Open.

#345 In prove-rs/z3.rs;

· cdstanford opened on Apr 13, 2025

Retrieve non-unsat proof attempts via on_clause callback

Status: Open.

#343 In prove-rs/z3.rs;

· LeskovarLukas opened on Apr 6, 2025

cmake 4.0.0 release breaks build

Status: Open.

#342 In prove-rs/z3.rs;

· scott-wyatt opened on Apr 1, 2025

Creating a tactic from an invalid tactic results in a SIGSEGV

Status: Open.

#338 In prove-rs/z3.rs;

· bakerk98 opened on Mar 21, 2025

Probleam in Rust version "mul" and "mul_towards_zero" function

Status: Open.

#335 In prove-rs/z3.rs;

· FoxMakarov opened on Jan 17, 2025

Should assert take &amp;mut self, instead of &amp;self?

Status: Open.

#334 In prove-rs/z3.rs;

· the-ssd opened on Jan 5, 2025

Missing API for BitVectors

Status: Open.

#332 In prove-rs/z3.rs;

· the-ssd opened on Jan 5, 2025

Unexpected behavior when trying to minimize bitvector

Status: Open.

#331 In prove-rs/z3.rs;

· danielrainer opened on Dec 17, 2024

Missing Exposure of Z3_context and Z3_sort in Recent Z3 Crate Versions

Status: Open.

#327 In prove-rs/z3.rs;

· zhristophe opened on Nov 29, 2024

High-level bindings to create quantifiers with additional attributes

Status: Open.

#325 In prove-rs/z3.rs;

· ole-thoeb opened on Nov 28, 2024