Search results

Printing SMT file with Z3 backend crashes CBMC

awsBugs or features of importance to AWS CBMC usersBugs or features of importance to AWS CBMC users

bug

Solvers

Status: Open.

Bug

#8637 In diffblue/cbmc;

· rod-chapman opened on May 11, 2025

Quantifier instantiation via simplistic E-matching

Solvers

Status: Open (in progress).

diffblue/cbmcnumber 8224

#8224 In diffblue/cbmc;

· tautschnig opened on Feb 27, 2024

double-width pointer encoding

Solvers

Status: Draft (not ready).

diffblue/cbmcnumber 6836

#6836 In diffblue/cbmc;

· kroening opened on Apr 29, 2022

[RFC] SMT Plan

cleanup

documentation

RFCRequest for commentRequest for comment

SMT Backend Interface

Solvers

Status: Open.

#6134 In diffblue/cbmc;

· TGWDB opened on May 21, 2021

Pointer encoding limits address space to 24bits for ILP32

enhancement

pending merge

Solvers

Status: Open.

#94 In diffblue/cbmc;

· peterschrammel opened on May 20, 2016