Search results

Using up-to-date version of CBMC

Status: Open.

#182 In diffblue/2ls;

· jparsert opened on Sep 4, 2025

Exception is thrown (Invariant check failed) when trying to verify a program from SV-COMP.

Status: Open.

#181 In diffblue/2ls;

· jparsert opened on Jul 10, 2025

Inconclusive Termination of rather simple float loop

Status: Open.

#180 In diffblue/2ls;

· cloerkes opened on Jul 10, 2025

An Unknown Instance of Loop Invariant?

Status: Open.

#178 In diffblue/2ls;

· sjxer723 opened on Apr 23, 2024

Is kInduction imprecise?

Status: Open.

#177 In diffblue/2ls;

· Novak756 opened on Apr 19, 2024

Support array memcpy

Status: Open.

#160 In diffblue/2ls;

· viktormalik opened on Jan 14, 2022

Assertion `!(pointer && arithmetics)' failed

Status: Open.

#159 In diffblue/2ls;

· blizzard4591 opened on Jan 5, 2022

Large arrays cause false positives

Status: Open.

#135 In diffblue/2ls;

· viktormalik opened on Nov 26, 2018

Heap-zones: fixing one variable in a difference row causes the other one to be fixed, too.

Status: Open.

#131 In diffblue/2ls;

· viktormalik opened on Oct 15, 2018

False negative with k-Induction and incremental BMC

Status: Open.

#123 In diffblue/2ls;

· lu-w opened on Aug 21, 2018

Implement stronger shape domain.

Status: Open.

#121 In diffblue/2ls;

· viktormalik opened on Aug 3, 2018

Extend non-termination analysis to recursion

enhancement

task

Status: Open.

#118 In diffblue/2ls;

· peterschrammel opened on Dec 30, 2017