Bug #5014
bug in /sv-comp16/c/bitvector/
Start date:
20/04/2017
Due date:
% Done:
90%
Estimated time:
Description
/hifrog --claim 1 --bitwidth 32 --unwind 40 --theoref ~/dev/hi-bench/challenge-bench/sv-comp16/c/bitvector/interleave_bits_true-unreach-call.c
It is SAT, but should be UNSAT!
History
#1 Updated by Karine Even Mendoza about 7 years ago
Doesn't refine 2 last claims, why?
#2 Updated by Karine Even Mendoza almost 7 years ago
- Status changed from New to Feedback
- Assignee set to Sepideh Asadi
- % Done changed from 0 to 90
Add type-byte-constraints (option 2 to solve this issue).
#3 Updated by Karine Even Mendoza almost 7 years ago
- Status changed from Feedback to Closed