Project

General

Profile

Bug #4998

bug in QF_BOOL: wrong result for prop in benchs in directrory ntdrivers-simplified

Added by Sepideh Asadi over 2 years ago. Updated about 2 years ago.

Status:
Feedback
Priority:
Normal
Start date:
12/04/2017
Due date:
% Done:

10%

Estimated time:

Description

/hifrog --claim 1 --logic prop --bitwidth 8 --unwind 1 ~/hi-bench/challenge-bench/sv-comp16/c/ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-termination.cil.c

VERIFICATION FAILED

wrong result! because claim 1 should hold

History

#1 Updated by Karine Even Mendoza over 2 years ago

KE: can be long time bug, as the old funfrof crashes,

XXX=============================================================================
XXX Partition: 4 (ass_in_subtree: 0) - c::stub_driver_init (loc: 101, SUM)
evolcheck: sat/cnf.cpp:675: bool cnft::process_clause(const bvt&, bvt&): Assertion `l.var_no()!=literalt::unused_var_no()' failed.
Aborted (core dumped)
karinek@karinek-VirtualBox:~/workspace/tools/verify_cprover/trunk/cprover/src/funfrog$ ./evolcheck ../../../../../hi-bench/main-bench/sv-comp16/c/ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-termination.cil.c

#2 Updated by Karine Even Mendoza over 2 years ago

  • Assignee set to Karine Even Mendoza

#3 Updated by Karine Even Mendoza about 2 years ago

Need larger bit-width:

Data 18446744072635809814(18446744072635809814) is not in between -256 and 255

#4 Updated by Karine Even Mendoza about 2 years ago

Data 18446744072635809814(18446744072635809814) is not in between -4294967296 and 4294967295
With 32 bits, but when using 64 bits - got out of memory.

Run with:
./hifrog ../../../../../../hi-bench/challenge-bench/sv-comp16/c/ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-termination.cil.c --type-constraints 2 --logic qfcuf --no-itp --theoref --force --bitwidth 32

#5 Updated by Karine Even Mendoza about 2 years ago

  • Priority changed from Normal to Low
  • % Done changed from 0 to 10

MEM ISSUES - LOW Priority

#6 Updated by Karine Even Mendoza about 2 years ago

  • Status changed from New to In Progress
  • Priority changed from Low to Normal

This is not related to the goto problem, we need to check it to understand the reason. Maybe the way the assert is encoded.

#7 Updated by Karine Even Mendoza about 2 years ago

  • Status changed from In Progress to Feedback
  • Assignee changed from Karine Even Mendoza to Antti Hyv√§rinen

Shall be with 64 bits not 8. Also I will try to use type constraints.
With 64 bits, even with unwind 1, we get "killed"...

Maybe we can minimize the number of refined instructions so we can use small register (less than 64...)?

Also available in: Atom PDF