Search results

Unbounded loop proof causes non-termination and giant SMT file

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

aws-high

bug

SMT Backend Interface

Status: Open.

#8505 In diffblue/cbmc;

· rod-chapman opened on Nov 14, 2024

Spurious failure with SMT2 backend

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

aws-medium

SMT Backend Interface

Status: Open.

#7689 In diffblue/cbmc;

· zhassan-aws opened on Apr 25, 2023

Incremental SMT back-end occasionally fails regression tests

CI

SMT Backend Interface

Status: Open.

#7549 In diffblue/cbmc;

· tautschnig opened on Feb 16, 2023

sqrtf appears to be non-deterministic and throwing spurious verification failures

bug

C Front End

SMT Backend Interface

Status: Open.

#6563 In diffblue/cbmc;

· sree314 opened on Jan 8, 2022

MathSAT SMT2 not working

SMT Backend Interface

Status: Open.

#6263 In diffblue/cbmc;

· xXMarkuski opened on Jul 30, 2021

remove encoding of arrays of bools into bitvector

SMT Backend Interface

Status: Open (in progress).

diffblue/cbmcnumber 6206

#6206 In diffblue/cbmc;

· kroening opened on Jun 28, 2021

[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

smt2_solver gives incorrect result on multidimensional arrays

Array Theory

bug

SMT Backend Interface

Status: Open.

#4749 In diffblue/cbmc;

· romainbrenguier opened on Jun 4, 2019

[RFC] CPROVER should use a reproducible resource limit rather than a time-out

feature request

SMT Backend Interface

Status: Open.

#4452 In diffblue/cbmc;

· martin-cs opened on Mar 28, 2019