bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--block--paride--pt.ko-main.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.: 85 91 763 3992
INFO: Compilation, preparation and instrumentation time: 0.239458799362
Removed calls to 'device_destroy' (function is undefined)
Removed calls to 'class_destroy' (function is undefined)
Removed calls to '__unregister_chrdev' (function is undefined)
Removed calls to 'pi_release' (function is undefined)
Removed calls to '__const_udelay' (function is undefined)
Removed calls to 'pi_disconnect' (function is undefined)
Removed calls to 'pi_write_block' (function is undefined)
Removed calls to 'pi_read_block' (function is undefined)
Removed calls to 'might_fault' (function is undefined)
Defining function printk as symbolic
Defining function __class_create as symbolic
Defining function device_create as symbolic
Defining function __register_chrdev as symbolic
Defining function snprintf as symbolic
Defining function pi_init as symbolic
Removed calls to 'pi_connect' (function is undefined)
Removed calls to 'pi_write_regr' (function is undefined)
Defining function schedule_timeout_interruptible as symbolic
Defining function pi_read_regr as symbolic
Defining function _copy_to_user as symbolic
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Defining function _copy_from_user as symbolic
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function noop_llseek as symbolic
Defining function mutex_trylock as symbolic
Linked our definitions to these undefined functions:
  __kmalloc
  kfree
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 0.23056602478
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 132 86 460 2212
INFO: Starting verification
KLEE: WARNING ONCE: function "pt_release" has inline asm
KLEE: WARNING ONCE: function "pt_open" has inline asm
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 12462 states (over memory cap)
KLEE: WARNING: killing 15318 states (over memory cap)
KLEE: WARNING: killing 15830 states (over memory cap)
KLEE: WARNING: killing 16093 states (over memory cap)
KLEE: WARNING: killing 15883 states (over memory cap)
KLEE: WARNING: killing 16633 states (over memory cap)
KLEE: WARNING: killing 16538 states (over memory cap)
KLEE: WARNING: killing 16449 states (over memory cap)
KLEE: WARNING: killing 16595 states (over memory cap)
KLEE: WARNING: killing 16634 states (over memory cap)
KLEE: WARNING: killing 11917 states (over memory cap)
KLEE: WARNING: killing 11651 states (over memory cap)
KLEE: WARNING: killing 16568 states (over memory cap)
KLEE: WARNING: killing 11785 states (over memory cap)
KLEE: WARNING: killing 11522 states (over memory cap)
KLEE: WARNING: killing 11597 states (over memory cap)
KLEE: WARNING: killing 11563 states (over memory cap)
KLEE: WARNING: killing 11748 states (over memory cap)
KLEE: WARNING: killing 11600 states (over memory cap)
KLEE: WARNING: killing 11449 states (over memory cap)
KLEE: WARNING: killing 11753 states (over memory cap)
KLEE: WARNING: killing 11939 states (over memory cap)
KLEE: WARNING: killing 11902 states (over memory cap)
KLEE: WARNING: killing 11635 states (over memory cap)
KLEE: WARNING: killing 11825 states (over memory cap)
KLEE: WARNING: killing 11784 states (over memory cap)
KLEE: WARNING: killing 11864 states (over memory cap)
KLEE: WARNING: killing 12158 states (over memory cap)
KLEE: WARNING: killing 11897 states (over memory cap)
KLEE: WARNING: killing 11751 states (over memory cap)
KLEE: WARNING: killing 12042 states (over memory cap)
KLEE: WARNING: killing 11897 states (over memory cap)
KLEE: WARNING: killing 11973 states (over memory cap)
KLEE: WARNING: killing 11935 states (over memory cap)
KLEE: WARNING: killing 11686 states (over memory cap)
KLEE: WARNING: killing 12080 states (over memory cap)
KLEE: WARNING: killing 11833 states (over memory cap)
KLEE: WARNING: killing 11794 states (over memory cap)
KLEE: WARNING: killing 11969 states (over memory cap)
KLEE: WARNING: killing 12150 states (over memory cap)
KLEE: WARNING: killing 11909 states (over memory cap)
KLEE: WARNING: killing 12087 states (over memory cap)
KLEE: WARNING: killing 11840 states (over memory cap)
KLEE: WARNING: killing 11697 states (over memory cap)
KLEE: WARNING: killing 11875 states (over memory cap)
KLEE: WARNING: killing 11950 states (over memory cap)
KLEE: WARNING: killing 11911 states (over memory cap)
KLEE: WARNING: killing 11983 states (over memory cap)
KLEE: WARNING: killing 11949 states (over memory cap)
KLEE: WARNING: killing 12026 states (over memory cap)
KLEE: WARNING: killing 11991 states (over memory cap)
KLEE: WARNING: killing 11856 states (over memory cap)
KLEE: WARNING: killing 11826 states (over memory cap)
KLEE: WARNING: killing 11996 states (over memory cap)
KLEE: WARNING: killing 11963 states (over memory cap)
KLEE: WARNING: killing 11729 states (over memory cap)
KLEE: WARNING: killing 11901 states (over memory cap)
KLEE: WARNING: killing 12070 states (over memory cap)
KLEE: WARNING: killing 11945 states (over memory cap)
KLEE: WARNING: killing 12012 states (over memory cap)
KLEE: WARNING: killing 11984 states (over memory cap)
KLEE: WARNING: killing 11852 states (over memory cap)
KLEE: WARNING: killing 11821 states (over memory cap)
KLEE: WARNING: killing 12095 states (over memory cap)
KLEE: WARNING: killing 11961 states (over memory cap)
KLEE: WARNING: killing 11927 states (over memory cap)
KLEE: WARNING: killing 12099 states (over memory cap)
KLEE: WARNING: killing 11967 states (over memory cap)
KLEE: WARNING: killing 11843 states (over memory cap)
KLEE: WARNING: killing 12115 states (over memory cap)
KLEE: WARNING: killing 12085 states (over memory cap)
KLEE: WARNING: killing 11851 states (over memory cap)
KLEE: WARNING: killing 11725 states (over memory cap)
KLEE: WARNING: killing 11696 states (over memory cap)
KLEE: WARNING: killing 12057 states (over memory cap)
KLEE: WARNING: killing 11832 states (over memory cap)
KLEE: WARNING: killing 11998 states (over memory cap)
KLEE: WARNING: killing 11776 states (over memory cap)
KLEE: WARNING: killing 11747 states (over memory cap)
KLEE: WARNING: killing 11908 states (over memory cap)
KLEE: WARNING: killing 11881 states (over memory cap)
KLEE: WARNING: killing 11853 states (over memory cap)
KLEE: WARNING: killing 11727 states (over memory cap)
KLEE: WARNING: killing 11894 states (over memory cap)
KLEE: WARNING: killing 11765 states (over memory cap)
KLEE: WARNING: killing 11637 states (over memory cap)
KLEE: WARNING: killing 11802 states (over memory cap)
KLEE: WARNING: killing 11872 states (over memory cap)
KLEE: WARNING: killing 11943 states (over memory cap)
KLEE: WARNING: killing 12007 states (over memory cap)
KLEE: WARNING: killing 11888 states (over memory cap)
KLEE: WARNING: killing 11865 states (over memory cap)
KLEE: WARNING: killing 11930 states (over memory cap)
KLEE: WARNING: killing 11811 states (over memory cap)
KLEE: WARNING: killing 11781 states (over memory cap)
KLEE: WARNING: killing 12031 states (over memory cap)
KLEE: WARNING: killing 11818 states (over memory cap)
KLEE: WARNING: killing 11699 states (over memory cap)
KLEE: WARNING: killing 11850 states (over memory cap)
KLEE: WARNING: killing 11552 states (over memory cap)
KLEE: WARNING: killing 11801 states (over memory cap)
KLEE: WARNING: killing 11866 states (over memory cap)
KLEE: WARNING: killing 11841 states (over memory cap)
KLEE: WARNING: killing 11813 states (over memory cap)
KLEE: WARNING: killing 11882 states (over memory cap)
