bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-kernel--locking--locktorture.ko-entry_point_true-unreach-call.cil.out.c


--------------------------------------------------------------------------------


5.0.0-KLEE:86e6f6f8-dg:03407af1-symbiotic:a8aa8ad6-minisat:3db58943-stp:17249213-sbt-instrumentation:dd7e4312
INFO: After compilation stats: Globals/Functions/Blocks/Instr.: 68 46 376 1510
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.139867067337
Removed calls to '__const_udelay' (function is undefined)
Defining function torture_random as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '__udelay' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'torture_init_end' (function is undefined)
Removed calls to 'ldv_check_final_state' (function is undefined)
Defining function ldv_release_1 as symbolic
Defining function ldv_probe_1 as symbolic
Removed calls to '_torture_stop_kthread' (function is undefined)
Defining function ldv_release_3 as symbolic
Defining function ldv_probe_3 as symbolic
Defining function ldv_release_2 as symbolic
Defining function ldv_probe_2 as symbolic
Defining function torture_init_begin as symbolic
Defining function printk as symbolic
Defining function __bitmap_weight as symbolic
Defining function torture_cleanup as symbolic
Defining function torture_onoff_failures as symbolic
Defining function kmem_cache_alloc as symbolic
Defining function ldv_some_page as symbolic
Linked our definitions to these undefined functions:
  strcmp
  __kmalloc
  kfree
  __VERIFIER_assume
  __VERIFIER_calloc0
  __VERIFIER_error
  __VERIFIER_exit
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
  __VERIFIER_nondet_pointer_named
  __VERIFIER_nondet_ulong_named
INFO: After-slicing optimizations and preparation time: 0.162174940109
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 81 51 173 697
INFO: Starting verification
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_9707f01a-c45b-4569-a42d-2e6942234761/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 16402 states (over memory cap)
KLEE: WARNING: killing 12508 states (over memory cap)
KLEE: WARNING: killing 11981 states (over memory cap)
KLEE: WARNING: killing 12169 states (over memory cap)
KLEE: WARNING: killing 12598 states (over memory cap)
KLEE: WARNING: killing 12429 states (over memory cap)
KLEE: WARNING: killing 12621 states (over memory cap)
KLEE: WARNING: killing 13047 states (over memory cap)
KLEE: WARNING: killing 13589 states (over memory cap)
KLEE: WARNING: killing 13313 states (over memory cap)
KLEE: WARNING: killing 13509 states (over memory cap)
KLEE: WARNING: killing 13578 states (over memory cap)
KLEE: WARNING: killing 13655 states (over memory cap)
KLEE: WARNING: killing 13847 states (over memory cap)
KLEE: WARNING: killing 13920 states (over memory cap)
KLEE: WARNING: killing 13540 states (over memory cap)
KLEE: WARNING: killing 13959 states (over memory cap)
KLEE: WARNING: killing 13463 states (over memory cap)
KLEE: WARNING: killing 13648 states (over memory cap)
KLEE: WARNING: killing 13838 states (over memory cap)
KLEE: WARNING: killing 13795 states (over memory cap)
KLEE: WARNING: killing 13418 states (over memory cap)
KLEE: WARNING: killing 13375 states (over memory cap)
KLEE: WARNING: killing 13452 states (over memory cap)
KLEE: WARNING: killing 13191 states (over memory cap)
KLEE: WARNING: killing 13378 states (over memory cap)
KLEE: WARNING: killing 13227 states (over memory cap)
KLEE: WARNING: killing 13524 states (over memory cap)
KLEE: WARNING: killing 13379 states (over memory cap)
KLEE: WARNING: killing 13783 states (over memory cap)
KLEE: WARNING: killing 14184 states (over memory cap)
KLEE: WARNING: killing 13709 states (over memory cap)
KLEE: WARNING: killing 13679 states (over memory cap)
KLEE: WARNING: killing 13643 states (over memory cap)
KLEE: WARNING: killing 13824 states (over memory cap)
KLEE: WARNING: killing 13900 states (over memory cap)
KLEE: WARNING: killing 13649 states (over memory cap)
KLEE: WARNING: killing 13509 states (over memory cap)
KLEE: WARNING: killing 13580 states (over memory cap)
KLEE: WARNING: killing 13983 states (over memory cap)
KLEE: WARNING: killing 13618 states (over memory cap)
KLEE: WARNING: killing 13473 states (over memory cap)
KLEE: WARNING: killing 13867 states (over memory cap)
KLEE: WARNING: killing 13624 states (over memory cap)
KLEE: WARNING: killing 13271 states (over memory cap)
KLEE: WARNING: killing 13773 states (over memory cap)
KLEE: WARNING: killing 13740 states (over memory cap)
KLEE: WARNING: killing 13815 states (over memory cap)
KLEE: WARNING: killing 13780 states (over memory cap)
KLEE: WARNING: killing 13646 states (over memory cap)
KLEE: WARNING: killing 13608 states (over memory cap)
KLEE: WARNING: killing 13688 states (over memory cap)
KLEE: WARNING: killing 13757 states (over memory cap)
KLEE: WARNING: killing 13519 states (over memory cap)
KLEE: WARNING: killing 13061 states (over memory cap)
KLEE: WARNING: killing 13447 states (over memory cap)
KLEE: WARNING: killing 13727 states (over memory cap)
KLEE: WARNING: killing 13284 states (over memory cap)
KLEE: WARNING: killing 13771 states (over memory cap)
KLEE: WARNING: killing 13741 states (over memory cap)
KLEE: WARNING: killing 13715 states (over memory cap)
KLEE: WARNING: killing 13787 states (over memory cap)
KLEE: WARNING: killing 13452 states (over memory cap)
KLEE: WARNING: killing 13421 states (over memory cap)
KLEE: WARNING: killing 13896 states (over memory cap)
KLEE: WARNING: killing 13664 states (over memory cap)
KLEE: WARNING: killing 13843 states (over memory cap)
KLEE: WARNING: killing 13813 states (over memory cap)
KLEE: WARNING: killing 13581 states (over memory cap)
KLEE: WARNING: killing 13554 states (over memory cap)
KLEE: WARNING: killing 13319 states (over memory cap)
KLEE: WARNING: killing 13496 states (over memory cap)
KLEE: WARNING: killing 13362 states (over memory cap)
KLEE: WARNING: killing 13531 states (over memory cap)
KLEE: WARNING: killing 13600 states (over memory cap)
KLEE: WARNING: killing 13174 states (over memory cap)
KLEE: WARNING: killing 13346 states (over memory cap)
KLEE: WARNING: killing 13320 states (over memory cap)
KLEE: WARNING: killing 14181 states (over memory cap)
KLEE: WARNING: killing 13862 states (over memory cap)
KLEE: WARNING: killing 13534 states (over memory cap)
KLEE: WARNING: killing 13413 states (over memory cap)
KLEE: WARNING: killing 13486 states (over memory cap)
KLEE: WARNING: killing 13852 states (over memory cap)
KLEE: WARNING: killing 13527 states (over memory cap)
KLEE: WARNING: killing 13406 states (over memory cap)
KLEE: WARNING: killing 13475 states (over memory cap)
KLEE: WARNING: killing 13844 states (over memory cap)
KLEE: WARNING: killing 13330 states (over memory cap)
KLEE: WARNING: killing 13789 states (over memory cap)
KLEE: WARNING: killing 13665 states (over memory cap)
KLEE: WARNING: killing 13544 states (over memory cap)
KLEE: WARNING: killing 13515 states (over memory cap)
KLEE: WARNING: killing 13397 states (over memory cap)
KLEE: WARNING: killing 13659 states (over memory cap)
KLEE: WARNING: killing 13344 states (over memory cap)
KLEE: WARNING: killing 13223 states (over memory cap)
KLEE: WARNING: killing 13393 states (over memory cap)
KLEE: WARNING: killing 13745 states (over memory cap)
KLEE: WARNING: killing 13522 states (over memory cap)
KLEE: WARNING: killing 13598 states (over memory cap)
KLEE: WARNING: killing 13201 states (over memory cap)
KLEE: WARNING: killing 13651 states (over memory cap)
KLEE: WARNING: killing 13245 states (over memory cap)
KLEE: WARNING: killing 13413 states (over memory cap)
KLEE: WARNING: killing 13288 states (over memory cap)
KLEE: WARNING: killing 13452 states (over memory cap)
KLEE: WARNING: killing 13149 states (over memory cap)
KLEE: WARNING: killing 13776 states (over memory cap)
KLEE: WARNING: killing 13470 states (over memory cap)
KLEE: WARNING: killing 13447 states (over memory cap)
KLEE: WARNING: killing 13342 states (over memory cap)
KLEE: WARNING: killing 13690 states (over memory cap)
KLEE: WARNING: killing 13389 states (over memory cap)
KLEE: WARNING: killing 13458 states (over memory cap)
KLEE: WARNING: killing 13335 states (over memory cap)
KLEE: WARNING: killing 13132 states (over memory cap)
KLEE: WARNING: killing 13204 states (over memory cap)
KLEE: WARNING: killing 13637 states (over memory cap)
