bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--net--arcnet--com90xx.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.: 64 50 606 2808
Removed infinite loop in ldv_stop
Removed infinite loop in ldv_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 0.224334001541
Defining function arcnet_interrupt as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'unregister_netdev' (function is undefined)
Removed calls to 'free_irq' (function is undefined)
Removed calls to 'iounmap' (function is undefined)
Removed calls to '__release_region' (function is undefined)
Removed calls to 'free_netdev' (function is undefined)
Removed calls to '__const_udelay' (function is undefined)
Defining function printk as symbolic
Defining function __request_region as symbolic
Defining function probe_irq_on as symbolic
Defining function probe_irq_off as symbolic
Defining function alloc_arcdev as symbolic
Defining function register_netdev as symbolic
Defining function request_threaded_irq as symbolic
Defining function ioremap_nocache as symbolic
Linked our definitions to these undefined functions:
  __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.277235984802
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 110 53 343 1699
INFO: Starting verification
KLEE: WARNING ONCE: function "main" has inline asm
KLEE: WARNING ONCE: function "check_mirror" has inline asm
KLEE: WARNING ONCE: function "com90xx_command" has inline asm
KLEE: WARNING ONCE: function "com90xx_status" has inline asm
KLEE: WARNING ONCE: function "com90xx_setmask" has inline asm
KLEE: WARNING ONCE: function "com90xx_reset" has inline asm
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_fcafd4c8-6b6d-4bde-8dc8-620332029922/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: ERROR: /tmp/symbiotic-EMU1ED/linux-4.2-rc1.tar.xz-08_1a-drivers--net--arcnet--com90xx.ko-entry_point_true-unreach-call.cil.out.c:5471: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 7406 states (over memory cap)
KLEE: WARNING: killing 7880 states (over memory cap)
KLEE: WARNING: killing 7779 states (over memory cap)
KLEE: WARNING: killing 7942 states (over memory cap)
KLEE: WARNING: killing 6420 states (over memory cap)
KLEE: WARNING: killing 6400 states (over memory cap)
KLEE: WARNING: killing 8177 states (over memory cap)
KLEE: WARNING: killing 6421 states (over memory cap)
KLEE: WARNING: killing 6343 states (over memory cap)
KLEE: WARNING: killing 6634 states (over memory cap)
KLEE: WARNING: killing 6804 states (over memory cap)
KLEE: WARNING: killing 7094 states (over memory cap)
KLEE: WARNING: killing 7018 states (over memory cap)
KLEE: WARNING: killing 7000 states (over memory cap)
KLEE: WARNING: killing 7347 states (over memory cap)
KLEE: WARNING: killing 7272 states (over memory cap)
KLEE: WARNING: killing 7496 states (over memory cap)
KLEE: WARNING: killing 7295 states (over memory cap)
KLEE: WARNING: killing 7455 states (over memory cap)
KLEE: WARNING: killing 7618 states (over memory cap)
KLEE: WARNING: killing 7540 states (over memory cap)
KLEE: WARNING: killing 7699 states (over memory cap)
KLEE: WARNING: killing 7679 states (over memory cap)
KLEE: WARNING: killing 7956 states (over memory cap)
KLEE: WARNING: killing 8000 states (over memory cap)
KLEE: WARNING: killing 7742 states (over memory cap)
KLEE: WARNING: killing 7958 states (over memory cap)
KLEE: WARNING: killing 7996 states (over memory cap)
KLEE: WARNING: killing 7736 states (over memory cap)
KLEE: WARNING: killing 7777 states (over memory cap)
KLEE: WARNING: killing 8109 states (over memory cap)
KLEE: WARNING: killing 7796 states (over memory cap)
KLEE: WARNING: killing 8070 states (over memory cap)
KLEE: WARNING: killing 5844 states (over memory cap)
KLEE: WARNING: killing 7864 states (over memory cap)
KLEE: WARNING: killing 8018 states (over memory cap)
KLEE: WARNING: killing 8174 states (over memory cap)
KLEE: WARNING: killing 8267 states (over memory cap)
KLEE: WARNING: killing 8191 states (over memory cap)
KLEE: WARNING: killing 8347 states (over memory cap)
KLEE: WARNING: killing 8270 states (over memory cap)
KLEE: WARNING: killing 8079 states (over memory cap)
KLEE: WARNING: killing 8228 states (over memory cap)
KLEE: WARNING: killing 7866 states (over memory cap)
KLEE: WARNING: killing 8187 states (over memory cap)
KLEE: WARNING: killing 5908 states (over memory cap)
KLEE: WARNING: killing 5673 states (over memory cap)
KLEE: WARNING: killing 8141 states (over memory cap)
KLEE: WARNING: killing 5763 states (over memory cap)
KLEE: WARNING: killing 8112 states (over memory cap)
KLEE: WARNING: killing 5855 states (over memory cap)
KLEE: WARNING: killing 7915 states (over memory cap)
KLEE: WARNING: killing 5610 states (over memory cap)
KLEE: WARNING: killing 8165 states (over memory cap)
KLEE: WARNING: killing 5697 states (over memory cap)
KLEE: WARNING: killing 7906 states (over memory cap)
KLEE: WARNING: killing 5784 states (over memory cap)
KLEE: WARNING: killing 7932 states (over memory cap)
KLEE: WARNING: killing 5762 states (over memory cap)
KLEE: WARNING: killing 5810 states (over memory cap)
KLEE: WARNING: killing 5582 states (over memory cap)
KLEE: WARNING: killing 5742 states (over memory cap)
KLEE: WARNING: killing 8036 states (over memory cap)
KLEE: WARNING: killing 5664 states (over memory cap)
KLEE: WARNING: killing 5547 states (over memory cap)
KLEE: WARNING: killing 5539 states (over memory cap)
KLEE: WARNING: killing 5641 states (over memory cap)
KLEE: WARNING: killing 5522 states (over memory cap)
KLEE: WARNING: killing 7853 states (over memory cap)
KLEE: WARNING: killing 5666 states (over memory cap)
KLEE: WARNING: killing 5765 states (over memory cap)
KLEE: WARNING: killing 5703 states (over memory cap)
KLEE: WARNING: killing 5751 states (over memory cap)
KLEE: WARNING: killing 5634 states (over memory cap)
KLEE: WARNING: killing 5409 states (over memory cap)
KLEE: WARNING: killing 5618 states (over memory cap)
KLEE: WARNING: killing 5502 states (over memory cap)
KLEE: WARNING: killing 5437 states (over memory cap)
KLEE: WARNING: killing 5538 states (over memory cap)
KLEE: WARNING: killing 5583 states (over memory cap)
KLEE: WARNING: killing 5630 states (over memory cap)
KLEE: WARNING: killing 5567 states (over memory cap)
KLEE: WARNING: killing 5828 states (over memory cap)
KLEE: WARNING: killing 5395 states (over memory cap)
KLEE: WARNING: killing 5547 states (over memory cap)
KLEE: WARNING: killing 5429 states (over memory cap)
KLEE: WARNING: killing 5370 states (over memory cap)
KLEE: WARNING: killing 5574 states (over memory cap)
KLEE: WARNING: killing 5566 states (over memory cap)
KLEE: WARNING: killing 5718 states (over memory cap)
KLEE: WARNING: killing 5657 states (over memory cap)
KLEE: WARNING: killing 5439 states (over memory cap)
KLEE: WARNING: killing 5587 states (over memory cap)
KLEE: WARNING: killing 5636 states (over memory cap)
KLEE: WARNING: killing 5363 states (over memory cap)
KLEE: WARNING: killing 5618 states (over memory cap)
KLEE: WARNING: killing 5663 states (over memory cap)
KLEE: WARNING: killing 5550 states (over memory cap)
KLEE: WARNING: killing 5544 states (over memory cap)
KLEE: WARNING: killing 5587 states (over memory cap)
KLEE: WARNING: killing 5528 states (over memory cap)
KLEE: WARNING: killing 5574 states (over memory cap)
KLEE: WARNING: killing 5514 states (over memory cap)
KLEE: WARNING: killing 5454 states (over memory cap)
KLEE: WARNING: killing 5550 states (over memory cap)
KLEE: WARNING: killing 5750 states (over memory cap)
KLEE: WARNING: killing 5329 states (over memory cap)
KLEE: WARNING: killing 5427 states (over memory cap)
KLEE: WARNING: killing 5367 states (over memory cap)
KLEE: WARNING: killing 5564 states (over memory cap)
KLEE: WARNING: killing 5402 states (over memory cap)
KLEE: WARNING: killing 5651 states (over memory cap)
KLEE: WARNING: killing 5593 states (over memory cap)
KLEE: WARNING: killing 5845 states (over memory cap)
KLEE: WARNING: killing 5477 states (over memory cap)
KLEE: WARNING: killing 5932 states (over memory cap)
KLEE: WARNING: killing 5668 states (over memory cap)
KLEE: WARNING: killing 5558 states (over memory cap)
KLEE: WARNING: killing 5397 states (over memory cap)
KLEE: WARNING: killing 5390 states (over memory cap)
KLEE: WARNING: killing 5585 states (over memory cap)
KLEE: WARNING: killing 5678 states (over memory cap)
