Project

General

Profile

Bug #5012

byte_add_1_true-unreach-call.c

Added by Sepideh Asadi about 7 years ago. Updated about 7 years ago.

Status:
Closed
Priority:
Normal
Assignee:
-
Start date:
19/04/2017
Due date:
% Done:

100%

Estimated time:

Description

./hifrog --claim 1 --unwind 5 --theoref --bitwidth 32 byte_add_1_true-unreach-call.c

with --unwind 10 is killed

while CBMC verifies this example in less than second

We need more optimization

History

#1 Updated by Karine Even Mendoza about 7 years ago

  • Status changed from New to Closed
  • % Done changed from 0 to 100

Works fine, but returns the wrong results, added it to another issue which refers to this problem

Also available in: Atom PDF