Project

General

Profile

Bug #5015

SAT is reported instead of UNSAT

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

Status:
Closed
Priority:
Normal
Assignee:
Sepideh Asadi
Start date:
20/04/2017
Due date:
% Done:

90%

Estimated time:

Description

/hifrog --claim 1 --theoref --bitwidth 16 --unwind 10 ~/dev/hi-bench/challenge-bench/sv-comp16/c/bitvector/gcd_1_true-unreach-call.c

Weak statement encodings (61) found
  Weak statement encodings (2) found

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

VERIFICATION FAILED
TOTAL TIME FOR CHECKING THIS CLAIM: 199.9
#X: Done

History

#1 Updated by Karine Even Mendoza about 7 years ago

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

#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

#3 Updated by Karine Even Mendoza almost 7 years ago

  • Status changed from Feedback to Closed

Also available in: Atom PDF