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--watchdog--it87_wdt.ko-entry_point_false-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.: 42 55 420 1961
Removed infinite loop in ldv_stop
Removed infinite loop in ldv_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 0.131855010986
Defining function no_llseek as symbolic
Removed calls to '__might_fault' (function is undefined)
Removed calls to '__release_region' (function is undefined)
Defining function printk as symbolic
Defining function __request_region as symbolic
Defining function _copy_to_user as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Defining function register_reboot_notifier as symbolic
Defining function unregister_reboot_notifier as symbolic
Defining function misc_register as symbolic
Defining function misc_deregister as symbolic
Linked our definitions to these undefined functions:
  __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.193097829819
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 69 51 224 1490
INFO: Starting verification
KLEE: WARNING ONCE: function "wdt_write" has inline asm
KLEE: WARNING ONCE: function "wdt_ioctl" has inline asm
KLEE: WARNING ONCE: function "wdt_open" has inline asm
KLEE: WARNING ONCE: function "wdt_release" has inline asm
KLEE: WARNING ONCE: function "wdt_stop" has inline asm
KLEE: WARNING ONCE: function "wdt_keepalive" has inline asm
KLEE: WARNING ONCE: function "superio_enter" has inline asm
KLEE: WARNING ONCE: function "wdt_update_timeout" has inline asm
KLEE: WARNING ONCE: function "wdt_start" has inline asm
KLEE: WARNING ONCE: function "main" has inline asm
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_3f65846c-570a-460b-9fdd-b17e76f0451f/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-CD5fJs/linux-4.2-rc1.tar.xz-08_1a-drivers--watchdog--it87_wdt.ko-entry_point_false-unreach-call.cil.out.c:3167: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 12635 states (over memory cap)
KLEE: WARNING: killing 14079 states (over memory cap)
KLEE: WARNING: killing 14424 states (over memory cap)
KLEE: WARNING: killing 14225 states (over memory cap)
KLEE: WARNING: killing 14479 states (over memory cap)
KLEE: WARNING: killing 14724 states (over memory cap)
KLEE: WARNING: killing 15395 states (over memory cap)
KLEE: WARNING: killing 10806 states (over memory cap)
KLEE: WARNING: killing 15179 states (over memory cap)
KLEE: WARNING: killing 10621 states (over memory cap)
KLEE: WARNING: killing 10484 states (over memory cap)
KLEE: WARNING: killing 10554 states (over memory cap)
KLEE: WARNING: killing 14970 states (over memory cap)
KLEE: WARNING: killing 10476 states (over memory cap)
KLEE: WARNING: killing 10336 states (over memory cap)
KLEE: WARNING: killing 14605 states (over memory cap)
KLEE: WARNING: killing 10671 states (over memory cap)
KLEE: WARNING: killing 10539 states (over memory cap)
KLEE: WARNING: killing 10202 states (over memory cap)
KLEE: WARNING: killing 14618 states (over memory cap)
KLEE: WARNING: killing 10437 states (over memory cap)
KLEE: WARNING: killing 10402 states (over memory cap)
KLEE: WARNING: killing 10073 states (over memory cap)
KLEE: WARNING: killing 10146 states (over memory cap)
KLEE: WARNING: killing 10021 states (over memory cap)
KLEE: WARNING: killing 10193 states (over memory cap)
KLEE: WARNING: killing 14526 states (over memory cap)
KLEE: WARNING: killing 10527 states (over memory cap)
KLEE: WARNING: killing 14335 states (over memory cap)
KLEE: WARNING: killing 10453 states (over memory cap)
KLEE: WARNING: killing 10332 states (over memory cap)
KLEE: WARNING: killing 10302 states (over memory cap)
KLEE: WARNING: killing 10185 states (over memory cap)
KLEE: WARNING: killing 10058 states (over memory cap)
KLEE: WARNING: killing 10137 states (over memory cap)
KLEE: WARNING: killing 10110 states (over memory cap)
KLEE: WARNING: killing 9991 states (over memory cap)
KLEE: WARNING: killing 9969 states (over memory cap)
KLEE: WARNING: killing 9943 states (over memory cap)
KLEE: WARNING: killing 10304 states (over memory cap)
KLEE: WARNING: killing 9805 states (over memory cap)
KLEE: WARNING: killing 9974 states (over memory cap)
KLEE: WARNING: killing 9661 states (over memory cap)
KLEE: WARNING: killing 9926 states (over memory cap)
KLEE: WARNING: killing 9999 states (over memory cap)
KLEE: WARNING: killing 10071 states (over memory cap)
KLEE: WARNING: killing 9863 states (over memory cap)
KLEE: WARNING: killing 9744 states (over memory cap)
KLEE: WARNING: killing 9908 states (over memory cap)
KLEE: WARNING: killing 10073 states (over memory cap)
KLEE: WARNING: killing 10053 states (over memory cap)
KLEE: WARNING: killing 9752 states (over memory cap)
KLEE: WARNING: killing 10103 states (over memory cap)
KLEE: WARNING: killing 10179 states (over memory cap)
KLEE: WARNING: killing 9688 states (over memory cap)
KLEE: WARNING: killing 9947 states (over memory cap)
KLEE: WARNING: killing 10021 states (over memory cap)
KLEE: WARNING: killing 9906 states (over memory cap)
KLEE: WARNING: killing 9883 states (over memory cap)
KLEE: WARNING: killing 9956 states (over memory cap)
KLEE: WARNING: killing 9752 states (over memory cap)
KLEE: WARNING: killing 10011 states (over memory cap)
KLEE: WARNING: killing 9896 states (over memory cap)
KLEE: WARNING: killing 9882 states (over memory cap)
KLEE: WARNING: killing 10139 states (over memory cap)
KLEE: WARNING: killing 10024 states (over memory cap)
KLEE: WARNING: killing 9822 states (over memory cap)
KLEE: WARNING: killing 9987 states (over memory cap)
KLEE: WARNING: killing 9967 states (over memory cap)
KLEE: WARNING: killing 9764 states (over memory cap)
KLEE: WARNING: killing 9565 states (over memory cap)
KLEE: WARNING: killing 10087 states (over memory cap)
KLEE: WARNING: killing 9977 states (over memory cap)
KLEE: WARNING: killing 9870 states (over memory cap)
KLEE: WARNING: killing 10028 states (over memory cap)
KLEE: WARNING: killing 9923 states (over memory cap)
KLEE: WARNING: killing 9815 states (over memory cap)
KLEE: WARNING: killing 9619 states (over memory cap)
KLEE: WARNING: killing 9870 states (over memory cap)
KLEE: WARNING: killing 9943 states (over memory cap)
KLEE: WARNING: killing 10009 states (over memory cap)
KLEE: WARNING: killing 9900 states (over memory cap)
KLEE: WARNING: killing 9710 states (over memory cap)
KLEE: WARNING: killing 9958 states (over memory cap)
KLEE: WARNING: killing 9584 states (over memory cap)
KLEE: WARNING: killing 10093 states (over memory cap)
KLEE: WARNING: killing 9990 states (over memory cap)
KLEE: WARNING: killing 10061 states (over memory cap)
KLEE: WARNING: killing 10042 states (over memory cap)
KLEE: WARNING: killing 9673 states (over memory cap)
KLEE: WARNING: killing 9918 states (over memory cap)
KLEE: WARNING: killing 9638 states (over memory cap)
KLEE: WARNING: killing 10056 states (over memory cap)
KLEE: WARNING: killing 9868 states (over memory cap)
KLEE: WARNING: killing 9935 states (over memory cap)
KLEE: WARNING: killing 9830 states (over memory cap)
KLEE: WARNING: killing 9813 states (over memory cap)
KLEE: WARNING: killing 9885 states (over memory cap)
KLEE: WARNING: killing 9693 states (over memory cap)
KLEE: WARNING: killing 9934 states (over memory cap)
KLEE: WARNING: killing 9837 states (over memory cap)
KLEE: WARNING: killing 10076 states (over memory cap)
KLEE: WARNING: killing 9887 states (over memory cap)
KLEE: WARNING: killing 10129 states (over memory cap)
KLEE: WARNING: killing 9852 states (over memory cap)
KLEE: WARNING: killing 9667 states (over memory cap)
KLEE: WARNING: killing 9738 states (over memory cap)
KLEE: WARNING: killing 10145 states (over memory cap)
KLEE: WARNING: killing 9787 states (over memory cap)
KLEE: WARNING: killing 10025 states (over memory cap)
