Project

General

Profile

Bug #5304

crash on ~/hi-bench/main-bench/bench_SATpaper_128/

Added by Sepideh Asadi almost 2 years ago. Updated almost 2 years ago.

Status:
Feedback
Priority:
Normal
Assignee:
Start date:
15/06/2017
Due date:
% Done:

0%

Estimated time:

Description

./hifrog --claim 1 --theoref --no-itp --unwind 10 --bitwidth 32 --heuristic 4 --type-byte-constraints 2

~/hi-bench/main-bench/bench_SATpaper_128/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--gpio--gpio-mc33880.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c

ERRoR message:
Caught exception: value_sett::assign type mismatch: rhs.type():

History

#1 Updated by Karine Even Mendoza almost 2 years ago

  • Assignee set to Karine Even Mendoza
  • Priority changed from Normal to High

#2 Updated by Karine Even Mendoza almost 2 years ago

  • Status changed from New to Feedback
  • Assignee changed from Karine Even Mendoza to Sepideh Asadi
  • Priority changed from High to Normal

For me it works fine, maybe it was a differnt benchmark?

(check-sat)
CONVERSION TIME: 0.65
; theory refiner query time so far: 0.000000
; 0 | 0 0 | 2.744 s | 136.445 MB
SOLVER TIME: 0.207
RESULT: UNSAT - it holds!

(Warning: Result holds ONLY in this bound (!) Initial unwinding bound: 10)
ASSERTION HOLDS

VERIFICATION SUCCESSFUL
TOTAL TIME FOR CHECKING THIS CLAIM: 3.068

Main Checked Assertion:
file ../../../../../../hi-bench/main-bench/bench_SATpaper_128/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--gpio--gpio-mc33880.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c line 2808 function ldv_blast_assert
assertion
FALSE
#X: Done.
karinek@karinek-VirtualBox:~/workspace/tools/hifrog_lra_lattice/hifrog/trunk/cprover/src/funfrog$ ./hifrog ../../../../../../hi-bench/main-bench/bench_SATpaper_128/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--gpio--gpio-mc33880.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c --claim 1 --theoref --no-itp --unwind 10 --bitwidth 32 --heuristic 4 --type-byte-constraints 2

Also available in: Atom PDF