Project

General

Profile

Bug #5016

when increasing bitwidth, wrong result is reported

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 8 --unwind 10 ~/dev/hi-bench/challenge-bench/sv-comp16/c/bitvector/num_conversion_2_true-unreach-call.c

Refinement successful
VERIFICATION SUCCESSFUL
----------------------
BUT when running with bw 32 it becomes SAT!!!!!:

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

Weak statement encodings (33) found
  Weak statement encodings (1) found

Obtained counter-examples are refined
(34 / 35 expressions bit-blasted)

VERIFICATION FAILED

History

#1 Updated by Sepideh Asadi about 7 years ago

CBMC is UNSAT.

#2 Updated by Karine Even Mendoza about 7 years ago

bitwidth 16 - SAT
bitwidth 8 - UNSAT

#3 Updated by Karine Even Mendoza almost 7 years ago

  • Assignee set to Antti Hyvärinen

The encoding (SMT + SSA parsing) is the same for 8 or 16 bits.
But the same encoding returns different results from opensmt when bitwidth is 8 or 16.

Anyidea?

#4 Updated by Karine Even Mendoza almost 7 years ago

  • Status changed from New to Feedback
  • Assignee changed from Antti Hyvärinen to Sepideh Asadi
  • % Done changed from 0 to 90

Add new functionality to support this case: --type-byte-constraints.
Works now

#5 Updated by Karine Even Mendoza almost 7 years ago

  • Status changed from Feedback to Closed

Also available in: Atom PDF