hifrog

File is: /home/asadis/hi-bench/challenge-bench/sv-comp17/c/busybox-1.22.0/touch_false-unreach-call_true-no-overflow_true-valid-memsafety.c

Verification was not successful, here is the last few lines: ...

Total number of claims in program...(1).
; Warning: disabling SATElite preprocessing to track proof
Use QF_UF logic.

---------checking claim # 1 ---------

; Warning: disabling SATElite preprocessing to track proof
hifrog: /home/asadis/new-hifrog/hifrog/trunk/cprover/src/funfrog/symex_assertion_sum.cpp:1695: ssa_exprt symex_assertion_sumt::get_next_version(const symbolt&): Assertion `state.level2.current_names.find(ssa_l1_identifier) != state.level2.current_names.end()' failed.

• INLINING function: __CPROVER_initialize
• INLINING function: main
  Processing a deferred function: __CPROVER_initialize
  Processing a deferred function: main
  Command terminated by signal 6
  real 4.12

Note: Busybox is full of pointer, heap manipulation,...as sated in the svcomp webpage this category aims to represent verification tasks from real software systems.

Note2: This crash happens in 9 benchmarks out of 40.