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

__CPROVER_assume behaviour different --float-overflow-check in CBMC 5.48 and CBMC 6.4

bug

Symbolic Execution

Status: Open.

#8633 In diffblue/cbmc;

· sree314 opened on Apr 29, 2025

Buggy handling of assignments involving pointer dereference

bug

Status: Open.

#8610 In diffblue/cbmc;

· nianzelee opened on Mar 31, 2025

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

Aliasing pre-condition not processed correctly if <code>is_fresh</code> clause it not standalone

bug

pending merge

soundnessSoundness bug? Review and add "aws" if it is, or remove "soundness" if it isn't.Soundness bug? Review and add "aws" if it is, or remove "soundness" if it isn't.

Status: Open.

#8492 In diffblue/cbmc;

· hanno-becker opened on Nov 4, 2024

CBMC crash if CPROVER_loop_entry is used inside an assertion inside a loop

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

bug

Status: Open.

#8453 In diffblue/cbmc;

· rod-chapman opened on Sep 13, 2024

scripts/parallel-properties.py mis-reports subprocess ABORT as TIMEOUT

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

bug

Status: Open.

#8452 In diffblue/cbmc;

· rod-chapman opened on Sep 13, 2024

CBMC wavefront does not terminate on simple decreases clause in loop

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

blocker

bug

Status: Open.

#8301 In diffblue/cbmc;

· rod-chapman opened on May 21, 2024

CBMC 5.95.1 reporting wrong line number if assertion is long

bug

Status: Open.

#8257 In diffblue/cbmc;

· christina1993 opened on Apr 9, 2024

<code>--nondet-static-exclude</code> silently fails

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

aws-high

bug

Status: Open.

#8225 In diffblue/cbmc;

· feliperodri opened on Mar 1, 2024

Shadow memory does not currently work on big-endian architectures

bug

Status: Open.

#8207 In diffblue/cbmc;

· tautschnig opened on Feb 16, 2024

Wrong linkage of global variables annotated with __attribute__((section))

bug

C Front End

Status: Open.

#8127 In diffblue/cbmc;

· cesaro opened on Dec 19, 2023