Project

General

Profile

Bug #5002

--theoref bug: BitBlaster.C:477: BVRef BitBlaster::bbBvand(PTRef): Assertion `logic.getPterm(logic.getPterm(tr)[0]).size() == logic.getPterm(logic.getPterm(tr)[1]).size()' failed.

Added by Karine Even Mendoza about 7 years ago. Updated about 7 years ago.

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

100%

Estimated time:

Description

Any idea what's the issue here? what do we need to fix?
IT happens in many benchmarks

  • WARNING: no body for function mite_list_devices
    SYMEX TIME: 183.009
    All SSA steps: 812
    Ignored SSA steps after slice: 457
    SLICER TIME: 0.309
    ; 0 | 0 0 | 144.640 s | 366.309 MB
    CONVERSION TIME: 10.686
    SOLVER TIME: 3.2
    RESULT: SAT - doesn't hold

Trying to refine with CUF+BitBlast
(driven by iterative CE-analysis)

; Warning: disabling SATElite preprocessing to track proof
; 0 | 0 0 | 150.548 s | 413.547 MB
; 0 | 0 0 | 150.920 s | 413.562 MB
; 0 | 0 0 | 151.564 s | 413.594 MB
; 0 | 0 0 | 152.300 s | 413.594 MB
; 0 | 0 0 | 153.204 s | 413.594 MB
; 0 | 0 0 | 154.212 s | 413.609 MB
; 0 | 0 0 | 155.324 s | 413.641 MB
; Warning: disabling SATElite preprocessing to track proof
; 0 | 0 0 | 158.176 s | 464.910 MB
hifrog: BitBlaster.C:477: BVRef BitBlaster::bbBvand(PTRef): Assertion `logic.getPterm(logic.getPterm(tr)[0]).size() logic.getPterm(logic.getPterm(tr)[1]).size()' failed.
13653==
13653 HEAP SUMMARY:
13653 in use at exit: 176,735,464 bytes in 323,346 blocks
13653 total heap usage: 2,346,632 allocs, 2,023,286 frees, 317,988,967 bytes allocated
13653
13653 LEAK SUMMARY:
13653 definitely lost: 422,361 bytes in 5,612 blocks
13653 indirectly lost: 4,507,836 bytes in 3,410 blocks
13653 possibly lost: 1,466,832 bytes in 31,599 blocks
13653 still reachable: 170,338,435 bytes in 282,725 blocks
13653 suppressed: 0 bytes in 0 blocks
13653 Rerun with --leak-check=full to see details of leaked memory
13653
13653 For counts of detected and suppressed errors, rerun with: -v
13653 ERROR SUMMARY: 0 errors from 0 contexts (suppressed: 0 from 0)
Aborted (core dumped)
karinek@karinek-VirtualBox:~/workspace/tools/hi-bench/challenge-bench$ valgrind ./hifrog sv-comp16/c/ldv-commit-tester/m0_false-unreach-call_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36-1.c --theoref --logic qfcuf --claim 1 --unwind 2 --bitwidth 32

History

#1 Updated by Karine Even Mendoza about 7 years ago

  • Priority changed from High to Urgent

It fails majority of the sv-comp, so it is super important to take care of it - if we wish to have sv-comp benchmarks!

#2 Updated by Karine Even Mendoza about 7 years ago

I think it is something we are not calling right, maybe something is missing (push(??)).

The error is from src/tsolvers/bvsolver/BitBlaster.C, in OpenSMT.
The method is: BVRef BitBlaster::bbBvand(PTRef tr).
The assert is: assert(logic.getPterm(logic.getPterm(tr)[0]).size() == logic.getPterm(logic.getPterm(tr)[1]).size()); // Should be e->get2nd( )->getWidth( ).

To solve it, I wish first to understand what is the reason it happens, what OpenSMT expects and what it gets that it is not ok, I wish to understand the bigger picture.

Also consider to add a message next to the assert: assert(cond && "the issue here is...."); can help for use for next time!

Thanks

#3 Updated by Antti Hyvärinen about 7 years ago

It should be fixed now. The assertion was old and not relevant, and checked in a new way already. I don't know how on earth is was on the code haha

#4 Updated by Karine Even Mendoza about 7 years ago

  • Status changed from Feedback to Closed
  • % Done changed from 0 to 100

IS ok now

Also available in: Atom PDF