List view

yices_new_uninterpreted_term does not produce an uninterpreted term

Status: Open.

#414 In SRI-CSL/yices2;

· disteph opened on Nov 1, 2022

fixes #414

Status: Draft (not ready).

SRI-CSL/yices2number 590

#590 In SRI-CSL/yices2;

· ahmed-irfan opened on Jul 12, 2025

MCSAT: add support for tuples (incl. nested with function types); blasts tuples in input constraints + reconstitutes them in models and interpolants

Status: Open (in progress).

SRI-CSL/yices2number 606

#606 In SRI-CSL/yices2;

· disteph opened on Mar 2, 2026

Feature request: making delegates available when solving from a Yices context

Status: Open.

#453 In SRI-CSL/yices2;

· disteph opened on Aug 3, 2023

QF_BV context delegates (#453): config/param selection, incremental state, assumptions, and delegate regressions

Status: Open (in progress).

SRI-CSL/yices2number 607

#607 In SRI-CSL/yices2;

· disteph opened on Mar 3, 2026

Wrap MCSAT as a Nelson-Oppen theory solver in CDCL(T) architecture

Status: Draft (not ready).

SRI-CSL/yices2number 611

#611 In SRI-CSL/yices2;

· disteph opened on Mar 10, 2026