Project

General

Profile

Bug #5009

Theoref BUG: wrong result after refinement

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

Status:
Closed
Priority:
Normal
Assignee:
Antti Hyvärinen
Start date:
16/04/2017
Due date:
% Done:

0%

Estimated time:

Description

/hifrog --claim 1 --theoref --no-itp --unwind 10 ~/hi-bench/challenge-bench/sv-comp16/c/busybox-1.22.0/sync_true-unreach-call.c

The correct result should be UNSAT but it is returned:

Weak statement encodings (11) found

Obtained counter-examples are refined
(11 / 14 expressions bit-blasted)
ASSERTION DOES NOT HOLD

VERIFICATION FAILED
TOTAL TIME FOR CHECKING THIS CLAIM: 2.586

Screen Shot 2017-04-16 at 12.15.10.png (257 KB) Screen Shot 2017-04-16 at 12.15.10.png Sepideh Asadi, 16/04/2017 12:16

History

#1 Updated by Karine Even Mendoza about 7 years ago

  • Status changed from New to Feedback
  • Assignee set to Antti Hyvärinen

/hi-bench/challenge-bench/sv-comp16/c/busybox-1.22.0/sync_true-unreach-call.c:
Reason: (Cannot refine due to 22 unsupported operators;e.g., pointer)
It works with logic prop, so there is no bug in the flow.

Antti, can we add pointer support?

#2 Updated by Karine Even Mendoza about 7 years ago

  • Status changed from Feedback to Closed

Feature postponed for next coding task - reopend when start encoding

Also available in: Atom PDF