Search results

RuntimeError when trying out portfolio example with z3 and cvc5

Status: Open.

#826 In pysmt/pysmt;

· R-Bose opened on Jan 29, 2026

Can not use QF_UFNIA

Status: Open.

#824 In pysmt/pysmt;

· nafur opened on Dec 18, 2025

bdd solver.get_model() returns assignment to variables removed by quantifier elimination

Status: Open.

#823 In pysmt/pysmt;

· AlbertoSambrotta opened on Dec 17, 2025

pysmt-install does not work on python 3.12

Status: Open.

#822 In pysmt/pysmt;

· njsyw1997 opened on Sep 29, 2025

Boolector Archived: Please Consider Supporting Bitwuzla as Backend

Status: Open.

#817 In pysmt/pysmt;

· hadipourh opened on Jul 29, 2025

BV logic and get_logic_by_name()/get_logic()

Status: Open.

#811 In pysmt/pysmt;

· jortvanleenen opened on May 21, 2025

Mathsat does not support arrays with boolean Type

Status: Open.

#807 In pysmt/pysmt;

· Framba-Luca opened on May 19, 2025

Enhance type‐narrowing support via TypeGuard utilities

Status: Open.

#804 In pysmt/pysmt;

· JanTomassi opened on May 18, 2025

MathSAT5Solver all_sat method crashes with SIGSEGV

Status: Open.

#786 In pysmt/pysmt;

· andreastedile opened on Dec 6, 2024

Any plans for Floating point support?

Status: Open.

#783 In pysmt/pysmt;

· bavalpey opened on Aug 13, 2024

Add type-hints to pysmt code

Status: Open.

#780 In pysmt/pysmt;

· enmag opened on Jul 17, 2024

Unable to use UFNRA

Status: Open.

#777 In pysmt/pysmt;

· MikolasJanota opened on Jul 13, 2024