Bug #5304
crash on ~/hi-bench/main-bench/bench_SATpaper_128/
0%
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 7 years ago
- Assignee set to Karine Even Mendoza
- Priority changed from Normal to High
#2 Updated by Karine Even Mendoza almost 7 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