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-drivers--usb--host--xhci-hcd.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.: 834 533 7338 55814
Removed infinite loop in arch_local_save_flags
Removed infinite loop in xhci_endpoint_init
Removed infinite loop in xhci_get_endpoint_interval
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 1.84591603279
Removed calls to 'usb_put_hcd' (function is undefined)
Removed calls to 'usb_hcd_pci_remove' (function is undefined)
Removed calls to 'usb_remove_hcd' (function is undefined)
Defining function pci_set_power_state as symbolic
Defining function usb_hcd_pci_probe as symbolic
Defining function usb_create_shared_hcd as symbolic
Defining function usb_add_hcd as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'usb_hcd_resume_root_hub' (function is undefined)
Removed calls to 'usb_wakeup_notification' (function is undefined)
Removed calls to 'complete' (function is undefined)
Removed calls to 'usb_hcd_poll_rh_status' (function is undefined)
Removed calls to 'usb_hcd_unlink_urb_from_ep' (function is undefined)
Removed calls to 'usb_hcd_giveback_urb' (function is undefined)
Removed calls to '__const_udelay' (function is undefined)
Removed calls to 'free_irq' (function is undefined)
Removed calls to 'pci_disable_msi' (function is undefined)
Removed calls to 'usb_enable_intel_xhci_ports' (function is undefined)
Removed calls to '_raw_spin_lock_irq' (function is undefined)
Removed calls to '_raw_spin_unlock_irq' (function is undefined)
Removed calls to 'usb_amd_dev_put' (function is undefined)
Removed calls to 'usb_disable_xhci_ports' (function is undefined)
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to 'add_timer' (function is undefined)
Removed calls to 'msleep' (function is undefined)
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function dev_warn as symbolic
Removed calls to 'lockdep_rcu_suspicious' (function is undefined)
Removed calls to 'ldv__builtin_va_start' (function is undefined)
Removed calls to 'ldv__builtin_va_end' (function is undefined)
Removed calls to 'wait_for_completion' (function is undefined)
Defining function debug_lockdep_rcu_enabled as symbolic
Defining function rcu_is_watching as symbolic
Defining function rcu_lockdep_current_cpu_online as symbolic
Defining function lock_is_held as symbolic
Defining function dev_err as symbolic
Defining function mod_timer as symbolic
Removed calls to 'dma_pool_free' (function is undefined)
Defining function radix_tree_lookup as symbolic
Defining function radix_tree_delete as symbolic
Defining function dma_pool_alloc as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'debug_dma_free_coherent' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Defining function del_timer_sync as symbolic
Removed calls to 'usb_hc_died' (function is undefined)
Removed calls to 'usb_amd_quirk_pll_enable' (function is undefined)
Defining function msecs_to_jiffies as symbolic
Defining function usb_acpi_power_manageable as symbolic
Defining function usb_acpi_set_power_state as symbolic
Defining function wait_for_completion_timeout as symbolic
Defining function usb_hcd_check_unlink_urb as symbolic
Removed calls to 'usb_amd_quirk_pll_disable' (function is undefined)
Defining function ___ratelimit as symbolic
Defining function usb_hcd_link_urb_to_ep as symbolic
Defining function sg_next as symbolic
Removed calls to 'pci_disable_msix' (function is undefined)
Defining function usb_hcd_is_primary_hcd as symbolic
Removed calls to 'dma_pool_destroy' (function is undefined)
Removed calls to 'usb_root_hub_lost_power' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'set_timer_slack' (function is undefined)
Removed calls to 'debug_dma_alloc_coherent' (function is undefined)
Defining function dmi_get_system_info as symbolic
Defining function strstr as symbolic
Defining function dma_pool_create as symbolic
Removed calls to 'synchronize_irq' (function is undefined)
Defining function snprintf as symbolic
Defining function usb_hcd_irq as symbolic
Defining function request_threaded_irq as symbolic
Defining function pci_enable_msi_range as symbolic
Defining function __bitmap_weight as symbolic
Defining function pci_set_mwi as symbolic
Defining function pci_bus_read_config_byte as symbolic
Defining function dma_set_mask as symbolic
Defining function dma_supported as symbolic
Defining function del_timer as symbolic
Removed calls to 'clk_unprepare' (function is undefined)
Removed calls to 'clk_disable' (function is undefined)
Removed calls to 'iounmap' (function is undefined)
Removed calls to '__release_region' (function is undefined)
Defining function usb_disabled as symbolic
Defining function platform_get_irq as symbolic
Defining function platform_get_resource as symbolic
Defining function usb_create_hcd as symbolic
Defining function __request_region as symbolic
Defining function ioremap_nocache as symbolic
Defining function devm_clk_get as symbolic
Defining function device_wakeup_enable as symbolic
Defining function clk_prepare as symbolic
Defining function clk_enable as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'pci_unregister_driver' (function is undefined)
Removed calls to 'platform_driver_unregister' (function is undefined)
Removed calls to 'ldv_check_final_state' (function is undefined)
Removed calls to 'usb_hcd_pci_shutdown' (function is undefined)
Defining function ldv_suspend_late_8 as symbolic
Defining function ldv_restore_early_8 as symbolic
Defining function ldv_resume_early_8 as symbolic
Defining function ldv_thaw_early_8 as symbolic
Defining function ldv_resume_noirq_8 as symbolic
Defining function ldv_freeze_noirq_8 as symbolic
Defining function ldv_prepare_8 as symbolic
Defining function ldv_freeze_late_8 as symbolic
Defining function ldv_thaw_noirq_8 as symbolic
Defining function ldv_poweroff_noirq_8 as symbolic
Defining function ldv_poweroff_late_8 as symbolic
Defining function ldv_restore_noirq_8 as symbolic
Defining function ldv_suspend_noirq_8 as symbolic
Defining function ldv_complete_8 as symbolic
Defining function ftrace_raw_output_prep as symbolic
Defining function trace_seq_printf as symbolic
Defining function trace_event_raw_init as symbolic
Defining function ftrace_event_reg as symbolic
Defining function trace_define_field as symbolic
Defining function __platform_driver_register as symbolic
Defining function __pci_register_driver as symbolic
Defining function kmem_cache_alloc as symbolic
Defining function ldv_some_page as symbolic
Linked our definitions to these undefined functions:
  strlen
  __kmalloc
  __memcpy
  kfree
  __VERIFIER_assume
  __VERIFIER_calloc0
  __VERIFIER_error
  __VERIFIER_exit
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
  __VERIFIER_nondet_pointer_named
  __VERIFIER_nondet_uint_named
  __VERIFIER_nondet_ulong_named
INFO: After-slicing optimizations and preparation time: 1.74239897728
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 745 364 3269 24985
INFO: Starting verification
KLEE: WARNING ONCE: function "xhci_pci_probe" has inline asm
KLEE: WARNING ONCE: function "xhci_irq" has inline asm
KLEE: WARNING ONCE: function "xhci_run" has inline asm
KLEE: WARNING ONCE: function "xhci_stop" has inline asm
KLEE: WARNING ONCE: function "xhci_shutdown" has inline asm
KLEE: WARNING ONCE: function "xhci_get_frame" has inline asm
KLEE: WARNING ONCE: function "xhci_urb_enqueue" has inline asm
KLEE: WARNING ONCE: function "xhci_urb_dequeue" has inline asm
KLEE: WARNING ONCE: function "xhci_hub_status_data" has inline asm
KLEE: WARNING ONCE: function "xhci_hub_control" has inline asm
KLEE: WARNING ONCE: function "xhci_bus_suspend" has inline asm
KLEE: WARNING ONCE: function "xhci_bus_resume" has inline asm
KLEE: WARNING ONCE: function "xhci_free_streams" has inline asm
KLEE: WARNING ONCE: function "xhci_add_endpoint" has inline asm
KLEE: WARNING ONCE: function "xhci_drop_endpoint" has inline asm
KLEE: WARNING ONCE: function "xhci_set_usb2_hardware_lpm" has inline asm
KLEE: WARNING ONCE: function "trace_xhci_dbg_context_change" has inline asm
KLEE: WARNING ONCE: function "xhci_configure_endpoint" has inline asm
KLEE: WARNING ONCE: function "trace_xhci_dbg_quirks" has inline asm
KLEE: WARNING ONCE: function "xhci_ring_cmd_db" has inline asm
KLEE: WARNING ONCE: function "prepare_ring" has inline asm
KLEE: WARNING ONCE: function "queue_trb" has inline asm
KLEE: WARNING ONCE: function "trace_xhci_dbg_ring_expansion___0" has inline asm
KLEE: WARNING ONCE: function "rcu_read_lock_sched_held" has inline asm
KLEE: WARNING ONCE: function "arch_local_save_flags" has inline asm
KLEE: WARNING ONCE: function "trace_xhci_dbg_address" has inline asm
KLEE: WARNING ONCE: function "xhci_endpoint_init" has inline asm
KLEE: WARNING ONCE: function "xhci_microframes_to_exponent" has inline asm
KLEE: WARNING ONCE: function "xhci_ring_device" has inline asm
KLEE: WARNING ONCE: function "trace_xhci_dbg_quirks___1" has inline asm
KLEE: WARNING ONCE: function "trace_xhci_dbg_reset_ep" has inline asm
KLEE: WARNING ONCE: function "trace_xhci_dbg_cancel_urb" has inline asm
KLEE: WARNING ONCE: function "xhci_halt" has inline asm
KLEE: WARNING ONCE: function "xhci_reset" has inline asm
KLEE: WARNING ONCE: function "trace_xhci_dbg_init" has inline asm
KLEE: WARNING ONCE: function "xhci_print_ir_set" has inline asm
KLEE: WARNING ONCE: function "trace_xhci_dbg_init___0" has inline asm
KLEE: WARNING ONCE: function "xhci_resume" has inline asm
KLEE: WARNING ONCE: function "xhci_set_cmd_ring_deq" has inline asm
KLEE: WARNING ONCE: function "compliance_mode_recovery" has inline asm
KLEE: WARNING ONCE: function "xhci_mem_init" has inline asm
KLEE: WARNING ONCE: function "xhci_suspend" has inline asm
KLEE: WARNING ONCE: function "handle_cmd_completion" has inline asm
KLEE: WARNING ONCE: function "trace_xhci_dbg_quirks___0" has inline asm
KLEE: WARNING ONCE: function "ring_doorbell_for_active_rings" has inline asm
KLEE: WARNING ONCE: function "trace_xhci_dbg_cancel_urb___0" has inline asm
KLEE: WARNING ONCE: function "trace_xhci_dbg_reset_ep___0" has inline asm
KLEE: WARNING ONCE: function "xhci_last_valid_endpoint" has inline asm
KLEE: WARNING ONCE: function "xhci_setup_streams_ep_input_ctx" has inline asm
KLEE: WARNING ONCE: function "trace_xhci_dbg_context_change___0" has inline asm
KLEE: WARNING ONCE: function "xhci_stop_endpoint_command_watchdog" has inline asm
KLEE: WARNING ONCE: function "xhci_quiesce" has inline asm
KLEE: WARNING ONCE: function "xhci_handshake" has inline asm
KLEE: WARNING ONCE: function "xhci_set_link_state" has inline asm
KLEE: WARNING ONCE: function "xhci_test_and_clear_bit" has inline asm
KLEE: WARNING ONCE: function "xhci_ring_ep_doorbell" has inline asm
KLEE: WARNING ONCE: function "xhci_cleanup_stalled_ring" has inline asm
KLEE: WARNING ONCE: function "giveback_first_trb" has inline asm
KLEE: WARNING ONCE: function "xhci_queue_isoc_tx_prepare" has inline asm
KLEE: WARNING ONCE: function "xhci_dbg_cmd_ptrs" has inline asm
KLEE: WARNING ONCE: function "xhci_dbg_regs" has inline asm
KLEE: WARNING ONCE: function "xhci_print_run_regs" has inline asm
KLEE: WARNING ONCE: function "xhci_handle_command_timeout" has inline asm
KLEE: WARNING ONCE: function "xhci_print_registers" has inline asm
KLEE: WARNING ONCE: function "xhci_mvebu_mbus_init_quirk" has inline asm
KLEE: WARNING ONCE: function "ldv_main_exported_11" has inline asm
KLEE: WARNING ONCE: function "ldv_main_exported_9" has inline asm
KLEE: WARNING: undefined reference to function: __VERIFIER_nondet_u16_named
KLEE: WARNING: undefined reference to function: usb_hcd_pci_shutdown
KLEE: ERROR: /tmp/symbiotic-Wq_6JE/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--host--xhci-hcd.ko-entry_point_true-unreach-call.cil.out.c:12893: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_f871e165-7c9b-4968-8d01-4d4344a0047b/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: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 20117 states (over memory cap)
KLEE: WARNING: killing 17646 states (over memory cap)
KLEE: WARNING: killing 16728 states (over memory cap)
KLEE: WARNING: killing 17046 states (over memory cap)
KLEE: WARNING: killing 17364 states (over memory cap)
KLEE: WARNING: killing 17036 states (over memory cap)
KLEE: WARNING: killing 16853 states (over memory cap)
KLEE: WARNING: killing 17540 states (over memory cap)
KLEE: WARNING: killing 16859 states (over memory cap)
KLEE: WARNING: killing 17329 states (over memory cap)
KLEE: WARNING: killing 18295 states (over memory cap)
KLEE: WARNING: killing 19551 states (over memory cap)
KLEE: WARNING: killing 18241 states (over memory cap)
KLEE: WARNING: killing 18707 states (over memory cap)
KLEE: WARNING: killing 19820 states (over memory cap)
KLEE: WARNING: killing 20867 states (over memory cap)
KLEE: WARNING: killing 20132 states (over memory cap)
KLEE: WARNING: killing 20328 states (over memory cap)
KLEE: WARNING: killing 20727 states (over memory cap)
KLEE: WARNING: killing 19782 states (over memory cap)
KLEE: WARNING: killing 19908 states (over memory cap)
KLEE: WARNING: killing 19237 states (over memory cap)
KLEE: WARNING: killing 18083 states (over memory cap)
KLEE: WARNING: killing 18833 states (over memory cap)
KLEE: WARNING: killing 18031 states (over memory cap)
KLEE: WARNING: killing 18568 states (over memory cap)
KLEE: WARNING: killing 18679 states (over memory cap)
KLEE: WARNING: killing 18019 states (over memory cap)
KLEE: WARNING: killing 18840 states (over memory cap)
KLEE: WARNING: killing 19019 states (over memory cap)
KLEE: WARNING: killing 18159 states (over memory cap)
KLEE: WARNING ONCE: calling external: __VERIFIER_nondet_u16_named(72559792) at /tmp/symbiotic-Wq_6JE/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--host--xhci-hcd.ko-entry_point_true-unreach-call.cil.out.c:27704
KLEE: ERROR: /tmp/symbiotic-Wq_6JE/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--host--xhci-hcd.ko-entry_point_true-unreach-call.cil.out.c:27702: failed external call: __VERIFIER_nondet_u16_named
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Wq_6JE/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--host--xhci-hcd.ko-entry_point_true-unreach-call.cil.out.c:26585: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 18827 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-Wq_6JE/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--host--xhci-hcd.ko-entry_point_true-unreach-call.cil.out.c:29264: failed external call: __VERIFIER_nondet_u16_named
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 18945 states (over memory cap)
KLEE: WARNING: killing 18771 states (over memory cap)
KLEE: WARNING: killing 19721 states (over memory cap)
KLEE: WARNING: killing 19214 states (over memory cap)
KLEE: WARNING: killing 18567 states (over memory cap)
KLEE: WARNING: killing 19646 states (over memory cap)
KLEE: WARNING: killing 19145 states (over memory cap)
KLEE: WARNING: killing 19609 states (over memory cap)
KLEE: WARNING: killing 18544 states (over memory cap)
KLEE: WARNING: killing 19073 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-Wq_6JE/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--host--xhci-hcd.ko-entry_point_true-unreach-call.cil.out.c:27025: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 19393 states (over memory cap)
KLEE: WARNING: killing 19434 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-Wq_6JE/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--host--xhci-hcd.ko-entry_point_true-unreach-call.cil.out.c:26640: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 20107 states (over memory cap)
KLEE: WARNING: killing 18777 states (over memory cap)
KLEE: WARNING: killing 19991 states (over memory cap)
KLEE: WARNING: killing 17838 states (over memory cap)
KLEE: WARNING: killing 18155 states (over memory cap)
KLEE: WARNING: killing 18476 states (over memory cap)
KLEE: WARNING: killing 18860 states (over memory cap)
KLEE: WARNING: killing 18910 states (over memory cap)
KLEE: WARNING: killing 17861 states (over memory cap)
KLEE: WARNING: killing 19129 states (over memory cap)
KLEE: WARNING: killing 19184 states (over memory cap)
KLEE: WARNING: killing 18746 states (over memory cap)
KLEE: WARNING: killing 20226 states (over memory cap)
KLEE: WARNING: killing 18780 states (over memory cap)
KLEE: WARNING: killing 18286 states (over memory cap)
KLEE: WARNING: killing 19549 states (over memory cap)
KLEE: WARNING: killing 19864 states (over memory cap)
KLEE: WARNING: killing 18568 states (over memory cap)
KLEE: WARNING: killing 18071 states (over memory cap)
KLEE: WARNING: killing 18719 states (over memory cap)
KLEE: WARNING: killing 19844 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-Wq_6JE/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--host--xhci-hcd.ko-entry_point_true-unreach-call.cil.out.c:27470: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 19218 states (over memory cap)
KLEE: WARNING: killing 18597 states (over memory cap)
KLEE: WARNING: killing 19308 states (over memory cap)
KLEE: WARNING: killing 18210 states (over memory cap)
KLEE: WARNING: killing 18658 states (over memory cap)
KLEE: WARNING: killing 19441 states (over memory cap)
KLEE: WARNING: killing 19292 states (over memory cap)
KLEE: WARNING: killing 18675 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-Wq_6JE/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--host--xhci-hcd.ko-entry_point_true-unreach-call.cil.out.c:26612: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 18650 states (over memory cap)
KLEE: WARNING: killing 19234 states (over memory cap)
KLEE: WARNING: killing 19412 states (over memory cap)
KLEE: WARNING: killing 19995 states (over memory cap)
KLEE: WARNING: killing 19048 states (over memory cap)
KLEE: WARNING: killing 19035 states (over memory cap)
KLEE: WARNING: killing 18285 states (over memory cap)
KLEE: WARNING: killing 19053 states (over memory cap)
KLEE: WARNING: killing 18768 states (over memory cap)
KLEE: WARNING: killing 18486 states (over memory cap)
KLEE: WARNING: killing 18406 states (over memory cap)
KLEE: WARNING: killing 18982 states (over memory cap)
KLEE: WARNING: killing 19628 states (over memory cap)
KLEE: WARNING: killing 19073 states (over memory cap)
KLEE: WARNING: killing 18733 states (over memory cap)
KLEE: WARNING: killing 18911 states (over memory cap)
KLEE: WARNING: killing 18956 states (over memory cap)
KLEE: WARNING: killing 19141 states (over memory cap)
KLEE: WARNING: killing 18333 states (over memory cap)
KLEE: WARNING: killing 19101 states (over memory cap)
KLEE: WARNING: killing 18500 states (over memory cap)
KLEE: WARNING: killing 18608 states (over memory cap)
KLEE: WARNING: killing 19443 states (over memory cap)
KLEE: WARNING: killing 19162 states (over memory cap)
KLEE: WARNING: killing 19794 states (over memory cap)
KLEE: WARNING: killing 19454 states (over memory cap)
KLEE: WARNING: killing 18654 states (over memory cap)
KLEE: WARNING: killing 20001 states (over memory cap)
KLEE: WARNING: killing 19791 states (over memory cap)
KLEE: WARNING: killing 19390 states (over memory cap)
KLEE: WARNING: killing 18924 states (over memory cap)
KLEE: WARNING: killing 18190 states (over memory cap)
KLEE: WARNING: killing 18489 states (over memory cap)
KLEE: WARNING: killing 18726 states (over memory cap)
KLEE: WARNING: killing 18847 states (over memory cap)
KLEE: WARNING: killing 19080 states (over memory cap)
KLEE: WARNING: killing 19264 states (over memory cap)
KLEE: WARNING: killing 18917 states (over memory cap)
KLEE: WARNING: killing 19228 states (over memory cap)
KLEE: WARNING: killing 18880 states (over memory cap)
KLEE: WARNING: killing 19824 states (over memory cap)
KLEE: WARNING: killing 18585 states (over memory cap)
KLEE: WARNING: killing 19152 states (over memory cap)
KLEE: WARNING: killing 19008 states (over memory cap)
KLEE: WARNING: killing 19374 states (over memory cap)
KLEE: WARNING: killing 18720 states (over memory cap)
KLEE: WARNING: killing 18446 states (over memory cap)
KLEE: WARNING: killing 19388 states (over memory cap)
KLEE: WARNING: killing 19245 states (over memory cap)
KLEE: WARNING: killing 19418 states (over memory cap)
KLEE: WARNING: killing 18512 states (over memory cap)
KLEE: WARNING: killing 18557 states (over memory cap)
KLEE: WARNING: killing 19243 states (over memory cap)
KLEE: WARNING: killing 19034 states (over memory cap)
KLEE: WARNING: killing 18832 states (over memory cap)
KLEE: WARNING: killing 18433 states (over memory cap)
KLEE: WARNING: killing 19495 states (over memory cap)
KLEE: WARNING: killing 19168 states (over memory cap)
KLEE: WARNING: killing 18447 states (over memory cap)
KLEE: WARNING: killing 19570 states (over memory cap)
KLEE: WARNING: killing 19368 states (over memory cap)
KLEE: WARNING: killing 19223 states (over memory cap)
KLEE: WARNING: killing 19713 states (over memory cap)
KLEE: WARNING: killing 19075 states (over memory cap)
KLEE: WARNING: killing 19061 states (over memory cap)
KLEE: WARNING: killing 18219 states (over memory cap)
KLEE: WARNING: killing 18701 states (over memory cap)
KLEE: WARNING: killing 18811 states (over memory cap)
KLEE: WARNING: killing 19741 states (over memory cap)
KLEE: WARNING: killing 19533 states (over memory cap)
KLEE: WARNING: killing 19519 states (over memory cap)
KLEE: WARNING: killing 18750 states (over memory cap)
KLEE: WARNING: killing 19670 states (over memory cap)
KLEE: WARNING: killing 17838 states (over memory cap)
KLEE: WARNING: killing 18562 states (over memory cap)
