smtinterpol-NPE-LAInterpolor-color.smt2

(set-option :produce-interpolants true)
(set-option :produce-models true)
(set-option :produce-unsat-cores true)
(set-logic QF_UFLIRA)
(push 1)
(declare-fun |__ADDRESS_OF_main::tmp___1| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_main::tmp___0| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_main::tmp| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_main::ldv_s_ath6kl_sdio_driver_sdio_driver| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_main::res_ath6kl_sdio_probe_41| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_main::var_ath6kl_sdio_probe_41_p1| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_main::var_group4| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_main::var_ath6kl_sdio_bmi_write_36_p2| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_main::var_ath6kl_sdio_bmi_write_36_p1| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_main::var_ath6kl_sdio_bmi_read_37_p2| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_main::var_ath6kl_sdio_bmi_read_37_p1| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_main::var_ath6kl_sdio_diag_write32_33_p2| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_main::var_ath6kl_sdio_diag_write32_33_p1| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_main::var_ath6kl_sdio_diag_read32_32_p2| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_main::var_ath6kl_sdio_diag_read32_32_p1| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_main::var_group3| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_main::var_group2| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_main::var_ath6kl_sdio_write_async_18_p5| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_main::var_ath6kl_sdio_write_async_18_p4| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_main::var_ath6kl_sdio_write_async_18_p3| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_main::var_ath6kl_sdio_write_async_18_p2| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_main::var_ath6kl_sdio_write_async_18_p1| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_main::var_ath6kl_sdio_read_write_sync_12_p4| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_main::var_ath6kl_sdio_read_write_sync_12_p3| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_main::var_ath6kl_sdio_read_write_sync_12_p2| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_main::var_ath6kl_sdio_read_write_sync_12_p1| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_main::var_group1| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun __ADDRESS_OF_ldv_sdio_element () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun __ADDRESS_OF_ath6kl_sdio_devices () Int)
(declare-fun __ADDRESS_OF_ath6kl_sdio_driver () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun __ADDRESS_OF_ath6kl_sdio_pm_ops () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun __ADDRESS_OF_ath6kl_sdio_ops () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun __ADDRESS_OF___tracepoint_ath6kl_sdio_scat () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun __ADDRESS_OF___tracepoint_ath6kl_sdio () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun __ADDRESS_OF_rcu_sched_lock_map () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun __ADDRESS_OF_jiffies () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun __ADDRESS_OF_debug_locks () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun __ADDRESS_OF_pv_irq_ops () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |main::ldv_s_ath6kl_sdio_driver_sdio_driver@3| () Int)
(declare-fun ldv_sdio_element@2 () Int)
(declare-fun *unsigned_short_int@1 (Int ) Int)
(assert (! (let ((.cse0 (+ __ADDRESS_OF_rcu_sched_lock_map 44)) (.cse1 (+ __ADDRESS_OF___tracepoint_ath6kl_sdio 36)) (.cse2 (+ __ADDRESS_OF___tracepoint_ath6kl_sdio_scat 36)) (.cse3 (+ __ADDRESS_OF_ath6kl_sdio_ops 176)) (.cse4 (+ __ADDRESS_OF_ath6kl_sdio_pm_ops 184)) (.cse5 (+ __ADDRESS_OF_ath6kl_sdio_devices 65))) (and (= (*unsigned_short_int@1 (+ (+ __ADDRESS_OF_ath6kl_sdio_devices (* 13 4)) 3)) 0) (= ldv_sdio_element@2 0) (= |main::ldv_s_ath6kl_sdio_driver_sdio_driver@3| 0) (= (__BASE_ADDRESS_OF__ __ADDRESS_OF_pv_irq_ops) __ADDRESS_OF_pv_irq_ops) (= (__BASE_ADDRESS_OF__ __ADDRESS_OF_debug_locks) __ADDRESS_OF_debug_locks) (= (__BASE_ADDRESS_OF__ __ADDRESS_OF_rcu_sched_lock_map) __ADDRESS_OF_rcu_sched_lock_map) (> __ADDRESS_OF_rcu_sched_lock_map 0) (= (__BASE_ADDRESS_OF__ __ADDRESS_OF_jiffies) __ADDRESS_OF_jiffies) (= (__BASE_ADDRESS_OF__ __ADDRESS_OF___tracepoint_ath6kl_sdio) __ADDRESS_OF___tracepoint_ath6kl_sdio) (> .cse0 0) (>= __ADDRESS_OF___tracepoint_ath6kl_sdio .cse0) (= (__BASE_ADDRESS_OF__ __ADDRESS_OF___tracepoint_ath6kl_sdio_scat) __ADDRESS_OF___tracepoint_ath6kl_sdio_scat) (> .cse1 0) (>= __ADDRESS_OF___tracepoint_ath6kl_sdio_scat .cse1) (= (__BASE_ADDRESS_OF__ __ADDRESS_OF_ath6kl_sdio_ops) __ADDRESS_OF_ath6kl_sdio_ops) (> .cse2 0) (>= __ADDRESS_OF_ath6kl_sdio_ops .cse2) (= (__BASE_ADDRESS_OF__ __ADDRESS_OF_ath6kl_sdio_pm_ops) __ADDRESS_OF_ath6kl_sdio_pm_ops) (> .cse3 0) (>= __ADDRESS_OF_ath6kl_sdio_pm_ops .cse3) (= (__BASE_ADDRESS_OF__ __ADDRESS_OF_ath6kl_sdio_devices) __ADDRESS_OF_ath6kl_sdio_devices) (> .cse4 0) (>= __ADDRESS_OF_ath6kl_sdio_devices .cse4) (= (__BASE_ADDRESS_OF__ __ADDRESS_OF_ath6kl_sdio_driver) __ADDRESS_OF_ath6kl_sdio_driver) (> .cse5 0) (>= __ADDRESS_OF_ath6kl_sdio_driver .cse5) (= (__BASE_ADDRESS_OF__ __ADDRESS_OF_ldv_sdio_element) __ADDRESS_OF_ldv_sdio_element) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_main::var_group1|) |__ADDRESS_OF_main::var_group1|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_main::var_ath6kl_sdio_read_write_sync_12_p1|) |__ADDRESS_OF_main::var_ath6kl_sdio_read_write_sync_12_p1|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_main::var_ath6kl_sdio_read_write_sync_12_p2|) |__ADDRESS_OF_main::var_ath6kl_sdio_read_write_sync_12_p2|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_main::var_ath6kl_sdio_read_write_sync_12_p3|) |__ADDRESS_OF_main::var_ath6kl_sdio_read_write_sync_12_p3|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_main::var_ath6kl_sdio_read_write_sync_12_p4|) |__ADDRESS_OF_main::var_ath6kl_sdio_read_write_sync_12_p4|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_main::var_ath6kl_sdio_write_async_18_p1|) |__ADDRESS_OF_main::var_ath6kl_sdio_write_async_18_p1|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_main::var_ath6kl_sdio_write_async_18_p2|) |__ADDRESS_OF_main::var_ath6kl_sdio_write_async_18_p2|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_main::var_ath6kl_sdio_write_async_18_p3|) |__ADDRESS_OF_main::var_ath6kl_sdio_write_async_18_p3|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_main::var_ath6kl_sdio_write_async_18_p4|) |__ADDRESS_OF_main::var_ath6kl_sdio_write_async_18_p4|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_main::var_ath6kl_sdio_write_async_18_p5|) |__ADDRESS_OF_main::var_ath6kl_sdio_write_async_18_p5|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_main::var_group2|) |__ADDRESS_OF_main::var_group2|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_main::var_group3|) |__ADDRESS_OF_main::var_group3|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_main::var_ath6kl_sdio_diag_read32_32_p1|) |__ADDRESS_OF_main::var_ath6kl_sdio_diag_read32_32_p1|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_main::var_ath6kl_sdio_diag_read32_32_p2|) |__ADDRESS_OF_main::var_ath6kl_sdio_diag_read32_32_p2|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_main::var_ath6kl_sdio_diag_write32_33_p1|) |__ADDRESS_OF_main::var_ath6kl_sdio_diag_write32_33_p1|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_main::var_ath6kl_sdio_diag_write32_33_p2|) |__ADDRESS_OF_main::var_ath6kl_sdio_diag_write32_33_p2|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_main::var_ath6kl_sdio_bmi_read_37_p1|) |__ADDRESS_OF_main::var_ath6kl_sdio_bmi_read_37_p1|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_main::var_ath6kl_sdio_bmi_read_37_p2|) |__ADDRESS_OF_main::var_ath6kl_sdio_bmi_read_37_p2|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_main::var_ath6kl_sdio_bmi_write_36_p1|) |__ADDRESS_OF_main::var_ath6kl_sdio_bmi_write_36_p1|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_main::var_ath6kl_sdio_bmi_write_36_p2|) |__ADDRESS_OF_main::var_ath6kl_sdio_bmi_write_36_p2|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_main::var_group4|) |__ADDRESS_OF_main::var_group4|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_main::var_ath6kl_sdio_probe_41_p1|) |__ADDRESS_OF_main::var_ath6kl_sdio_probe_41_p1|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_main::res_ath6kl_sdio_probe_41|) |__ADDRESS_OF_main::res_ath6kl_sdio_probe_41|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_main::ldv_s_ath6kl_sdio_driver_sdio_driver|) |__ADDRESS_OF_main::ldv_s_ath6kl_sdio_driver_sdio_driver|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_main::tmp|) |__ADDRESS_OF_main::tmp|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_main::tmp___0|) |__ADDRESS_OF_main::tmp___0|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_main::tmp___1|) |__ADDRESS_OF_main::tmp___1|))) :named term_2019))
(push 1)
(declare-fun |ath6kl_sdio_init::__retval__@2| () Int)
(declare-fun |main::tmp@3| () Int)
(declare-fun |ath6kl_sdio_init::ret@3| () Int)
(declare-fun sdio_register_driver (Int ) Int)
(declare-fun __ADDRESS_OF_ath6kl_sdio_driver () Int)
(declare-fun |__ADDRESS_OF_ath6kl_sdio_init::ret| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(assert (! (and (let ((.cse0 (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_ath6kl_sdio_init::ret|) |__ADDRESS_OF_ath6kl_sdio_init::ret|)) (.cse1 (= |ath6kl_sdio_init::ret@3| (sdio_register_driver __ADDRESS_OF_ath6kl_sdio_driver))) (.cse2 (= |ath6kl_sdio_init::ret@3| 0))) (or (and .cse0 .cse1 (not .cse2)) (and .cse0 .cse1 .cse2))) (= |ath6kl_sdio_init::__retval__@2| |ath6kl_sdio_init::ret@3|) (= |main::tmp@3| |ath6kl_sdio_init::__retval__@2|)) :named term_2020))
(push 1)
(declare-fun |main::tmp@3| () Int)
(assert (! (= |main::tmp@3| 0) :named term_2021))
(push 1)
(declare-fun |main::var_ath6kl_sdio_diag_read32_32_p2@2| () Int)
(declare-fun |ath6kl_sdio_diag_read32::data@2| () Int)
(declare-fun |main::var_ath6kl_sdio_diag_read32_32_p1@2| () Int)
(declare-fun |ath6kl_sdio_diag_read32::address@2| () Int)
(declare-fun |main::var_group1@2| () Int)
(declare-fun |ath6kl_sdio_diag_read32::ar@2| () Int)
(declare-fun |main::tmp___0@3| () Int)
(declare-fun |main::tmp___1@3| () Int)
(declare-fun |main::ldv_s_ath6kl_sdio_driver_sdio_driver@3| () Int)
(assert (! (and (let ((.cse0 (= |main::tmp___1@3| 0))) (or (and .cse0 (not (= |main::ldv_s_ath6kl_sdio_driver_sdio_driver@3| 0))) (not .cse0))) (not (= |main::tmp___0@3| 0)) (not (= |main::tmp___0@3| 1)) (not (= |main::tmp___0@3| 2)) (not (= |main::tmp___0@3| 3)) (not (= |main::tmp___0@3| 4)) (not (= |main::tmp___0@3| 5)) (not (= |main::tmp___0@3| 6)) (not (= |main::tmp___0@3| 7)) (not (= |main::tmp___0@3| 8)) (not (= |main::tmp___0@3| 9)) (not (= |main::tmp___0@3| 10)) (= |main::tmp___0@3| 11) (= |ath6kl_sdio_diag_read32::ar@2| |main::var_group1@2|) (= |ath6kl_sdio_diag_read32::address@2| |main::var_ath6kl_sdio_diag_read32_32_p1@2|) (= |ath6kl_sdio_diag_read32::data@2| |main::var_ath6kl_sdio_diag_read32_32_p2@2|)) :named term_2022))
(push 1)
(declare-fun __ADDRESS_OF_ath6kl_sdio_driver () Int)
(declare-fun |__ADDRESS_OF_ath6kl_set_addrwin_reg::addr| () Int)
(declare-fun |ath6kl_sdio_diag_read32::address@2| () Int)
(declare-fun |ath6kl_set_addrwin_reg::addr@2| () Int)
(declare-fun |ath6kl_set_addrwin_reg::reg_addr@2| () Int)
(declare-fun |ath6kl_sdio_diag_read32::ar@2| () Int)
(declare-fun |ath6kl_set_addrwin_reg::ar@2| () Int)
(declare-fun |__ADDRESS_OF_ath6kl_sdio_diag_read32::status| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(assert (! (let ((.cse0 (+ __ADDRESS_OF_ath6kl_sdio_driver 145))) (and (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_ath6kl_sdio_diag_read32::status|) |__ADDRESS_OF_ath6kl_sdio_diag_read32::status|) (= |ath6kl_set_addrwin_reg::ar@2| |ath6kl_sdio_diag_read32::ar@2|) (= |ath6kl_set_addrwin_reg::reg_addr@2| 1148) (= |ath6kl_set_addrwin_reg::addr@2| |ath6kl_sdio_diag_read32::address@2|) (> .cse0 0) (>= |__ADDRESS_OF_ath6kl_set_addrwin_reg::addr| .cse0))) :named term_2023))
(push 1)
(declare-fun |__ADDRESS_OF_ath6kl_set_addrwin_reg::i| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_ath6kl_set_addrwin_reg::addr| () Int)
(declare-fun |__ADDRESS_OF_ath6kl_set_addrwin_reg::addr_val| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_ath6kl_set_addrwin_reg::status| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |ath6kl_set_addrwin_reg::i@3| () Int)
(assert (! (let ((.cse0 (+ |__ADDRESS_OF_ath6kl_set_addrwin_reg::addr| 4))) (and (= |ath6kl_set_addrwin_reg::i@3| 1) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_ath6kl_set_addrwin_reg::status|) |__ADDRESS_OF_ath6kl_set_addrwin_reg::status|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_ath6kl_set_addrwin_reg::addr_val|) |__ADDRESS_OF_ath6kl_set_addrwin_reg::addr_val|) (> .cse0 0) (>= |__ADDRESS_OF_ath6kl_set_addrwin_reg::addr_val| .cse0) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_ath6kl_set_addrwin_reg::i|) |__ADDRESS_OF_ath6kl_set_addrwin_reg::i|))) :named term_2024))
(push 1)
(declare-fun |ath6kl_sdio_read_write_sync::request@2| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::len@2| () Int)
(declare-fun |__ADDRESS_OF_ath6kl_set_addrwin_reg::addr_val| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::buf@2| () Int)
(declare-fun |ath6kl_set_addrwin_reg::i@3| () Int)
(declare-fun |ath6kl_set_addrwin_reg::reg_addr@2| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::addr@2| () Int)
(declare-fun |ath6kl_set_addrwin_reg::ar@2| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::ar@2| () Int)
(declare-fun |ath6kl_set_addrwin_reg::addr@2| () Int)
(declare-fun *unsigned_int@1 (Int ) Int)
(declare-fun |__ADDRESS_OF_ath6kl_set_addrwin_reg::addr| () Int)
(assert (! (and (<= |ath6kl_set_addrwin_reg::i@3| 3) (= (*unsigned_int@1 |__ADDRESS_OF_ath6kl_set_addrwin_reg::addr|) |ath6kl_set_addrwin_reg::addr@2|) (= |ath6kl_sdio_read_write_sync::ar@2| |ath6kl_set_addrwin_reg::ar@2|) (= |ath6kl_sdio_read_write_sync::addr@2| (+ |ath6kl_set_addrwin_reg::reg_addr@2| |ath6kl_set_addrwin_reg::i@3|)) (= |ath6kl_sdio_read_write_sync::buf@2| |__ADDRESS_OF_ath6kl_set_addrwin_reg::addr_val|) (= |ath6kl_sdio_read_write_sync::len@2| 4) (= |ath6kl_sdio_read_write_sync::request@2| 338)) :named term_2025))
(push 1)
(declare-fun |ath6kl_sdio_read_write_sync::ar@2| () Int)
(declare-fun |ath6kl_sdio_priv::ar@2| () Int)
(declare-fun |__ADDRESS_OF_ath6kl_sdio_read_write_sync::tmp___0| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_ath6kl_sdio_read_write_sync::bounced| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_ath6kl_sdio_read_write_sync::ret| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_ath6kl_sdio_read_write_sync::tbuf| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_ath6kl_sdio_read_write_sync::tmp| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_ath6kl_set_addrwin_reg::addr_val| () Int)
(declare-fun |__ADDRESS_OF_ath6kl_sdio_read_write_sync::ar_sdio| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(assert (! (let ((.cse0 (+ |__ADDRESS_OF_ath6kl_set_addrwin_reg::addr_val| 4))) (and (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_ath6kl_sdio_read_write_sync::ar_sdio|) |__ADDRESS_OF_ath6kl_sdio_read_write_sync::ar_sdio|) (> .cse0 0) (>= |__ADDRESS_OF_ath6kl_sdio_read_write_sync::ar_sdio| .cse0) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_ath6kl_sdio_read_write_sync::tmp|) |__ADDRESS_OF_ath6kl_sdio_read_write_sync::tmp|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_ath6kl_sdio_read_write_sync::tbuf|) |__ADDRESS_OF_ath6kl_sdio_read_write_sync::tbuf|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_ath6kl_sdio_read_write_sync::ret|) |__ADDRESS_OF_ath6kl_sdio_read_write_sync::ret|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_ath6kl_sdio_read_write_sync::bounced|) |__ADDRESS_OF_ath6kl_sdio_read_write_sync::bounced|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_ath6kl_sdio_read_write_sync::tmp___0|) |__ADDRESS_OF_ath6kl_sdio_read_write_sync::tmp___0|) (= |ath6kl_sdio_priv::ar@2| |ath6kl_sdio_read_write_sync::ar@2|))) :named term_2026))
(push 1)
(declare-fun |ath6kl_sdio_priv::__retval__@2| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::tmp@3| () Int)
(declare-fun |__ADDRESS_OF_ath6kl_sdio_priv::__CPAchecker_TMP_0| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |ath6kl_sdio_priv::__CPAchecker_TMP_0@2| () Int)
(declare-fun |*(void)*@1| (Int ) Int)
(declare-fun |ath6kl_sdio_priv::ar@2| () Int)
(assert (! (and (= |ath6kl_sdio_priv::__CPAchecker_TMP_0@2| (|*(void)*@1| (+ |ath6kl_sdio_priv::ar@2| 121))) (= |ath6kl_sdio_priv::__retval__@2| |ath6kl_sdio_priv::__CPAchecker_TMP_0@2|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_ath6kl_sdio_priv::__CPAchecker_TMP_0|) |__ADDRESS_OF_ath6kl_sdio_priv::__CPAchecker_TMP_0|) (= |ath6kl_sdio_read_write_sync::tmp@3| |ath6kl_sdio_priv::__retval__@2|)) :named term_2027))
(push 1)
(declare-fun |ath6kl_sdio_read_write_sync::buf@2| () Int)
(declare-fun |buf_needs_bounce::buf@2| () Int)
(declare-fun _&_ (Int Int ) Int)
(declare-fun |ath6kl_sdio_read_write_sync::request@2| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::bounced@3| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::tbuf@3| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::tmp@3| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::ar_sdio@3| () Int)
(assert (! (and (= |ath6kl_sdio_read_write_sync::ar_sdio@3| |ath6kl_sdio_read_write_sync::tmp@3|) (= |ath6kl_sdio_read_write_sync::tbuf@3| 0) (= |ath6kl_sdio_read_write_sync::bounced@3| 0) (= (_&_ |ath6kl_sdio_read_write_sync::request@2| 128) 0) (= |buf_needs_bounce::buf@2| |ath6kl_sdio_read_write_sync::buf@2|)) :named term_2028))
(push 1)
(declare-fun |buf_needs_bounce::__retval__@2| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::tmp___0@3| () Int)
(declare-fun |buf_needs_bounce::tmp___1@3| () Int)
(declare-fun |buf_needs_bounce::tmp___0@3| () Int)
(declare-fun |buf_needs_bounce::tmp@3| () Int)
(declare-fun __virt_addr_valid (Int ) Int)
(declare-fun |buf_needs_bounce::buf@2| () Int)
(declare-fun _&_ (Int Int ) Int)
(declare-fun |__ADDRESS_OF_buf_needs_bounce::tmp___1| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_buf_needs_bounce::tmp___0| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_buf_needs_bounce::tmp| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |buf_needs_bounce::tmp___0@2| () Int)
(declare-fun |buf_needs_bounce::tmp@2| () Int)
(assert (! (and (let ((.cse0 (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_buf_needs_bounce::tmp|) |__ADDRESS_OF_buf_needs_bounce::tmp|)) (.cse1 (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_buf_needs_bounce::tmp___0|) |__ADDRESS_OF_buf_needs_bounce::tmp___0|)) (.cse2 (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_buf_needs_bounce::tmp___1|) |__ADDRESS_OF_buf_needs_bounce::tmp___1|)) (.cse3 (= (_&_ |buf_needs_bounce::buf@2| 3) 0)) (.cse6 (= |buf_needs_bounce::tmp@3| (__virt_addr_valid |buf_needs_bounce::buf@2|))) (.cse7 (= |buf_needs_bounce::tmp@3| 0)) (.cse8 (= |buf_needs_bounce::tmp___0@3| 0)) (.cse4 (= |buf_needs_bounce::tmp___1@3| 1)) (.cse5 (= |buf_needs_bounce::__retval__@2| |buf_needs_bounce::tmp___1@3|))) (or (and .cse0 .cse1 .cse2 (not .cse3) .cse4 .cse5 (= |buf_needs_bounce::tmp@3| |buf_needs_bounce::tmp@2|) (= |buf_needs_bounce::tmp___0@3| |buf_needs_bounce::tmp___0@2|)) (and .cse0 .cse1 .cse2 .cse3 .cse6 (not .cse7) .cse8 (= |buf_needs_bounce::tmp___1@3| 0) .cse5) (and .cse0 .cse1 .cse2 .cse3 .cse6 .cse7 (= |buf_needs_bounce::tmp___0@3| 1) (not .cse8) .cse4 .cse5))) (= |ath6kl_sdio_read_write_sync::tmp___0@3| |buf_needs_bounce::__retval__@2|)) :named term_2029))
(push 1)
(declare-fun |ath6kl_sdio_read_write_sync::len@2| () Int)
(declare-fun |ath6kl_sdio_io::len@2| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::tbuf@4| () Int)
(declare-fun |ath6kl_sdio_io::buf@2| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::addr@2| () Int)
(declare-fun |ath6kl_sdio_io::addr@2| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::request@2| () Int)
(declare-fun |ath6kl_sdio_io::request@2| () Int)
(declare-fun |*(struct_sdio_func)*@1| (Int ) Int)
(declare-fun |ath6kl_sdio_read_write_sync::ar_sdio@3| () Int)
(declare-fun |ath6kl_sdio_io::func@2| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::bounced@4| () Int)
(declare-fun _&_ (Int Int ) Int)
(declare-fun |*(unsigned_char)*@1| (Int ) Int)
(declare-fun |ath6kl_sdio_read_write_sync::__CPAchecker_TMP_0@2| () Int)
(declare-fun |__ADDRESS_OF_ath6kl_sdio_read_write_sync::__CPAchecker_TMP_0| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |ath6kl_sdio_read_write_sync::tmp___0@3| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::bounced@3| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::__CPAchecker_TMP_0@1| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::buf@2| () Int)
(assert (! (and (let ((.cse0 (= |ath6kl_sdio_read_write_sync::tmp___0@3| 0))) (or (and .cse0 (= |ath6kl_sdio_read_write_sync::tbuf@4| |ath6kl_sdio_read_write_sync::buf@2|) (= |ath6kl_sdio_read_write_sync::__CPAchecker_TMP_0@2| |ath6kl_sdio_read_write_sync::__CPAchecker_TMP_0@1|) (= |ath6kl_sdio_read_write_sync::bounced@4| |ath6kl_sdio_read_write_sync::bounced@3|)) (let ((.cse1 (|*(unsigned_char)*@1| (+ |ath6kl_sdio_read_write_sync::ar_sdio@3| 3684)))) (and (not .cse0) (= |ath6kl_sdio_read_write_sync::__CPAchecker_TMP_0@2| .cse1) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_ath6kl_sdio_read_write_sync::__CPAchecker_TMP_0|) |__ADDRESS_OF_ath6kl_sdio_read_write_sync::__CPAchecker_TMP_0|) (not (= |ath6kl_sdio_read_write_sync::__CPAchecker_TMP_0@2| 0)) (= |ath6kl_sdio_read_write_sync::tbuf@4| .cse1) (not (= (_&_ |ath6kl_sdio_read_write_sync::request@2| 2) 0)) (= |ath6kl_sdio_read_write_sync::bounced@4| 1))))) (= |ath6kl_sdio_io::func@2| (|*(struct_sdio_func)*@1| (+ |ath6kl_sdio_read_write_sync::ar_sdio@3| 0))) (= |ath6kl_sdio_io::request@2| |ath6kl_sdio_read_write_sync::request@2|) (= |ath6kl_sdio_io::addr@2| |ath6kl_sdio_read_write_sync::addr@2|) (= |ath6kl_sdio_io::buf@2| |ath6kl_sdio_read_write_sync::tbuf@4|) (= |ath6kl_sdio_io::len@2| |ath6kl_sdio_read_write_sync::len@2|)) :named term_2030))
(push 1)
(declare-fun |ath6kl_sdio_io::func@2| () Int)
(declare-fun |ldv_sdio_claim_host_1::ldv_func_arg1@2| () Int)
(declare-fun |__ADDRESS_OF_ath6kl_sdio_io::ret| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |ath6kl_sdio_io::ret@3| () Int)
(assert (! (and (= |ath6kl_sdio_io::ret@3| 0) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_ath6kl_sdio_io::ret|) |__ADDRESS_OF_ath6kl_sdio_io::ret|) (= |ldv_sdio_claim_host_1::ldv_func_arg1@2| |ath6kl_sdio_io::func@2|)) :named term_2031))
(push 1)
(declare-fun *signed_int@1 (Int ) Int)
(declare-fun |*(struct_mmc_host)*@1| (Int ) Int)
(declare-fun |*(struct_mmc_card)*@1| (Int ) Int)
(declare-fun |ldv_sdio_claim_host_1::ldv_func_arg1@2| () Int)
(declare-fun |ldv_sdio_claim_host::dev_id@2| () Int)
(assert (! (= |ldv_sdio_claim_host::dev_id@2| (*signed_int@1 (+ (|*(struct_mmc_host)*@1| (+ (|*(struct_mmc_card)*@1| (+ |ldv_sdio_claim_host_1::ldv_func_arg1@2| 0)) 0)) 1310))) :named term_2032))
(push 1)
(declare-fun |ldv_sdio_claim_host::dev_id@2| () Int)
(declare-fun ldv_sdio_element@3 () Int)
(declare-fun ldv_sdio_element@2 () Int)
(assert (! (and (= ldv_sdio_element@2 0) (= ldv_sdio_element@3 |ldv_sdio_claim_host::dev_id@2|)) :named term_2033))
(push 1)
(assert (! true :named term_2034))
(push 1)
(declare-fun |ath6kl_sdio_io::func@2| () Int)
(declare-fun |ldv_sdio_writesb_2::ldv_func_arg1@2| () Int)
(declare-fun _&_ (Int Int ) Int)
(declare-fun |ath6kl_sdio_io::request@2| () Int)
(declare-fun |ath6kl_sdio_io::addr@3| () Int)
(declare-fun |ath6kl_sdio_io::addr@4| () Int)
(declare-fun |ath6kl_sdio_io::addr@2| () Int)
(declare-fun _&_ (Int Int ) Int)
(declare-fun |ath6kl_sdio_io::len@2| () Int)
(assert (! (and (let ((.cse0 (let ((.cse4 (<= |ath6kl_sdio_io::addr@2| 8191)) (.cse2 (not (= (_&_ |ath6kl_sdio_io::request@2| 2) 0))) (.cse3 (> |ath6kl_sdio_io::addr@2| 2047))) (or (and .cse2 .cse3 .cse4 (= |ath6kl_sdio_io::addr@3| (+ (- |ath6kl_sdio_io::addr@2| |ath6kl_sdio_io::len@2|) 2048))) (and (or (and .cse2 .cse3 (not .cse4)) (and .cse2 (not .cse3))) (= |ath6kl_sdio_io::addr@3| |ath6kl_sdio_io::addr@2|))))) (.cse1 (= |ath6kl_sdio_io::addr@3| 16384))) (or (and .cse0 .cse1 (= |ath6kl_sdio_io::addr@4| (+ (- |ath6kl_sdio_io::addr@3| |ath6kl_sdio_io::len@2|) 12288))) (and .cse0 (not .cse1) (= |ath6kl_sdio_io::addr@4| |ath6kl_sdio_io::addr@3|)))) (not (= (_&_ |ath6kl_sdio_io::request@2| 256) 0)) (= |ldv_sdio_writesb_2::ldv_func_arg1@2| |ath6kl_sdio_io::func@2|)) :named term_2035))
(push 1)
(declare-fun *signed_int@1 (Int ) Int)
(declare-fun |*(struct_mmc_host)*@1| (Int ) Int)
(declare-fun |*(struct_mmc_card)*@1| (Int ) Int)
(declare-fun |ldv_sdio_writesb_2::ldv_func_arg1@2| () Int)
(declare-fun |ldv_check_context::x@2| () Int)
(assert (! (= |ldv_check_context::x@2| (*signed_int@1 (+ (|*(struct_mmc_host)*@1| (+ (|*(struct_mmc_card)*@1| (+ |ldv_sdio_writesb_2::ldv_func_arg1@2| 0)) 0)) 1310))) :named term_2036))
(push 1)
(declare-fun |ldv_check_context::x@2| () Int)
(declare-fun ldv_sdio_element@3 () Int)
(assert (! (= ldv_sdio_element@3 |ldv_check_context::x@2|) :named term_2037))
(push 1)
(declare-fun |ldv_sdio_writesb_2::__retval__@2| () Int)
(declare-fun |ath6kl_sdio_io::ret@4| () Int)
(assert (! (and (= |ldv_sdio_writesb_2::__retval__@2| 0) (= |ath6kl_sdio_io::ret@4| |ldv_sdio_writesb_2::__retval__@2|)) :named term_2038))
(push 1)
(declare-fun |ath6kl_sdio_io::func@2| () Int)
(declare-fun |ldv_sdio_release_host_6::ldv_func_arg1@2| () Int)
(assert (! (= |ldv_sdio_release_host_6::ldv_func_arg1@2| |ath6kl_sdio_io::func@2|) :named term_2039))
(push 1)
(declare-fun *signed_int@1 (Int ) Int)
(declare-fun |*(struct_mmc_host)*@1| (Int ) Int)
(declare-fun |*(struct_mmc_card)*@1| (Int ) Int)
(declare-fun |ldv_sdio_release_host_6::ldv_func_arg1@2| () Int)
(declare-fun |ldv_sdio_release_host::dev_id@2| () Int)
(assert (! (= |ldv_sdio_release_host::dev_id@2| (*signed_int@1 (+ (|*(struct_mmc_host)*@1| (+ (|*(struct_mmc_card)*@1| (+ |ldv_sdio_release_host_6::ldv_func_arg1@2| 0)) 0)) 1310))) :named term_2040))
(push 1)
(declare-fun ldv_sdio_element@4 () Int)
(declare-fun |ldv_sdio_release_host::dev_id@2| () Int)
(declare-fun ldv_sdio_element@3 () Int)
(assert (! (and (= ldv_sdio_element@3 |ldv_sdio_release_host::dev_id@2|) (= ldv_sdio_element@4 0)) :named term_2041))
(push 1)
(assert (! true :named term_2042))
(push 1)
(declare-fun |ath6kl_sdio_io::len@2| () Int)
(declare-fun |trace_ath6kl_sdio::buf_len@2| () Int)
(declare-fun |ath6kl_sdio_io::buf@2| () Int)
(declare-fun |trace_ath6kl_sdio::buf@2| () Int)
(declare-fun |ath6kl_sdio_io::request@2| () Int)
(declare-fun |trace_ath6kl_sdio::flags@2| () Int)
(declare-fun |ath6kl_sdio_io::addr@4| () Int)
(declare-fun |trace_ath6kl_sdio::addr@2| () Int)
(declare-fun __string__ (Int ) Int)
(declare-fun |ath6kl_sdio_io::__CPAchecker_TMP_1@3| () Int)
(declare-fun _&_ (Int Int ) Int)
(declare-fun __string__ (Int ) Int)
(declare-fun |ath6kl_sdio_io::__CPAchecker_TMP_0@3| () Int)
(declare-fun _&_ (Int Int ) Int)
(declare-fun |__ADDRESS_OF_ath6kl_sdio_io::__CPAchecker_TMP_1| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_ath6kl_sdio_io::__CPAchecker_TMP_0| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(assert (! (and (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_ath6kl_sdio_io::__CPAchecker_TMP_0|) |__ADDRESS_OF_ath6kl_sdio_io::__CPAchecker_TMP_0|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_ath6kl_sdio_io::__CPAchecker_TMP_1|) |__ADDRESS_OF_ath6kl_sdio_io::__CPAchecker_TMP_1|) (not (= (_&_ |ath6kl_sdio_io::request@2| 2) 0)) (= |ath6kl_sdio_io::__CPAchecker_TMP_0@3| (__string__ 12)) (not (= (_&_ |ath6kl_sdio_io::request@2| 256) 0)) (= |ath6kl_sdio_io::__CPAchecker_TMP_1@3| (__string__ 13)) (= |trace_ath6kl_sdio::addr@2| |ath6kl_sdio_io::addr@4|) (= |trace_ath6kl_sdio::flags@2| |ath6kl_sdio_io::request@2|) (= |trace_ath6kl_sdio::buf@2| |ath6kl_sdio_io::buf@2|) (= |trace_ath6kl_sdio::buf_len@2| |ath6kl_sdio_io::len@2|)) :named term_2043))
(push 1)
(declare-fun |__ADDRESS_OF_ath6kl_sdio_read_write_sync::ar_sdio| () Int)
(declare-fun |__ADDRESS_OF_static_key_false::key| () Int)
(declare-fun __tracepoint_ath6kl_sdio$funcs@2 () Int)
(declare-fun |*(struct_tracepoint_func)*@1| (Int ) Int)
(declare-fun __ADDRESS_OF___tracepoint_ath6kl_sdio () Int)
(declare-fun |static_key_false::key@2| () Int)
(declare-fun |__ADDRESS_OF_trace_ath6kl_sdio::tmp___1| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_trace_ath6kl_sdio::tmp___0| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_trace_ath6kl_sdio::tmp| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_trace_ath6kl_sdio::__warned| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_trace_ath6kl_sdio::_________p1| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_trace_ath6kl_sdio::__data| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_trace_ath6kl_sdio::it_func_ptr| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(assert (! (let ((.cse0 (+ |__ADDRESS_OF_ath6kl_sdio_read_write_sync::ar_sdio| 8))) (and (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_trace_ath6kl_sdio::it_func_ptr|) |__ADDRESS_OF_trace_ath6kl_sdio::it_func_ptr|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_trace_ath6kl_sdio::__data|) |__ADDRESS_OF_trace_ath6kl_sdio::__data|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_trace_ath6kl_sdio::_________p1|) |__ADDRESS_OF_trace_ath6kl_sdio::_________p1|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_trace_ath6kl_sdio::__warned|) |__ADDRESS_OF_trace_ath6kl_sdio::__warned|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_trace_ath6kl_sdio::tmp|) |__ADDRESS_OF_trace_ath6kl_sdio::tmp|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_trace_ath6kl_sdio::tmp___0|) |__ADDRESS_OF_trace_ath6kl_sdio::tmp___0|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_trace_ath6kl_sdio::tmp___1|) |__ADDRESS_OF_trace_ath6kl_sdio::tmp___1|) (= |static_key_false::key@2| (+ __ADDRESS_OF___tracepoint_ath6kl_sdio 8)) (= (|*(struct_tracepoint_func)*@1| (+ __ADDRESS_OF___tracepoint_ath6kl_sdio 28)) __tracepoint_ath6kl_sdio$funcs@2) (> .cse0 0) (>= |__ADDRESS_OF_static_key_false::key| .cse0))) :named term_2044))
(push 1)
(declare-fun |__ADDRESS_OF_static_key_false::key| () Int)
(declare-fun |__ADDRESS_OF_atomic_read::v| () Int)
(declare-fun |static_key_false::key@2| () Int)
(declare-fun |atomic_read::v@2| () Int)
(declare-fun |__ADDRESS_OF_static_key_false::tmp___0| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_static_key_false::tmp| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(assert (! (let ((.cse0 (+ |__ADDRESS_OF_static_key_false::key| 8))) (and (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_static_key_false::tmp|) |__ADDRESS_OF_static_key_false::tmp|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_static_key_false::tmp___0|) |__ADDRESS_OF_static_key_false::tmp___0|) (= |atomic_read::v@2| (+ |static_key_false::key@2| 0)) (> .cse0 0) (>= |__ADDRESS_OF_atomic_read::v| .cse0))) :named term_2045))
(push 1)
(declare-fun |atomic_read::__retval__@2| () Int)
(declare-fun |static_key_false::tmp@3| () Int)
(declare-fun *signed_int@1 (Int ) Int)
(declare-fun |atomic_read::v@2| () Int)
(assert (! (and (= |atomic_read::__retval__@2| (*signed_int@1 (+ |atomic_read::v@2| 0))) (= |static_key_false::tmp@3| |atomic_read::__retval__@2|)) :named term_2046))
(push 1)
(declare-fun |static_key_false::tmp@3| () Int)
(declare-fun |__builtin_expect::exp@2| () Int)
(assert (! (= |__builtin_expect::exp@2| (ite (not (= |static_key_false::tmp@3| 0)) 1 0)) :named term_2047))
(push 1)
(declare-fun |__builtin_expect::__retval__@2| () Int)
(declare-fun |static_key_false::tmp___0@3| () Int)
(declare-fun |__builtin_expect::exp@2| () Int)
(assert (! (and (= |__builtin_expect::__retval__@2| |__builtin_expect::exp@2|) (= |static_key_false::tmp___0@3| |__builtin_expect::__retval__@2|)) :named term_2048))
(push 1)
(declare-fun |static_key_false::__retval__@2| () Int)
(declare-fun |trace_ath6kl_sdio::tmp___1@3| () Int)
(declare-fun |static_key_false::tmp___0@3| () Int)
(assert (! (and (> |static_key_false::tmp___0@3| 0) (= |static_key_false::__retval__@2| 1) (= |trace_ath6kl_sdio::tmp___1@3| |static_key_false::__retval__@2|)) :named term_2049))
(push 1)
(declare-fun |trace_ath6kl_sdio::tmp___1@3| () Int)
(assert (! (not (= |trace_ath6kl_sdio::tmp___1@3| 0)) :named term_2050))
(push 1)
(declare-fun |__ADDRESS_OF_rcu_read_lock_sched_notrace::tmp| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(assert (! (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_rcu_read_lock_sched_notrace::tmp|) |__ADDRESS_OF_rcu_read_lock_sched_notrace::tmp|) :named term_2051))
(push 1)
(declare-fun |current_thread_info::__retval__@2| () Int)
(declare-fun |rcu_read_lock_sched_notrace::tmp@3| () Int)
(declare-fun |current_thread_info::ti@3| () Int)
(declare-fun |current_thread_info::pfo_ret__@2| () Int)
(declare-fun |__ADDRESS_OF_current_thread_info::pfo_ret__| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_current_thread_info::ti| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(assert (! (and (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_current_thread_info::ti|) |__ADDRESS_OF_current_thread_info::ti|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_current_thread_info::pfo_ret__|) |__ADDRESS_OF_current_thread_info::pfo_ret__|) (= |current_thread_info::ti@3| (- |current_thread_info::pfo_ret__@2| 8152)) (= |current_thread_info::__retval__@2| |current_thread_info::ti@3|) (= |rcu_read_lock_sched_notrace::tmp@3| |current_thread_info::__retval__@2|)) :named term_2052))
(push 1)
(declare-fun *signed_int@1 (Int ) Int)
(declare-fun __ADDRESS_OF___tracepoint_ath6kl_sdio () Int)
(declare-fun *signed_int@2 (Int ) Int)
(declare-fun *signed_int@1 (Int ) Int)
(declare-fun |rcu_read_lock_sched_notrace::tmp@3| () Int)
(declare-fun *signed_int@2 (Int ) Int)
(assert (! (and (let ((.cse0 (+ |rcu_read_lock_sched_notrace::tmp@3| 28))) (= (*signed_int@2 .cse0) (+ (*signed_int@1 .cse0) 1))) (let ((.cse1 (+ __ADDRESS_OF___tracepoint_ath6kl_sdio 8))) (= (*signed_int@2 .cse1) (*signed_int@1 .cse1)))) :named term_2053))
(push 1)
(declare-fun |trace_ath6kl_sdio::it_func_ptr@3| () Int)
(declare-fun |trace_ath6kl_sdio::_________p1@3| () Int)
(declare-fun |trace_ath6kl_sdio::tmp@3| () Int)
(declare-fun debug_lockdep_rcu_enabled () Int)
(declare-fun |*(struct_tracepoint_func)*@1| (Int ) Int)
(declare-fun __ADDRESS_OF___tracepoint_ath6kl_sdio () Int)
(declare-fun |trace_ath6kl_sdio::__warned@2| () Int)
(assert (! (and (let ((.cse0 (= |trace_ath6kl_sdio::_________p1@3| (|*(struct_tracepoint_func)*@1| (+ __ADDRESS_OF___tracepoint_ath6kl_sdio 28)))) (.cse1 (= |trace_ath6kl_sdio::tmp@3| debug_lockdep_rcu_enabled)) (.cse2 (= |trace_ath6kl_sdio::tmp@3| 0))) (or (and .cse0 .cse1 (not .cse2) (not (= |trace_ath6kl_sdio::__warned@2| 0))) (and .cse0 .cse1 .cse2))) (= |trace_ath6kl_sdio::it_func_ptr@3| |trace_ath6kl_sdio::_________p1@3|) (= |trace_ath6kl_sdio::it_func_ptr@3| 0)) :named term_2054))
(push 1)
(declare-fun |__ADDRESS_OF_rcu_read_unlock_sched_notrace::tmp| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(assert (! (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_rcu_read_unlock_sched_notrace::tmp|) |__ADDRESS_OF_rcu_read_unlock_sched_notrace::tmp|) :named term_2055))
(push 1)
(declare-fun |current_thread_info::__retval__@3| () Int)
(declare-fun |rcu_read_unlock_sched_notrace::tmp@3| () Int)
(declare-fun |current_thread_info::ti@5| () Int)
(declare-fun |current_thread_info::pfo_ret__@3| () Int)
(declare-fun |__ADDRESS_OF_current_thread_info::pfo_ret__| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_current_thread_info::ti| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(assert (! (and (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_current_thread_info::ti|) |__ADDRESS_OF_current_thread_info::ti|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_current_thread_info::pfo_ret__|) |__ADDRESS_OF_current_thread_info::pfo_ret__|) (= |current_thread_info::ti@5| (- |current_thread_info::pfo_ret__@3| 8152)) (= |current_thread_info::__retval__@3| |current_thread_info::ti@5|) (= |rcu_read_unlock_sched_notrace::tmp@3| |current_thread_info::__retval__@3|)) :named term_2056))
(push 1)
(declare-fun *signed_int@2 (Int ) Int)
(declare-fun __ADDRESS_OF___tracepoint_ath6kl_sdio () Int)
(declare-fun *signed_int@3 (Int ) Int)
(declare-fun *signed_int@2 (Int ) Int)
(declare-fun |rcu_read_unlock_sched_notrace::tmp@3| () Int)
(declare-fun *signed_int@3 (Int ) Int)
(assert (! (and (let ((.cse0 (+ |rcu_read_unlock_sched_notrace::tmp@3| 28))) (= (*signed_int@3 .cse0) (+ (*signed_int@2 .cse0) (- 1)))) (let ((.cse1 (+ __ADDRESS_OF___tracepoint_ath6kl_sdio 8))) (= (*signed_int@3 .cse1) (*signed_int@2 .cse1)))) :named term_2057))
(push 1)
(assert (! true :named term_2058))
(push 1)
(declare-fun |ath6kl_sdio_io::__retval__@2| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::ret@3| () Int)
(declare-fun |ath6kl_sdio_io::ret@4| () Int)
(assert (! (and (= |ath6kl_sdio_io::__retval__@2| |ath6kl_sdio_io::ret@4|) (= |ath6kl_sdio_read_write_sync::ret@3| |ath6kl_sdio_io::__retval__@2|)) :named term_2059))
(push 1)
(declare-fun |ath6kl_sdio_read_write_sync::__retval__@2| () Int)
(declare-fun |ath6kl_set_addrwin_reg::status@3| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::ret@3| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::bounced@4| () Int)
(declare-fun _&_ (Int Int ) Int)
(declare-fun |ath6kl_sdio_read_write_sync::request@2| () Int)
(assert (! (and (let ((.cse0 (= (_&_ |ath6kl_sdio_read_write_sync::request@2| 1) 0)) (.cse1 (= |ath6kl_sdio_read_write_sync::bounced@4| 0))) (or (and .cse0 .cse1) (and .cse0 (not .cse1)))) (= |ath6kl_sdio_read_write_sync::__retval__@2| |ath6kl_sdio_read_write_sync::ret@3|) (= |ath6kl_set_addrwin_reg::status@3| |ath6kl_sdio_read_write_sync::__retval__@2|)) :named term_2060))
(push 1)
(declare-fun |ath6kl_set_addrwin_reg::i@3| () Int)
(declare-fun |ath6kl_set_addrwin_reg::i@4| () Int)
(declare-fun |ath6kl_set_addrwin_reg::status@3| () Int)
(assert (! (and (= |ath6kl_set_addrwin_reg::status@3| 0) (= |ath6kl_set_addrwin_reg::i@4| (+ |ath6kl_set_addrwin_reg::i@3| 1))) :named term_2061))
(push 1)
(declare-fun |ath6kl_sdio_read_write_sync::request@3| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::len@3| () Int)
(declare-fun |__ADDRESS_OF_ath6kl_set_addrwin_reg::addr_val| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::buf@3| () Int)
(declare-fun |ath6kl_set_addrwin_reg::i@4| () Int)
(declare-fun |ath6kl_set_addrwin_reg::reg_addr@2| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::addr@3| () Int)
(declare-fun |ath6kl_set_addrwin_reg::ar@2| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::ar@3| () Int)
(assert (! (and (<= |ath6kl_set_addrwin_reg::i@4| 3) (= |ath6kl_sdio_read_write_sync::ar@3| |ath6kl_set_addrwin_reg::ar@2|) (= |ath6kl_sdio_read_write_sync::addr@3| (+ |ath6kl_set_addrwin_reg::reg_addr@2| |ath6kl_set_addrwin_reg::i@4|)) (= |ath6kl_sdio_read_write_sync::buf@3| |__ADDRESS_OF_ath6kl_set_addrwin_reg::addr_val|) (= |ath6kl_sdio_read_write_sync::len@3| 4) (= |ath6kl_sdio_read_write_sync::request@3| 338)) :named term_2062))
(push 1)
(declare-fun |ath6kl_sdio_read_write_sync::ar@3| () Int)
(declare-fun |ath6kl_sdio_priv::ar@3| () Int)
(declare-fun |__ADDRESS_OF_ath6kl_sdio_read_write_sync::tmp___0| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_ath6kl_sdio_read_write_sync::bounced| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_ath6kl_sdio_read_write_sync::ret| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_ath6kl_sdio_read_write_sync::tbuf| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_ath6kl_sdio_read_write_sync::tmp| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_ath6kl_sdio_read_write_sync::ar_sdio| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(assert (! (and (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_ath6kl_sdio_read_write_sync::ar_sdio|) |__ADDRESS_OF_ath6kl_sdio_read_write_sync::ar_sdio|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_ath6kl_sdio_read_write_sync::tmp|) |__ADDRESS_OF_ath6kl_sdio_read_write_sync::tmp|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_ath6kl_sdio_read_write_sync::tbuf|) |__ADDRESS_OF_ath6kl_sdio_read_write_sync::tbuf|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_ath6kl_sdio_read_write_sync::ret|) |__ADDRESS_OF_ath6kl_sdio_read_write_sync::ret|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_ath6kl_sdio_read_write_sync::bounced|) |__ADDRESS_OF_ath6kl_sdio_read_write_sync::bounced|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_ath6kl_sdio_read_write_sync::tmp___0|) |__ADDRESS_OF_ath6kl_sdio_read_write_sync::tmp___0|) (= |ath6kl_sdio_priv::ar@3| |ath6kl_sdio_read_write_sync::ar@3|)) :named term_2063))
(push 1)
(declare-fun |ath6kl_sdio_priv::__retval__@3| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::tmp@5| () Int)
(declare-fun |__ADDRESS_OF_ath6kl_sdio_priv::__CPAchecker_TMP_0| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |ath6kl_sdio_priv::__CPAchecker_TMP_0@3| () Int)
(declare-fun |*(void)*@1| (Int ) Int)
(declare-fun |ath6kl_sdio_priv::ar@3| () Int)
(assert (! (and (= |ath6kl_sdio_priv::__CPAchecker_TMP_0@3| (|*(void)*@1| (+ |ath6kl_sdio_priv::ar@3| 121))) (= |ath6kl_sdio_priv::__retval__@3| |ath6kl_sdio_priv::__CPAchecker_TMP_0@3|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_ath6kl_sdio_priv::__CPAchecker_TMP_0|) |__ADDRESS_OF_ath6kl_sdio_priv::__CPAchecker_TMP_0|) (= |ath6kl_sdio_read_write_sync::tmp@5| |ath6kl_sdio_priv::__retval__@3|)) :named term_2064))
(push 1)
(declare-fun |ath6kl_sdio_read_write_sync::buf@3| () Int)
(declare-fun |buf_needs_bounce::buf@3| () Int)
(declare-fun _&_ (Int Int ) Int)
(declare-fun |ath6kl_sdio_read_write_sync::request@3| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::bounced@6| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::tbuf@6| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::tmp@5| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::ar_sdio@5| () Int)
(assert (! (and (= |ath6kl_sdio_read_write_sync::ar_sdio@5| |ath6kl_sdio_read_write_sync::tmp@5|) (= |ath6kl_sdio_read_write_sync::tbuf@6| 0) (= |ath6kl_sdio_read_write_sync::bounced@6| 0) (= (_&_ |ath6kl_sdio_read_write_sync::request@3| 128) 0) (= |buf_needs_bounce::buf@3| |ath6kl_sdio_read_write_sync::buf@3|)) :named term_2065))
(push 1)
(declare-fun |buf_needs_bounce::__retval__@3| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::tmp___0@5| () Int)
(declare-fun |buf_needs_bounce::tmp___1@5| () Int)
(declare-fun |buf_needs_bounce::tmp___0@5| () Int)
(declare-fun |buf_needs_bounce::tmp@5| () Int)
(declare-fun __virt_addr_valid (Int ) Int)
(declare-fun |buf_needs_bounce::buf@3| () Int)
(declare-fun _&_ (Int Int ) Int)
(declare-fun |__ADDRESS_OF_buf_needs_bounce::tmp___1| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_buf_needs_bounce::tmp___0| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_buf_needs_bounce::tmp| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |buf_needs_bounce::tmp___0@4| () Int)
(declare-fun |buf_needs_bounce::tmp@4| () Int)
(assert (! (and (let ((.cse0 (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_buf_needs_bounce::tmp|) |__ADDRESS_OF_buf_needs_bounce::tmp|)) (.cse1 (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_buf_needs_bounce::tmp___0|) |__ADDRESS_OF_buf_needs_bounce::tmp___0|)) (.cse2 (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_buf_needs_bounce::tmp___1|) |__ADDRESS_OF_buf_needs_bounce::tmp___1|)) (.cse3 (= (_&_ |buf_needs_bounce::buf@3| 3) 0)) (.cse6 (= |buf_needs_bounce::tmp@5| (__virt_addr_valid |buf_needs_bounce::buf@3|))) (.cse7 (= |buf_needs_bounce::tmp@5| 0)) (.cse8 (= |buf_needs_bounce::tmp___0@5| 0)) (.cse4 (= |buf_needs_bounce::tmp___1@5| 1)) (.cse5 (= |buf_needs_bounce::__retval__@3| |buf_needs_bounce::tmp___1@5|))) (or (and .cse0 .cse1 .cse2 (not .cse3) .cse4 .cse5 (= |buf_needs_bounce::tmp@5| |buf_needs_bounce::tmp@4|) (= |buf_needs_bounce::tmp___0@5| |buf_needs_bounce::tmp___0@4|)) (and .cse0 .cse1 .cse2 .cse3 .cse6 (not .cse7) .cse8 (= |buf_needs_bounce::tmp___1@5| 0) .cse5) (and .cse0 .cse1 .cse2 .cse3 .cse6 .cse7 (= |buf_needs_bounce::tmp___0@5| 1) (not .cse8) .cse4 .cse5))) (= |ath6kl_sdio_read_write_sync::tmp___0@5| |buf_needs_bounce::__retval__@3|)) :named term_2066))
(push 1)
(declare-fun |ath6kl_sdio_read_write_sync::len@3| () Int)
(declare-fun |ath6kl_sdio_io::len@3| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::tbuf@7| () Int)
(declare-fun |ath6kl_sdio_io::buf@3| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::addr@3| () Int)
(declare-fun |ath6kl_sdio_io::addr@5| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::request@3| () Int)
(declare-fun |ath6kl_sdio_io::request@3| () Int)
(declare-fun |*(struct_sdio_func)*@1| (Int ) Int)
(declare-fun |ath6kl_sdio_read_write_sync::ar_sdio@5| () Int)
(declare-fun |ath6kl_sdio_io::func@3| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::bounced@7| () Int)
(declare-fun _&_ (Int Int ) Int)
(declare-fun |*(unsigned_char)*@1| (Int ) Int)
(declare-fun |ath6kl_sdio_read_write_sync::__CPAchecker_TMP_0@3| () Int)
(declare-fun |__ADDRESS_OF_ath6kl_sdio_read_write_sync::__CPAchecker_TMP_0| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |ath6kl_sdio_read_write_sync::tmp___0@5| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::bounced@6| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::__CPAchecker_TMP_0@2| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::buf@3| () Int)
(assert (! (and (let ((.cse0 (= |ath6kl_sdio_read_write_sync::tmp___0@5| 0))) (or (and .cse0 (= |ath6kl_sdio_read_write_sync::tbuf@7| |ath6kl_sdio_read_write_sync::buf@3|) (= |ath6kl_sdio_read_write_sync::__CPAchecker_TMP_0@3| |ath6kl_sdio_read_write_sync::__CPAchecker_TMP_0@2|) (= |ath6kl_sdio_read_write_sync::bounced@7| |ath6kl_sdio_read_write_sync::bounced@6|)) (let ((.cse1 (|*(unsigned_char)*@1| (+ |ath6kl_sdio_read_write_sync::ar_sdio@5| 3684)))) (and (not .cse0) (= |ath6kl_sdio_read_write_sync::__CPAchecker_TMP_0@3| .cse1) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_ath6kl_sdio_read_write_sync::__CPAchecker_TMP_0|) |__ADDRESS_OF_ath6kl_sdio_read_write_sync::__CPAchecker_TMP_0|) (not (= |ath6kl_sdio_read_write_sync::__CPAchecker_TMP_0@3| 0)) (= |ath6kl_sdio_read_write_sync::tbuf@7| .cse1) (not (= (_&_ |ath6kl_sdio_read_write_sync::request@3| 2) 0)) (= |ath6kl_sdio_read_write_sync::bounced@7| 1))))) (= |ath6kl_sdio_io::func@3| (|*(struct_sdio_func)*@1| (+ |ath6kl_sdio_read_write_sync::ar_sdio@5| 0))) (= |ath6kl_sdio_io::request@3| |ath6kl_sdio_read_write_sync::request@3|) (= |ath6kl_sdio_io::addr@5| |ath6kl_sdio_read_write_sync::addr@3|) (= |ath6kl_sdio_io::buf@3| |ath6kl_sdio_read_write_sync::tbuf@7|) (= |ath6kl_sdio_io::len@3| |ath6kl_sdio_read_write_sync::len@3|)) :named term_2067))
(push 1)
(declare-fun |ath6kl_sdio_io::func@3| () Int)
(declare-fun |ldv_sdio_claim_host_1::ldv_func_arg1@3| () Int)
(declare-fun |__ADDRESS_OF_ath6kl_sdio_io::ret| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |ath6kl_sdio_io::ret@6| () Int)
(assert (! (and (= |ath6kl_sdio_io::ret@6| 0) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_ath6kl_sdio_io::ret|) |__ADDRESS_OF_ath6kl_sdio_io::ret|) (= |ldv_sdio_claim_host_1::ldv_func_arg1@3| |ath6kl_sdio_io::func@3|)) :named term_2068))
(push 1)
(declare-fun *signed_int@3 (Int ) Int)
(declare-fun |*(struct_mmc_host)*@1| (Int ) Int)
(declare-fun |*(struct_mmc_card)*@1| (Int ) Int)
(declare-fun |ldv_sdio_claim_host_1::ldv_func_arg1@3| () Int)
(declare-fun |ldv_sdio_claim_host::dev_id@3| () Int)
(assert (! (= |ldv_sdio_claim_host::dev_id@3| (*signed_int@3 (+ (|*(struct_mmc_host)*@1| (+ (|*(struct_mmc_card)*@1| (+ |ldv_sdio_claim_host_1::ldv_func_arg1@3| 0)) 0)) 1310))) :named term_2069))
(push 1)
(declare-fun |ldv_sdio_claim_host::dev_id@3| () Int)
(declare-fun ldv_sdio_element@5 () Int)
(declare-fun ldv_sdio_element@4 () Int)
(assert (! (and (= ldv_sdio_element@4 0) (= ldv_sdio_element@5 |ldv_sdio_claim_host::dev_id@3|)) :named term_2070))
(push 1)
(assert (! true :named term_2071))
(push 1)
(declare-fun |ath6kl_sdio_io::func@3| () Int)
(declare-fun |ldv_sdio_writesb_2::ldv_func_arg1@3| () Int)
(declare-fun _&_ (Int Int ) Int)
(declare-fun |ath6kl_sdio_io::request@3| () Int)
(declare-fun |ath6kl_sdio_io::addr@6| () Int)
(declare-fun |ath6kl_sdio_io::addr@7| () Int)
(declare-fun |ath6kl_sdio_io::addr@5| () Int)
(declare-fun _&_ (Int Int ) Int)
(declare-fun |ath6kl_sdio_io::len@3| () Int)
(assert (! (and (let ((.cse0 (let ((.cse4 (<= |ath6kl_sdio_io::addr@5| 8191)) (.cse2 (not (= (_&_ |ath6kl_sdio_io::request@3| 2) 0))) (.cse3 (> |ath6kl_sdio_io::addr@5| 2047))) (or (and .cse2 .cse3 .cse4 (= |ath6kl_sdio_io::addr@6| (+ (- |ath6kl_sdio_io::addr@5| |ath6kl_sdio_io::len@3|) 2048))) (and (or (and .cse2 .cse3 (not .cse4)) (and .cse2 (not .cse3))) (= |ath6kl_sdio_io::addr@6| |ath6kl_sdio_io::addr@5|))))) (.cse1 (= |ath6kl_sdio_io::addr@6| 16384))) (or (and .cse0 .cse1 (= |ath6kl_sdio_io::addr@7| (+ (- |ath6kl_sdio_io::addr@6| |ath6kl_sdio_io::len@3|) 12288))) (and .cse0 (not .cse1) (= |ath6kl_sdio_io::addr@7| |ath6kl_sdio_io::addr@6|)))) (not (= (_&_ |ath6kl_sdio_io::request@3| 256) 0)) (= |ldv_sdio_writesb_2::ldv_func_arg1@3| |ath6kl_sdio_io::func@3|)) :named term_2072))
(push 1)
(declare-fun *signed_int@3 (Int ) Int)
(declare-fun |*(struct_mmc_host)*@1| (Int ) Int)
(declare-fun |*(struct_mmc_card)*@1| (Int ) Int)
(declare-fun |ldv_sdio_writesb_2::ldv_func_arg1@3| () Int)
(declare-fun |ldv_check_context::x@3| () Int)
(assert (! (= |ldv_check_context::x@3| (*signed_int@3 (+ (|*(struct_mmc_host)*@1| (+ (|*(struct_mmc_card)*@1| (+ |ldv_sdio_writesb_2::ldv_func_arg1@3| 0)) 0)) 1310))) :named term_2073))
(push 1)
(declare-fun |ldv_check_context::x@3| () Int)
(declare-fun ldv_sdio_element@5 () Int)
(assert (! (= ldv_sdio_element@5 |ldv_check_context::x@3|) :named term_2074))
(push 1)
(declare-fun |ldv_sdio_writesb_2::__retval__@3| () Int)
(declare-fun |ath6kl_sdio_io::ret@7| () Int)
(assert (! (and (= |ldv_sdio_writesb_2::__retval__@3| 0) (= |ath6kl_sdio_io::ret@7| |ldv_sdio_writesb_2::__retval__@3|)) :named term_2075))
(push 1)
(declare-fun |ath6kl_sdio_io::func@3| () Int)
(declare-fun |ldv_sdio_release_host_6::ldv_func_arg1@3| () Int)
(assert (! (= |ldv_sdio_release_host_6::ldv_func_arg1@3| |ath6kl_sdio_io::func@3|) :named term_2076))
(push 1)
(declare-fun *signed_int@3 (Int ) Int)
(declare-fun |*(struct_mmc_host)*@1| (Int ) Int)
(declare-fun |*(struct_mmc_card)*@1| (Int ) Int)
(declare-fun |ldv_sdio_release_host_6::ldv_func_arg1@3| () Int)
(declare-fun |ldv_sdio_release_host::dev_id@3| () Int)
(assert (! (= |ldv_sdio_release_host::dev_id@3| (*signed_int@3 (+ (|*(struct_mmc_host)*@1| (+ (|*(struct_mmc_card)*@1| (+ |ldv_sdio_release_host_6::ldv_func_arg1@3| 0)) 0)) 1310))) :named term_2077))
(push 1)
(declare-fun ldv_sdio_element@6 () Int)
(declare-fun |ldv_sdio_release_host::dev_id@3| () Int)
(declare-fun ldv_sdio_element@5 () Int)
(assert (! (and (= ldv_sdio_element@5 |ldv_sdio_release_host::dev_id@3|) (= ldv_sdio_element@6 0)) :named term_2078))
(push 1)
(assert (! true :named term_2079))
(push 1)
(declare-fun |ath6kl_sdio_io::len@3| () Int)
(declare-fun |trace_ath6kl_sdio::buf_len@3| () Int)
(declare-fun |ath6kl_sdio_io::buf@3| () Int)
(declare-fun |trace_ath6kl_sdio::buf@3| () Int)
(declare-fun |ath6kl_sdio_io::request@3| () Int)
(declare-fun |trace_ath6kl_sdio::flags@3| () Int)
(declare-fun |ath6kl_sdio_io::addr@7| () Int)
(declare-fun |trace_ath6kl_sdio::addr@3| () Int)
(declare-fun __string__ (Int ) Int)
(declare-fun |ath6kl_sdio_io::__CPAchecker_TMP_1@5| () Int)
(declare-fun _&_ (Int Int ) Int)
(declare-fun __string__ (Int ) Int)
(declare-fun |ath6kl_sdio_io::__CPAchecker_TMP_0@5| () Int)
(declare-fun _&_ (Int Int ) Int)
(declare-fun |__ADDRESS_OF_ath6kl_sdio_io::__CPAchecker_TMP_1| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_ath6kl_sdio_io::__CPAchecker_TMP_0| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(assert (! (and (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_ath6kl_sdio_io::__CPAchecker_TMP_0|) |__ADDRESS_OF_ath6kl_sdio_io::__CPAchecker_TMP_0|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_ath6kl_sdio_io::__CPAchecker_TMP_1|) |__ADDRESS_OF_ath6kl_sdio_io::__CPAchecker_TMP_1|) (not (= (_&_ |ath6kl_sdio_io::request@3| 2) 0)) (= |ath6kl_sdio_io::__CPAchecker_TMP_0@5| (__string__ 12)) (not (= (_&_ |ath6kl_sdio_io::request@3| 256) 0)) (= |ath6kl_sdio_io::__CPAchecker_TMP_1@5| (__string__ 13)) (= |trace_ath6kl_sdio::addr@3| |ath6kl_sdio_io::addr@7|) (= |trace_ath6kl_sdio::flags@3| |ath6kl_sdio_io::request@3|) (= |trace_ath6kl_sdio::buf@3| |ath6kl_sdio_io::buf@3|) (= |trace_ath6kl_sdio::buf_len@3| |ath6kl_sdio_io::len@3|)) :named term_2080))
(push 1)
(declare-fun __ADDRESS_OF___tracepoint_ath6kl_sdio () Int)
(declare-fun |static_key_false::key@3| () Int)
(declare-fun |__ADDRESS_OF_trace_ath6kl_sdio::tmp___1| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_trace_ath6kl_sdio::tmp___0| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_trace_ath6kl_sdio::tmp| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_trace_ath6kl_sdio::__warned| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_trace_ath6kl_sdio::_________p1| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_trace_ath6kl_sdio::__data| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_trace_ath6kl_sdio::it_func_ptr| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(assert (! (and (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_trace_ath6kl_sdio::it_func_ptr|) |__ADDRESS_OF_trace_ath6kl_sdio::it_func_ptr|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_trace_ath6kl_sdio::__data|) |__ADDRESS_OF_trace_ath6kl_sdio::__data|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_trace_ath6kl_sdio::_________p1|) |__ADDRESS_OF_trace_ath6kl_sdio::_________p1|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_trace_ath6kl_sdio::__warned|) |__ADDRESS_OF_trace_ath6kl_sdio::__warned|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_trace_ath6kl_sdio::tmp|) |__ADDRESS_OF_trace_ath6kl_sdio::tmp|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_trace_ath6kl_sdio::tmp___0|) |__ADDRESS_OF_trace_ath6kl_sdio::tmp___0|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_trace_ath6kl_sdio::tmp___1|) |__ADDRESS_OF_trace_ath6kl_sdio::tmp___1|) (= |static_key_false::key@3| (+ __ADDRESS_OF___tracepoint_ath6kl_sdio 8))) :named term_2081))
(push 1)
(declare-fun |static_key_false::key@3| () Int)
(declare-fun |atomic_read::v@3| () Int)
(declare-fun |__ADDRESS_OF_static_key_false::tmp___0| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_static_key_false::tmp| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(assert (! (and (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_static_key_false::tmp|) |__ADDRESS_OF_static_key_false::tmp|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_static_key_false::tmp___0|) |__ADDRESS_OF_static_key_false::tmp___0|) (= |atomic_read::v@3| (+ |static_key_false::key@3| 0))) :named term_2082))
(push 1)
(declare-fun |atomic_read::__retval__@3| () Int)
(declare-fun |static_key_false::tmp@5| () Int)
(declare-fun *signed_int@3 (Int ) Int)
(declare-fun |atomic_read::v@3| () Int)
(assert (! (and (= |atomic_read::__retval__@3| (*signed_int@3 (+ |atomic_read::v@3| 0))) (= |static_key_false::tmp@5| |atomic_read::__retval__@3|)) :named term_2083))
(push 1)
(declare-fun |static_key_false::tmp@5| () Int)
(declare-fun |__builtin_expect::exp@3| () Int)
(assert (! (= |__builtin_expect::exp@3| (ite (not (= |static_key_false::tmp@5| 0)) 1 0)) :named term_2084))
(push 1)
(declare-fun |__builtin_expect::__retval__@3| () Int)
(declare-fun |static_key_false::tmp___0@5| () Int)
(declare-fun |__builtin_expect::exp@3| () Int)
(assert (! (and (= |__builtin_expect::__retval__@3| |__builtin_expect::exp@3|) (= |static_key_false::tmp___0@5| |__builtin_expect::__retval__@3|)) :named term_2085))
(push 1)
(declare-fun |static_key_false::__retval__@3| () Int)
(declare-fun |trace_ath6kl_sdio::tmp___1@5| () Int)
(declare-fun |static_key_false::tmp___0@5| () Int)
(assert (! (and (> |static_key_false::tmp___0@5| 0) (= |static_key_false::__retval__@3| 1) (= |trace_ath6kl_sdio::tmp___1@5| |static_key_false::__retval__@3|)) :named term_2086))
(push 1)
(declare-fun |trace_ath6kl_sdio::tmp___1@5| () Int)
(assert (! (not (= |trace_ath6kl_sdio::tmp___1@5| 0)) :named term_2087))
(push 1)
(declare-fun |__ADDRESS_OF_rcu_read_lock_sched_notrace::tmp| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(assert (! (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_rcu_read_lock_sched_notrace::tmp|) |__ADDRESS_OF_rcu_read_lock_sched_notrace::tmp|) :named term_2088))
(push 1)
(declare-fun |current_thread_info::__retval__@4| () Int)
(declare-fun |rcu_read_lock_sched_notrace::tmp@5| () Int)
(declare-fun |current_thread_info::ti@7| () Int)
(declare-fun |current_thread_info::pfo_ret__@4| () Int)
(declare-fun |__ADDRESS_OF_current_thread_info::pfo_ret__| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_current_thread_info::ti| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(assert (! (and (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_current_thread_info::ti|) |__ADDRESS_OF_current_thread_info::ti|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_current_thread_info::pfo_ret__|) |__ADDRESS_OF_current_thread_info::pfo_ret__|) (= |current_thread_info::ti@7| (- |current_thread_info::pfo_ret__@4| 8152)) (= |current_thread_info::__retval__@4| |current_thread_info::ti@7|) (= |rcu_read_lock_sched_notrace::tmp@5| |current_thread_info::__retval__@4|)) :named term_2089))
(push 1)
(declare-fun *signed_int@3 (Int ) Int)
(declare-fun __ADDRESS_OF___tracepoint_ath6kl_sdio () Int)
(declare-fun *signed_int@4 (Int ) Int)
(declare-fun *signed_int@3 (Int ) Int)
(declare-fun |rcu_read_lock_sched_notrace::tmp@5| () Int)
(declare-fun *signed_int@4 (Int ) Int)
(assert (! (and (let ((.cse0 (+ |rcu_read_lock_sched_notrace::tmp@5| 28))) (= (*signed_int@4 .cse0) (+ (*signed_int@3 .cse0) 1))) (let ((.cse1 (+ __ADDRESS_OF___tracepoint_ath6kl_sdio 8))) (= (*signed_int@4 .cse1) (*signed_int@3 .cse1)))) :named term_2090))
(push 1)
(declare-fun |trace_ath6kl_sdio::it_func_ptr@5| () Int)
(declare-fun |trace_ath6kl_sdio::_________p1@5| () Int)
(declare-fun |trace_ath6kl_sdio::tmp@5| () Int)
(declare-fun debug_lockdep_rcu_enabled () Int)
(declare-fun |*(struct_tracepoint_func)*@1| (Int ) Int)
(declare-fun __ADDRESS_OF___tracepoint_ath6kl_sdio () Int)
(declare-fun |trace_ath6kl_sdio::__warned@3| () Int)
(assert (! (and (let ((.cse0 (= |trace_ath6kl_sdio::_________p1@5| (|*(struct_tracepoint_func)*@1| (+ __ADDRESS_OF___tracepoint_ath6kl_sdio 28)))) (.cse1 (= |trace_ath6kl_sdio::tmp@5| debug_lockdep_rcu_enabled)) (.cse2 (= |trace_ath6kl_sdio::tmp@5| 0))) (or (and .cse0 .cse1 (not .cse2) (not (= |trace_ath6kl_sdio::__warned@3| 0))) (and .cse0 .cse1 .cse2))) (= |trace_ath6kl_sdio::it_func_ptr@5| |trace_ath6kl_sdio::_________p1@5|) (= |trace_ath6kl_sdio::it_func_ptr@5| 0)) :named term_2091))
(push 1)
(declare-fun |__ADDRESS_OF_rcu_read_unlock_sched_notrace::tmp| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(assert (! (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_rcu_read_unlock_sched_notrace::tmp|) |__ADDRESS_OF_rcu_read_unlock_sched_notrace::tmp|) :named term_2092))
(push 1)
(declare-fun |current_thread_info::__retval__@5| () Int)
(declare-fun |rcu_read_unlock_sched_notrace::tmp@5| () Int)
(declare-fun |current_thread_info::ti@9| () Int)
(declare-fun |current_thread_info::pfo_ret__@5| () Int)
(declare-fun |__ADDRESS_OF_current_thread_info::pfo_ret__| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_current_thread_info::ti| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(assert (! (and (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_current_thread_info::ti|) |__ADDRESS_OF_current_thread_info::ti|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_current_thread_info::pfo_ret__|) |__ADDRESS_OF_current_thread_info::pfo_ret__|) (= |current_thread_info::ti@9| (- |current_thread_info::pfo_ret__@5| 8152)) (= |current_thread_info::__retval__@5| |current_thread_info::ti@9|) (= |rcu_read_unlock_sched_notrace::tmp@5| |current_thread_info::__retval__@5|)) :named term_2093))
(push 1)
(declare-fun *signed_int@4 (Int ) Int)
(declare-fun __ADDRESS_OF___tracepoint_ath6kl_sdio () Int)
(declare-fun *signed_int@5 (Int ) Int)
(declare-fun *signed_int@4 (Int ) Int)
(declare-fun |rcu_read_unlock_sched_notrace::tmp@5| () Int)
(declare-fun *signed_int@5 (Int ) Int)
(assert (! (and (let ((.cse0 (+ |rcu_read_unlock_sched_notrace::tmp@5| 28))) (= (*signed_int@5 .cse0) (+ (*signed_int@4 .cse0) (- 1)))) (let ((.cse1 (+ __ADDRESS_OF___tracepoint_ath6kl_sdio 8))) (= (*signed_int@5 .cse1) (*signed_int@4 .cse1)))) :named term_2094))
(push 1)
(assert (! true :named term_2095))
(push 1)
(declare-fun |ath6kl_sdio_io::__retval__@3| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::ret@5| () Int)
(declare-fun |ath6kl_sdio_io::ret@7| () Int)
(assert (! (and (= |ath6kl_sdio_io::__retval__@3| |ath6kl_sdio_io::ret@7|) (= |ath6kl_sdio_read_write_sync::ret@5| |ath6kl_sdio_io::__retval__@3|)) :named term_2096))
(push 1)
(declare-fun |ath6kl_sdio_read_write_sync::__retval__@3| () Int)
(declare-fun |ath6kl_set_addrwin_reg::status@4| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::ret@5| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::bounced@7| () Int)
(declare-fun _&_ (Int Int ) Int)
(declare-fun |ath6kl_sdio_read_write_sync::request@3| () Int)
(assert (! (and (let ((.cse0 (= (_&_ |ath6kl_sdio_read_write_sync::request@3| 1) 0)) (.cse1 (= |ath6kl_sdio_read_write_sync::bounced@7| 0))) (or (and .cse0 .cse1) (and .cse0 (not .cse1)))) (= |ath6kl_sdio_read_write_sync::__retval__@3| |ath6kl_sdio_read_write_sync::ret@5|) (= |ath6kl_set_addrwin_reg::status@4| |ath6kl_sdio_read_write_sync::__retval__@3|)) :named term_2097))
(push 1)
(declare-fun |ath6kl_set_addrwin_reg::i@4| () Int)
(declare-fun |ath6kl_set_addrwin_reg::i@5| () Int)
(declare-fun |ath6kl_set_addrwin_reg::status@4| () Int)
(assert (! (and (= |ath6kl_set_addrwin_reg::status@4| 0) (= |ath6kl_set_addrwin_reg::i@5| (+ |ath6kl_set_addrwin_reg::i@4| 1))) :named term_2098))
(push 1)
(declare-fun |ath6kl_sdio_read_write_sync::request@4| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::len@4| () Int)
(declare-fun |__ADDRESS_OF_ath6kl_set_addrwin_reg::addr_val| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::buf@4| () Int)
(declare-fun |ath6kl_set_addrwin_reg::i@5| () Int)
(declare-fun |ath6kl_set_addrwin_reg::reg_addr@2| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::addr@4| () Int)
(declare-fun |ath6kl_set_addrwin_reg::ar@2| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::ar@4| () Int)
(assert (! (and (<= |ath6kl_set_addrwin_reg::i@5| 3) (= |ath6kl_sdio_read_write_sync::ar@4| |ath6kl_set_addrwin_reg::ar@2|) (= |ath6kl_sdio_read_write_sync::addr@4| (+ |ath6kl_set_addrwin_reg::reg_addr@2| |ath6kl_set_addrwin_reg::i@5|)) (= |ath6kl_sdio_read_write_sync::buf@4| |__ADDRESS_OF_ath6kl_set_addrwin_reg::addr_val|) (= |ath6kl_sdio_read_write_sync::len@4| 4) (= |ath6kl_sdio_read_write_sync::request@4| 338)) :named term_2099))
(push 1)
(declare-fun |ath6kl_sdio_read_write_sync::ar@4| () Int)
(declare-fun |ath6kl_sdio_priv::ar@4| () Int)
(declare-fun |__ADDRESS_OF_ath6kl_sdio_read_write_sync::tmp___0| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_ath6kl_sdio_read_write_sync::bounced| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_ath6kl_sdio_read_write_sync::ret| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_ath6kl_sdio_read_write_sync::tbuf| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_ath6kl_sdio_read_write_sync::tmp| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_ath6kl_sdio_read_write_sync::ar_sdio| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(assert (! (and (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_ath6kl_sdio_read_write_sync::ar_sdio|) |__ADDRESS_OF_ath6kl_sdio_read_write_sync::ar_sdio|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_ath6kl_sdio_read_write_sync::tmp|) |__ADDRESS_OF_ath6kl_sdio_read_write_sync::tmp|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_ath6kl_sdio_read_write_sync::tbuf|) |__ADDRESS_OF_ath6kl_sdio_read_write_sync::tbuf|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_ath6kl_sdio_read_write_sync::ret|) |__ADDRESS_OF_ath6kl_sdio_read_write_sync::ret|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_ath6kl_sdio_read_write_sync::bounced|) |__ADDRESS_OF_ath6kl_sdio_read_write_sync::bounced|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_ath6kl_sdio_read_write_sync::tmp___0|) |__ADDRESS_OF_ath6kl_sdio_read_write_sync::tmp___0|) (= |ath6kl_sdio_priv::ar@4| |ath6kl_sdio_read_write_sync::ar@4|)) :named term_2100))
(push 1)
(declare-fun |ath6kl_sdio_priv::__retval__@4| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::tmp@7| () Int)
(declare-fun |__ADDRESS_OF_ath6kl_sdio_priv::__CPAchecker_TMP_0| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |ath6kl_sdio_priv::__CPAchecker_TMP_0@4| () Int)
(declare-fun |*(void)*@1| (Int ) Int)
(declare-fun |ath6kl_sdio_priv::ar@4| () Int)
(assert (! (and (= |ath6kl_sdio_priv::__CPAchecker_TMP_0@4| (|*(void)*@1| (+ |ath6kl_sdio_priv::ar@4| 121))) (= |ath6kl_sdio_priv::__retval__@4| |ath6kl_sdio_priv::__CPAchecker_TMP_0@4|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_ath6kl_sdio_priv::__CPAchecker_TMP_0|) |__ADDRESS_OF_ath6kl_sdio_priv::__CPAchecker_TMP_0|) (= |ath6kl_sdio_read_write_sync::tmp@7| |ath6kl_sdio_priv::__retval__@4|)) :named term_2101))
(push 1)
(declare-fun |ath6kl_sdio_read_write_sync::buf@4| () Int)
(declare-fun |buf_needs_bounce::buf@4| () Int)
(declare-fun _&_ (Int Int ) Int)
(declare-fun |ath6kl_sdio_read_write_sync::request@4| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::bounced@9| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::tbuf@9| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::tmp@7| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::ar_sdio@7| () Int)
(assert (! (and (= |ath6kl_sdio_read_write_sync::ar_sdio@7| |ath6kl_sdio_read_write_sync::tmp@7|) (= |ath6kl_sdio_read_write_sync::tbuf@9| 0) (= |ath6kl_sdio_read_write_sync::bounced@9| 0) (= (_&_ |ath6kl_sdio_read_write_sync::request@4| 128) 0) (= |buf_needs_bounce::buf@4| |ath6kl_sdio_read_write_sync::buf@4|)) :named term_2102))
(push 1)
(declare-fun |buf_needs_bounce::__retval__@4| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::tmp___0@7| () Int)
(declare-fun |buf_needs_bounce::tmp___1@7| () Int)
(declare-fun |buf_needs_bounce::tmp___0@7| () Int)
(declare-fun |buf_needs_bounce::tmp@7| () Int)
(declare-fun __virt_addr_valid (Int ) Int)
(declare-fun |buf_needs_bounce::buf@4| () Int)
(declare-fun _&_ (Int Int ) Int)
(declare-fun |__ADDRESS_OF_buf_needs_bounce::tmp___1| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_buf_needs_bounce::tmp___0| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_buf_needs_bounce::tmp| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |buf_needs_bounce::tmp___0@6| () Int)
(declare-fun |buf_needs_bounce::tmp@6| () Int)
(assert (! (and (let ((.cse0 (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_buf_needs_bounce::tmp|) |__ADDRESS_OF_buf_needs_bounce::tmp|)) (.cse1 (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_buf_needs_bounce::tmp___0|) |__ADDRESS_OF_buf_needs_bounce::tmp___0|)) (.cse2 (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_buf_needs_bounce::tmp___1|) |__ADDRESS_OF_buf_needs_bounce::tmp___1|)) (.cse3 (= (_&_ |buf_needs_bounce::buf@4| 3) 0)) (.cse6 (= |buf_needs_bounce::tmp@7| (__virt_addr_valid |buf_needs_bounce::buf@4|))) (.cse7 (= |buf_needs_bounce::tmp@7| 0)) (.cse8 (= |buf_needs_bounce::tmp___0@7| 0)) (.cse4 (= |buf_needs_bounce::tmp___1@7| 1)) (.cse5 (= |buf_needs_bounce::__retval__@4| |buf_needs_bounce::tmp___1@7|))) (or (and .cse0 .cse1 .cse2 (not .cse3) .cse4 .cse5 (= |buf_needs_bounce::tmp@7| |buf_needs_bounce::tmp@6|) (= |buf_needs_bounce::tmp___0@7| |buf_needs_bounce::tmp___0@6|)) (and .cse0 .cse1 .cse2 .cse3 .cse6 (not .cse7) .cse8 (= |buf_needs_bounce::tmp___1@7| 0) .cse5) (and .cse0 .cse1 .cse2 .cse3 .cse6 .cse7 (= |buf_needs_bounce::tmp___0@7| 1) (not .cse8) .cse4 .cse5))) (= |ath6kl_sdio_read_write_sync::tmp___0@7| |buf_needs_bounce::__retval__@4|)) :named term_2103))
(push 1)
(declare-fun |ath6kl_sdio_read_write_sync::len@4| () Int)
(declare-fun |ath6kl_sdio_io::len@4| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::tbuf@10| () Int)
(declare-fun |ath6kl_sdio_io::buf@4| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::addr@4| () Int)
(declare-fun |ath6kl_sdio_io::addr@8| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::request@4| () Int)
(declare-fun |ath6kl_sdio_io::request@4| () Int)
(declare-fun |*(struct_sdio_func)*@1| (Int ) Int)
(declare-fun |ath6kl_sdio_read_write_sync::ar_sdio@7| () Int)
(declare-fun |ath6kl_sdio_io::func@4| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::bounced@10| () Int)
(declare-fun _&_ (Int Int ) Int)
(declare-fun |*(unsigned_char)*@1| (Int ) Int)
(declare-fun |ath6kl_sdio_read_write_sync::__CPAchecker_TMP_0@4| () Int)
(declare-fun |__ADDRESS_OF_ath6kl_sdio_read_write_sync::__CPAchecker_TMP_0| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |ath6kl_sdio_read_write_sync::tmp___0@7| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::bounced@9| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::__CPAchecker_TMP_0@3| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::buf@4| () Int)
(assert (! (and (let ((.cse0 (= |ath6kl_sdio_read_write_sync::tmp___0@7| 0))) (or (and .cse0 (= |ath6kl_sdio_read_write_sync::tbuf@10| |ath6kl_sdio_read_write_sync::buf@4|) (= |ath6kl_sdio_read_write_sync::__CPAchecker_TMP_0@4| |ath6kl_sdio_read_write_sync::__CPAchecker_TMP_0@3|) (= |ath6kl_sdio_read_write_sync::bounced@10| |ath6kl_sdio_read_write_sync::bounced@9|)) (let ((.cse1 (|*(unsigned_char)*@1| (+ |ath6kl_sdio_read_write_sync::ar_sdio@7| 3684)))) (and (not .cse0) (= |ath6kl_sdio_read_write_sync::__CPAchecker_TMP_0@4| .cse1) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_ath6kl_sdio_read_write_sync::__CPAchecker_TMP_0|) |__ADDRESS_OF_ath6kl_sdio_read_write_sync::__CPAchecker_TMP_0|) (not (= |ath6kl_sdio_read_write_sync::__CPAchecker_TMP_0@4| 0)) (= |ath6kl_sdio_read_write_sync::tbuf@10| .cse1) (not (= (_&_ |ath6kl_sdio_read_write_sync::request@4| 2) 0)) (= |ath6kl_sdio_read_write_sync::bounced@10| 1))))) (= |ath6kl_sdio_io::func@4| (|*(struct_sdio_func)*@1| (+ |ath6kl_sdio_read_write_sync::ar_sdio@7| 0))) (= |ath6kl_sdio_io::request@4| |ath6kl_sdio_read_write_sync::request@4|) (= |ath6kl_sdio_io::addr@8| |ath6kl_sdio_read_write_sync::addr@4|) (= |ath6kl_sdio_io::buf@4| |ath6kl_sdio_read_write_sync::tbuf@10|) (= |ath6kl_sdio_io::len@4| |ath6kl_sdio_read_write_sync::len@4|)) :named term_2104))
(push 1)
(declare-fun |ath6kl_sdio_io::func@4| () Int)
(declare-fun |ldv_sdio_claim_host_1::ldv_func_arg1@4| () Int)
(declare-fun |__ADDRESS_OF_ath6kl_sdio_io::ret| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |ath6kl_sdio_io::ret@9| () Int)
(assert (! (and (= |ath6kl_sdio_io::ret@9| 0) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_ath6kl_sdio_io::ret|) |__ADDRESS_OF_ath6kl_sdio_io::ret|) (= |ldv_sdio_claim_host_1::ldv_func_arg1@4| |ath6kl_sdio_io::func@4|)) :named term_2105))
(push 1)
(declare-fun *signed_int@5 (Int ) Int)
(declare-fun |*(struct_mmc_host)*@1| (Int ) Int)
(declare-fun |*(struct_mmc_card)*@1| (Int ) Int)
(declare-fun |ldv_sdio_claim_host_1::ldv_func_arg1@4| () Int)
(declare-fun |ldv_sdio_claim_host::dev_id@4| () Int)
(assert (! (= |ldv_sdio_claim_host::dev_id@4| (*signed_int@5 (+ (|*(struct_mmc_host)*@1| (+ (|*(struct_mmc_card)*@1| (+ |ldv_sdio_claim_host_1::ldv_func_arg1@4| 0)) 0)) 1310))) :named term_2106))
(push 1)
(declare-fun |ldv_sdio_claim_host::dev_id@4| () Int)
(declare-fun ldv_sdio_element@7 () Int)
(declare-fun ldv_sdio_element@6 () Int)
(assert (! (and (= ldv_sdio_element@6 0) (= ldv_sdio_element@7 |ldv_sdio_claim_host::dev_id@4|)) :named term_2107))
(push 1)
(assert (! true :named term_2108))
(push 1)
(declare-fun |ath6kl_sdio_io::func@4| () Int)
(declare-fun |ldv_sdio_writesb_2::ldv_func_arg1@4| () Int)
(declare-fun _&_ (Int Int ) Int)
(declare-fun |ath6kl_sdio_io::request@4| () Int)
(declare-fun |ath6kl_sdio_io::addr@9| () Int)
(declare-fun |ath6kl_sdio_io::addr@10| () Int)
(declare-fun |ath6kl_sdio_io::addr@8| () Int)
(declare-fun _&_ (Int Int ) Int)
(declare-fun |ath6kl_sdio_io::len@4| () Int)
(assert (! (and (let ((.cse0 (let ((.cse4 (<= |ath6kl_sdio_io::addr@8| 8191)) (.cse2 (not (= (_&_ |ath6kl_sdio_io::request@4| 2) 0))) (.cse3 (> |ath6kl_sdio_io::addr@8| 2047))) (or (and .cse2 .cse3 .cse4 (= |ath6kl_sdio_io::addr@9| (+ (- |ath6kl_sdio_io::addr@8| |ath6kl_sdio_io::len@4|) 2048))) (and (or (and .cse2 .cse3 (not .cse4)) (and .cse2 (not .cse3))) (= |ath6kl_sdio_io::addr@9| |ath6kl_sdio_io::addr@8|))))) (.cse1 (= |ath6kl_sdio_io::addr@9| 16384))) (or (and .cse0 .cse1 (= |ath6kl_sdio_io::addr@10| (+ (- |ath6kl_sdio_io::addr@9| |ath6kl_sdio_io::len@4|) 12288))) (and .cse0 (not .cse1) (= |ath6kl_sdio_io::addr@10| |ath6kl_sdio_io::addr@9|)))) (not (= (_&_ |ath6kl_sdio_io::request@4| 256) 0)) (= |ldv_sdio_writesb_2::ldv_func_arg1@4| |ath6kl_sdio_io::func@4|)) :named term_2109))
(push 1)
(declare-fun *signed_int@5 (Int ) Int)
(declare-fun |*(struct_mmc_host)*@1| (Int ) Int)
(declare-fun |*(struct_mmc_card)*@1| (Int ) Int)
(declare-fun |ldv_sdio_writesb_2::ldv_func_arg1@4| () Int)
(declare-fun |ldv_check_context::x@4| () Int)
(assert (! (= |ldv_check_context::x@4| (*signed_int@5 (+ (|*(struct_mmc_host)*@1| (+ (|*(struct_mmc_card)*@1| (+ |ldv_sdio_writesb_2::ldv_func_arg1@4| 0)) 0)) 1310))) :named term_2110))
(push 1)
(declare-fun |ldv_check_context::x@4| () Int)
(declare-fun ldv_sdio_element@7 () Int)
(assert (! (= ldv_sdio_element@7 |ldv_check_context::x@4|) :named term_2111))
(push 1)
(declare-fun |ldv_sdio_writesb_2::__retval__@4| () Int)
(declare-fun |ath6kl_sdio_io::ret@10| () Int)
(assert (! (and (= |ldv_sdio_writesb_2::__retval__@4| 0) (= |ath6kl_sdio_io::ret@10| |ldv_sdio_writesb_2::__retval__@4|)) :named term_2112))
(push 1)
(declare-fun |ath6kl_sdio_io::func@4| () Int)
(declare-fun |ldv_sdio_release_host_6::ldv_func_arg1@4| () Int)
(assert (! (= |ldv_sdio_release_host_6::ldv_func_arg1@4| |ath6kl_sdio_io::func@4|) :named term_2113))
(push 1)
(declare-fun *signed_int@5 (Int ) Int)
(declare-fun |*(struct_mmc_host)*@1| (Int ) Int)
(declare-fun |*(struct_mmc_card)*@1| (Int ) Int)
(declare-fun |ldv_sdio_release_host_6::ldv_func_arg1@4| () Int)
(declare-fun |ldv_sdio_release_host::dev_id@4| () Int)
(assert (! (= |ldv_sdio_release_host::dev_id@4| (*signed_int@5 (+ (|*(struct_mmc_host)*@1| (+ (|*(struct_mmc_card)*@1| (+ |ldv_sdio_release_host_6::ldv_func_arg1@4| 0)) 0)) 1310))) :named term_2114))
(push 1)
(declare-fun ldv_sdio_element@8 () Int)
(declare-fun |ldv_sdio_release_host::dev_id@4| () Int)
(declare-fun ldv_sdio_element@7 () Int)
(assert (! (and (= ldv_sdio_element@7 |ldv_sdio_release_host::dev_id@4|) (= ldv_sdio_element@8 0)) :named term_2115))
(push 1)
(assert (! true :named term_2116))
(push 1)
(declare-fun |ath6kl_sdio_io::len@4| () Int)
(declare-fun |trace_ath6kl_sdio::buf_len@4| () Int)
(declare-fun |ath6kl_sdio_io::buf@4| () Int)
(declare-fun |trace_ath6kl_sdio::buf@4| () Int)
(declare-fun |ath6kl_sdio_io::request@4| () Int)
(declare-fun |trace_ath6kl_sdio::flags@4| () Int)
(declare-fun |ath6kl_sdio_io::addr@10| () Int)
(declare-fun |trace_ath6kl_sdio::addr@4| () Int)
(declare-fun __string__ (Int ) Int)
(declare-fun |ath6kl_sdio_io::__CPAchecker_TMP_1@7| () Int)
(declare-fun _&_ (Int Int ) Int)
(declare-fun __string__ (Int ) Int)
(declare-fun |ath6kl_sdio_io::__CPAchecker_TMP_0@7| () Int)
(declare-fun _&_ (Int Int ) Int)
(declare-fun |__ADDRESS_OF_ath6kl_sdio_io::__CPAchecker_TMP_1| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_ath6kl_sdio_io::__CPAchecker_TMP_0| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(assert (! (and (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_ath6kl_sdio_io::__CPAchecker_TMP_0|) |__ADDRESS_OF_ath6kl_sdio_io::__CPAchecker_TMP_0|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_ath6kl_sdio_io::__CPAchecker_TMP_1|) |__ADDRESS_OF_ath6kl_sdio_io::__CPAchecker_TMP_1|) (not (= (_&_ |ath6kl_sdio_io::request@4| 2) 0)) (= |ath6kl_sdio_io::__CPAchecker_TMP_0@7| (__string__ 12)) (not (= (_&_ |ath6kl_sdio_io::request@4| 256) 0)) (= |ath6kl_sdio_io::__CPAchecker_TMP_1@7| (__string__ 13)) (= |trace_ath6kl_sdio::addr@4| |ath6kl_sdio_io::addr@10|) (= |trace_ath6kl_sdio::flags@4| |ath6kl_sdio_io::request@4|) (= |trace_ath6kl_sdio::buf@4| |ath6kl_sdio_io::buf@4|) (= |trace_ath6kl_sdio::buf_len@4| |ath6kl_sdio_io::len@4|)) :named term_2117))
(push 1)
(declare-fun __ADDRESS_OF___tracepoint_ath6kl_sdio () Int)
(declare-fun |static_key_false::key@4| () Int)
(declare-fun |__ADDRESS_OF_trace_ath6kl_sdio::tmp___1| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_trace_ath6kl_sdio::tmp___0| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_trace_ath6kl_sdio::tmp| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_trace_ath6kl_sdio::__warned| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_trace_ath6kl_sdio::_________p1| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_trace_ath6kl_sdio::__data| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_trace_ath6kl_sdio::it_func_ptr| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(assert (! (and (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_trace_ath6kl_sdio::it_func_ptr|) |__ADDRESS_OF_trace_ath6kl_sdio::it_func_ptr|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_trace_ath6kl_sdio::__data|) |__ADDRESS_OF_trace_ath6kl_sdio::__data|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_trace_ath6kl_sdio::_________p1|) |__ADDRESS_OF_trace_ath6kl_sdio::_________p1|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_trace_ath6kl_sdio::__warned|) |__ADDRESS_OF_trace_ath6kl_sdio::__warned|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_trace_ath6kl_sdio::tmp|) |__ADDRESS_OF_trace_ath6kl_sdio::tmp|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_trace_ath6kl_sdio::tmp___0|) |__ADDRESS_OF_trace_ath6kl_sdio::tmp___0|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_trace_ath6kl_sdio::tmp___1|) |__ADDRESS_OF_trace_ath6kl_sdio::tmp___1|) (= |static_key_false::key@4| (+ __ADDRESS_OF___tracepoint_ath6kl_sdio 8))) :named term_2118))
(push 1)
(declare-fun |static_key_false::key@4| () Int)
(declare-fun |atomic_read::v@4| () Int)
(declare-fun |__ADDRESS_OF_static_key_false::tmp___0| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_static_key_false::tmp| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(assert (! (and (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_static_key_false::tmp|) |__ADDRESS_OF_static_key_false::tmp|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_static_key_false::tmp___0|) |__ADDRESS_OF_static_key_false::tmp___0|) (= |atomic_read::v@4| (+ |static_key_false::key@4| 0))) :named term_2119))
(push 1)
(declare-fun |atomic_read::__retval__@4| () Int)
(declare-fun |static_key_false::tmp@7| () Int)
(declare-fun *signed_int@5 (Int ) Int)
(declare-fun |atomic_read::v@4| () Int)
(assert (! (and (= |atomic_read::__retval__@4| (*signed_int@5 (+ |atomic_read::v@4| 0))) (= |static_key_false::tmp@7| |atomic_read::__retval__@4|)) :named term_2120))
(push 1)
(declare-fun |static_key_false::tmp@7| () Int)
(declare-fun |__builtin_expect::exp@4| () Int)
(assert (! (= |__builtin_expect::exp@4| (ite (not (= |static_key_false::tmp@7| 0)) 1 0)) :named term_2121))
(push 1)
(declare-fun |__builtin_expect::__retval__@4| () Int)
(declare-fun |static_key_false::tmp___0@7| () Int)
(declare-fun |__builtin_expect::exp@4| () Int)
(assert (! (and (= |__builtin_expect::__retval__@4| |__builtin_expect::exp@4|) (= |static_key_false::tmp___0@7| |__builtin_expect::__retval__@4|)) :named term_2122))
(push 1)
(declare-fun |static_key_false::__retval__@4| () Int)
(declare-fun |trace_ath6kl_sdio::tmp___1@7| () Int)
(declare-fun |static_key_false::tmp___0@7| () Int)
(assert (! (and (> |static_key_false::tmp___0@7| 0) (= |static_key_false::__retval__@4| 1) (= |trace_ath6kl_sdio::tmp___1@7| |static_key_false::__retval__@4|)) :named term_2123))
(push 1)
(declare-fun |trace_ath6kl_sdio::tmp___1@7| () Int)
(assert (! (not (= |trace_ath6kl_sdio::tmp___1@7| 0)) :named term_2124))
(push 1)
(declare-fun |__ADDRESS_OF_rcu_read_lock_sched_notrace::tmp| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(assert (! (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_rcu_read_lock_sched_notrace::tmp|) |__ADDRESS_OF_rcu_read_lock_sched_notrace::tmp|) :named term_2125))
(push 1)
(declare-fun |current_thread_info::__retval__@6| () Int)
(declare-fun |rcu_read_lock_sched_notrace::tmp@7| () Int)
(declare-fun |current_thread_info::ti@11| () Int)
(declare-fun |current_thread_info::pfo_ret__@6| () Int)
(declare-fun |__ADDRESS_OF_current_thread_info::pfo_ret__| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_current_thread_info::ti| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(assert (! (and (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_current_thread_info::ti|) |__ADDRESS_OF_current_thread_info::ti|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_current_thread_info::pfo_ret__|) |__ADDRESS_OF_current_thread_info::pfo_ret__|) (= |current_thread_info::ti@11| (- |current_thread_info::pfo_ret__@6| 8152)) (= |current_thread_info::__retval__@6| |current_thread_info::ti@11|) (= |rcu_read_lock_sched_notrace::tmp@7| |current_thread_info::__retval__@6|)) :named term_2126))
(push 1)
(declare-fun *signed_int@5 (Int ) Int)
(declare-fun __ADDRESS_OF___tracepoint_ath6kl_sdio () Int)
(declare-fun *signed_int@6 (Int ) Int)
(declare-fun *signed_int@5 (Int ) Int)
(declare-fun |rcu_read_lock_sched_notrace::tmp@7| () Int)
(declare-fun *signed_int@6 (Int ) Int)
(assert (! (and (let ((.cse0 (+ |rcu_read_lock_sched_notrace::tmp@7| 28))) (= (*signed_int@6 .cse0) (+ (*signed_int@5 .cse0) 1))) (let ((.cse1 (+ __ADDRESS_OF___tracepoint_ath6kl_sdio 8))) (= (*signed_int@6 .cse1) (*signed_int@5 .cse1)))) :named term_2127))
(push 1)
(declare-fun |trace_ath6kl_sdio::it_func_ptr@7| () Int)
(declare-fun |trace_ath6kl_sdio::_________p1@7| () Int)
(declare-fun |trace_ath6kl_sdio::tmp@7| () Int)
(declare-fun debug_lockdep_rcu_enabled () Int)
(declare-fun |*(struct_tracepoint_func)*@1| (Int ) Int)
(declare-fun __ADDRESS_OF___tracepoint_ath6kl_sdio () Int)
(declare-fun |trace_ath6kl_sdio::__warned@4| () Int)
(assert (! (and (let ((.cse0 (= |trace_ath6kl_sdio::_________p1@7| (|*(struct_tracepoint_func)*@1| (+ __ADDRESS_OF___tracepoint_ath6kl_sdio 28)))) (.cse1 (= |trace_ath6kl_sdio::tmp@7| debug_lockdep_rcu_enabled)) (.cse2 (= |trace_ath6kl_sdio::tmp@7| 0))) (or (and .cse0 .cse1 (not .cse2) (not (= |trace_ath6kl_sdio::__warned@4| 0))) (and .cse0 .cse1 .cse2))) (= |trace_ath6kl_sdio::it_func_ptr@7| |trace_ath6kl_sdio::_________p1@7|) (= |trace_ath6kl_sdio::it_func_ptr@7| 0)) :named term_2128))
(push 1)
(declare-fun |__ADDRESS_OF_rcu_read_unlock_sched_notrace::tmp| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(assert (! (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_rcu_read_unlock_sched_notrace::tmp|) |__ADDRESS_OF_rcu_read_unlock_sched_notrace::tmp|) :named term_2129))
(push 1)
(declare-fun |current_thread_info::__retval__@7| () Int)
(declare-fun |rcu_read_unlock_sched_notrace::tmp@7| () Int)
(declare-fun |current_thread_info::ti@13| () Int)
(declare-fun |current_thread_info::pfo_ret__@7| () Int)
(declare-fun |__ADDRESS_OF_current_thread_info::pfo_ret__| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_current_thread_info::ti| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(assert (! (and (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_current_thread_info::ti|) |__ADDRESS_OF_current_thread_info::ti|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_current_thread_info::pfo_ret__|) |__ADDRESS_OF_current_thread_info::pfo_ret__|) (= |current_thread_info::ti@13| (- |current_thread_info::pfo_ret__@7| 8152)) (= |current_thread_info::__retval__@7| |current_thread_info::ti@13|) (= |rcu_read_unlock_sched_notrace::tmp@7| |current_thread_info::__retval__@7|)) :named term_2130))
(push 1)
(declare-fun *signed_int@6 (Int ) Int)
(declare-fun __ADDRESS_OF___tracepoint_ath6kl_sdio () Int)
(declare-fun *signed_int@7 (Int ) Int)
(declare-fun *signed_int@6 (Int ) Int)
(declare-fun |rcu_read_unlock_sched_notrace::tmp@7| () Int)
(declare-fun *signed_int@7 (Int ) Int)
(assert (! (and (let ((.cse0 (+ |rcu_read_unlock_sched_notrace::tmp@7| 28))) (= (*signed_int@7 .cse0) (+ (*signed_int@6 .cse0) (- 1)))) (let ((.cse1 (+ __ADDRESS_OF___tracepoint_ath6kl_sdio 8))) (= (*signed_int@7 .cse1) (*signed_int@6 .cse1)))) :named term_2131))
(push 1)
(assert (! true :named term_2132))
(push 1)
(declare-fun |ath6kl_sdio_io::__retval__@4| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::ret@7| () Int)
(declare-fun |ath6kl_sdio_io::ret@10| () Int)
(assert (! (and (= |ath6kl_sdio_io::__retval__@4| |ath6kl_sdio_io::ret@10|) (= |ath6kl_sdio_read_write_sync::ret@7| |ath6kl_sdio_io::__retval__@4|)) :named term_2133))
(push 1)
(declare-fun |ath6kl_sdio_read_write_sync::__retval__@4| () Int)
(declare-fun |ath6kl_set_addrwin_reg::status@5| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::ret@7| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::bounced@10| () Int)
(declare-fun _&_ (Int Int ) Int)
(declare-fun |ath6kl_sdio_read_write_sync::request@4| () Int)
(assert (! (and (let ((.cse0 (= (_&_ |ath6kl_sdio_read_write_sync::request@4| 1) 0)) (.cse1 (= |ath6kl_sdio_read_write_sync::bounced@10| 0))) (or (and .cse0 .cse1) (and .cse0 (not .cse1)))) (= |ath6kl_sdio_read_write_sync::__retval__@4| |ath6kl_sdio_read_write_sync::ret@7|) (= |ath6kl_set_addrwin_reg::status@5| |ath6kl_sdio_read_write_sync::__retval__@4|)) :named term_2134))
(push 1)
(declare-fun |ath6kl_set_addrwin_reg::i@5| () Int)
(declare-fun |ath6kl_set_addrwin_reg::i@6| () Int)
(declare-fun |ath6kl_set_addrwin_reg::status@5| () Int)
(assert (! (and (= |ath6kl_set_addrwin_reg::status@5| 0) (= |ath6kl_set_addrwin_reg::i@6| (+ |ath6kl_set_addrwin_reg::i@5| 1))) :named term_2135))
(push 1)
(declare-fun |ath6kl_sdio_read_write_sync::request@5| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::len@5| () Int)
(declare-fun |__ADDRESS_OF_ath6kl_set_addrwin_reg::addr| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::buf@5| () Int)
(declare-fun |ath6kl_set_addrwin_reg::reg_addr@2| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::addr@5| () Int)
(declare-fun |ath6kl_set_addrwin_reg::ar@2| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::ar@5| () Int)
(declare-fun |ath6kl_set_addrwin_reg::status@5| () Int)
(declare-fun |ath6kl_set_addrwin_reg::i@6| () Int)
(assert (! (and (not (<= |ath6kl_set_addrwin_reg::i@6| 3)) (= |ath6kl_set_addrwin_reg::status@5| 0) (= |ath6kl_sdio_read_write_sync::ar@5| |ath6kl_set_addrwin_reg::ar@2|) (= |ath6kl_sdio_read_write_sync::addr@5| |ath6kl_set_addrwin_reg::reg_addr@2|) (= |ath6kl_sdio_read_write_sync::buf@5| |__ADDRESS_OF_ath6kl_set_addrwin_reg::addr|) (= |ath6kl_sdio_read_write_sync::len@5| 4) (= |ath6kl_sdio_read_write_sync::request@5| 594)) :named term_2136))
(push 1)
(declare-fun |ath6kl_sdio_read_write_sync::ar@5| () Int)
(declare-fun |ath6kl_sdio_priv::ar@5| () Int)
(declare-fun |__ADDRESS_OF_ath6kl_sdio_read_write_sync::tmp___0| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_ath6kl_sdio_read_write_sync::bounced| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_ath6kl_sdio_read_write_sync::ret| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_ath6kl_sdio_read_write_sync::tbuf| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_ath6kl_sdio_read_write_sync::tmp| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_ath6kl_sdio_read_write_sync::ar_sdio| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(assert (! (and (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_ath6kl_sdio_read_write_sync::ar_sdio|) |__ADDRESS_OF_ath6kl_sdio_read_write_sync::ar_sdio|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_ath6kl_sdio_read_write_sync::tmp|) |__ADDRESS_OF_ath6kl_sdio_read_write_sync::tmp|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_ath6kl_sdio_read_write_sync::tbuf|) |__ADDRESS_OF_ath6kl_sdio_read_write_sync::tbuf|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_ath6kl_sdio_read_write_sync::ret|) |__ADDRESS_OF_ath6kl_sdio_read_write_sync::ret|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_ath6kl_sdio_read_write_sync::bounced|) |__ADDRESS_OF_ath6kl_sdio_read_write_sync::bounced|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_ath6kl_sdio_read_write_sync::tmp___0|) |__ADDRESS_OF_ath6kl_sdio_read_write_sync::tmp___0|) (= |ath6kl_sdio_priv::ar@5| |ath6kl_sdio_read_write_sync::ar@5|)) :named term_2137))
(push 1)
(declare-fun |ath6kl_sdio_priv::__retval__@5| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::tmp@9| () Int)
(declare-fun |__ADDRESS_OF_ath6kl_sdio_priv::__CPAchecker_TMP_0| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |ath6kl_sdio_priv::__CPAchecker_TMP_0@5| () Int)
(declare-fun |*(void)*@1| (Int ) Int)
(declare-fun |ath6kl_sdio_priv::ar@5| () Int)
(assert (! (and (= |ath6kl_sdio_priv::__CPAchecker_TMP_0@5| (|*(void)*@1| (+ |ath6kl_sdio_priv::ar@5| 121))) (= |ath6kl_sdio_priv::__retval__@5| |ath6kl_sdio_priv::__CPAchecker_TMP_0@5|) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_ath6kl_sdio_priv::__CPAchecker_TMP_0|) |__ADDRESS_OF_ath6kl_sdio_priv::__CPAchecker_TMP_0|) (= |ath6kl_sdio_read_write_sync::tmp@9| |ath6kl_sdio_priv::__retval__@5|)) :named term_2138))
(push 1)
(declare-fun |ath6kl_sdio_read_write_sync::buf@5| () Int)
(declare-fun |buf_needs_bounce::buf@5| () Int)
(declare-fun _&_ (Int Int ) Int)
(declare-fun |ath6kl_sdio_read_write_sync::request@5| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::bounced@12| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::tbuf@12| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::tmp@9| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::ar_sdio@9| () Int)
(assert (! (and (= |ath6kl_sdio_read_write_sync::ar_sdio@9| |ath6kl_sdio_read_write_sync::tmp@9|) (= |ath6kl_sdio_read_write_sync::tbuf@12| 0) (= |ath6kl_sdio_read_write_sync::bounced@12| 0) (= (_&_ |ath6kl_sdio_read_write_sync::request@5| 128) 0) (= |buf_needs_bounce::buf@5| |ath6kl_sdio_read_write_sync::buf@5|)) :named term_2139))
(push 1)
(declare-fun |buf_needs_bounce::__retval__@5| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::tmp___0@9| () Int)
(declare-fun |buf_needs_bounce::tmp___1@9| () Int)
(declare-fun |buf_needs_bounce::tmp___0@9| () Int)
(declare-fun |buf_needs_bounce::tmp@9| () Int)
(declare-fun __virt_addr_valid (Int ) Int)
(declare-fun |buf_needs_bounce::buf@5| () Int)
(declare-fun _&_ (Int Int ) Int)
(declare-fun |__ADDRESS_OF_buf_needs_bounce::tmp___1| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_buf_needs_bounce::tmp___0| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |__ADDRESS_OF_buf_needs_bounce::tmp| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |buf_needs_bounce::tmp___0@8| () Int)
(declare-fun |buf_needs_bounce::tmp@8| () Int)
(assert (! (and (let ((.cse0 (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_buf_needs_bounce::tmp|) |__ADDRESS_OF_buf_needs_bounce::tmp|)) (.cse1 (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_buf_needs_bounce::tmp___0|) |__ADDRESS_OF_buf_needs_bounce::tmp___0|)) (.cse2 (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_buf_needs_bounce::tmp___1|) |__ADDRESS_OF_buf_needs_bounce::tmp___1|)) (.cse3 (= (_&_ |buf_needs_bounce::buf@5| 3) 0)) (.cse6 (= |buf_needs_bounce::tmp@9| (__virt_addr_valid |buf_needs_bounce::buf@5|))) (.cse7 (= |buf_needs_bounce::tmp@9| 0)) (.cse8 (= |buf_needs_bounce::tmp___0@9| 0)) (.cse4 (= |buf_needs_bounce::tmp___1@9| 1)) (.cse5 (= |buf_needs_bounce::__retval__@5| |buf_needs_bounce::tmp___1@9|))) (or (and .cse0 .cse1 .cse2 (not .cse3) .cse4 .cse5 (= |buf_needs_bounce::tmp@9| |buf_needs_bounce::tmp@8|) (= |buf_needs_bounce::tmp___0@9| |buf_needs_bounce::tmp___0@8|)) (and .cse0 .cse1 .cse2 .cse3 .cse6 (not .cse7) .cse8 (= |buf_needs_bounce::tmp___1@9| 0) .cse5) (and .cse0 .cse1 .cse2 .cse3 .cse6 .cse7 (= |buf_needs_bounce::tmp___0@9| 1) (not .cse8) .cse4 .cse5))) (= |ath6kl_sdio_read_write_sync::tmp___0@9| |buf_needs_bounce::__retval__@5|)) :named term_2140))
(push 1)
(declare-fun |ath6kl_sdio_read_write_sync::len@5| () Int)
(declare-fun |ath6kl_sdio_io::len@5| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::tbuf@13| () Int)
(declare-fun |ath6kl_sdio_io::buf@5| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::addr@5| () Int)
(declare-fun |ath6kl_sdio_io::addr@11| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::request@5| () Int)
(declare-fun |ath6kl_sdio_io::request@5| () Int)
(declare-fun |*(struct_sdio_func)*@1| (Int ) Int)
(declare-fun |ath6kl_sdio_read_write_sync::ar_sdio@9| () Int)
(declare-fun |ath6kl_sdio_io::func@5| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::bounced@13| () Int)
(declare-fun _&_ (Int Int ) Int)
(declare-fun |*(unsigned_char)*@1| (Int ) Int)
(declare-fun |ath6kl_sdio_read_write_sync::__CPAchecker_TMP_0@5| () Int)
(declare-fun |__ADDRESS_OF_ath6kl_sdio_read_write_sync::__CPAchecker_TMP_0| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |ath6kl_sdio_read_write_sync::tmp___0@9| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::bounced@12| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::__CPAchecker_TMP_0@4| () Int)
(declare-fun |ath6kl_sdio_read_write_sync::buf@5| () Int)
(assert (! (and (let ((.cse0 (= |ath6kl_sdio_read_write_sync::tmp___0@9| 0))) (or (and .cse0 (= |ath6kl_sdio_read_write_sync::tbuf@13| |ath6kl_sdio_read_write_sync::buf@5|) (= |ath6kl_sdio_read_write_sync::__CPAchecker_TMP_0@5| |ath6kl_sdio_read_write_sync::__CPAchecker_TMP_0@4|) (= |ath6kl_sdio_read_write_sync::bounced@13| |ath6kl_sdio_read_write_sync::bounced@12|)) (let ((.cse1 (|*(unsigned_char)*@1| (+ |ath6kl_sdio_read_write_sync::ar_sdio@9| 3684)))) (and (not .cse0) (= |ath6kl_sdio_read_write_sync::__CPAchecker_TMP_0@5| .cse1) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_ath6kl_sdio_read_write_sync::__CPAchecker_TMP_0|) |__ADDRESS_OF_ath6kl_sdio_read_write_sync::__CPAchecker_TMP_0|) (not (= |ath6kl_sdio_read_write_sync::__CPAchecker_TMP_0@5| 0)) (= |ath6kl_sdio_read_write_sync::tbuf@13| .cse1) (not (= (_&_ |ath6kl_sdio_read_write_sync::request@5| 2) 0)) (= |ath6kl_sdio_read_write_sync::bounced@13| 1))))) (= |ath6kl_sdio_io::func@5| (|*(struct_sdio_func)*@1| (+ |ath6kl_sdio_read_write_sync::ar_sdio@9| 0))) (= |ath6kl_sdio_io::request@5| |ath6kl_sdio_read_write_sync::request@5|) (= |ath6kl_sdio_io::addr@11| |ath6kl_sdio_read_write_sync::addr@5|) (= |ath6kl_sdio_io::buf@5| |ath6kl_sdio_read_write_sync::tbuf@13|) (= |ath6kl_sdio_io::len@5| |ath6kl_sdio_read_write_sync::len@5|)) :named term_2141))
(push 1)
(declare-fun |ath6kl_sdio_io::func@5| () Int)
(declare-fun |ldv_sdio_claim_host_1::ldv_func_arg1@5| () Int)
(declare-fun |__ADDRESS_OF_ath6kl_sdio_io::ret| () Int)
(declare-fun __BASE_ADDRESS_OF__ (Int ) Int)
(declare-fun |ath6kl_sdio_io::ret@12| () Int)
(assert (! (and (= |ath6kl_sdio_io::ret@12| 0) (= (__BASE_ADDRESS_OF__ |__ADDRESS_OF_ath6kl_sdio_io::ret|) |__ADDRESS_OF_ath6kl_sdio_io::ret|) (= |ldv_sdio_claim_host_1::ldv_func_arg1@5| |ath6kl_sdio_io::func@5|)) :named term_2142))
(push 1)
(declare-fun *signed_int@7 (Int ) Int)
(declare-fun |*(struct_mmc_host)*@1| (Int ) Int)
(declare-fun |*(struct_mmc_card)*@1| (Int ) Int)
(declare-fun |ldv_sdio_claim_host_1::ldv_func_arg1@5| () Int)
(declare-fun |ldv_sdio_claim_host::dev_id@5| () Int)
(assert (! (= |ldv_sdio_claim_host::dev_id@5| (*signed_int@7 (+ (|*(struct_mmc_host)*@1| (+ (|*(struct_mmc_card)*@1| (+ |ldv_sdio_claim_host_1::ldv_func_arg1@5| 0)) 0)) 1310))) :named term_2143))
(push 1)
(declare-fun |ldv_sdio_claim_host::dev_id@5| () Int)
(declare-fun ldv_sdio_element@9 () Int)
(declare-fun ldv_sdio_element@8 () Int)
(assert (! (and (= ldv_sdio_element@8 0) (= ldv_sdio_element@9 |ldv_sdio_claim_host::dev_id@5|)) :named term_2144))
(push 1)
(assert (! true :named term_2145))
(push 1)
(declare-fun |ath6kl_sdio_io::func@5| () Int)
(declare-fun |ldv_sdio_memcpy_toio_3::ldv_func_arg1@2| () Int)
(declare-fun _&_ (Int Int ) Int)
(declare-fun |ath6kl_sdio_io::request@5| () Int)
(declare-fun |ath6kl_sdio_io::addr@12| () Int)
(declare-fun |ath6kl_sdio_io::addr@13| () Int)
(declare-fun |ath6kl_sdio_io::addr@11| () Int)
(declare-fun _&_ (Int Int ) Int)
(declare-fun |ath6kl_sdio_io::len@5| () Int)
(assert (! (and (let ((.cse0 (let ((.cse4 (<= |ath6kl_sdio_io::addr@11| 8191)) (.cse2 (not (= (_&_ |ath6kl_sdio_io::request@5| 2) 0))) (.cse3 (> |ath6kl_sdio_io::addr@11| 2047))) (or (and .cse2 .cse3 .cse4 (= |ath6kl_sdio_io::addr@12| (+ (- |ath6kl_sdio_io::addr@11| |ath6kl_sdio_io::len@5|) 2048))) (and (or (and .cse2 .cse3 (not .cse4)) (and .cse2 (not .cse3))) (= |ath6kl_sdio_io::addr@12| |ath6kl_sdio_io::addr@11|))))) (.cse1 (= |ath6kl_sdio_io::addr@12| 16384))) (or (and .cse0 .cse1 (= |ath6kl_sdio_io::addr@13| (+ (- |ath6kl_sdio_io::addr@12| |ath6kl_sdio_io::len@5|) 12288))) (and .cse0 (not .cse1) (= |ath6kl_sdio_io::addr@13| |ath6kl_sdio_io::addr@12|)))) (= (_&_ |ath6kl_sdio_io::request@5| 256) 0) (= |ldv_sdio_memcpy_toio_3::ldv_func_arg1@2| |ath6kl_sdio_io::func@5|)) :named term_2146))
(push 1)
(declare-fun *signed_int@7 (Int ) Int)
(declare-fun |*(struct_mmc_host)*@1| (Int ) Int)
(declare-fun |*(struct_mmc_card)*@1| (Int ) Int)
(declare-fun |ldv_sdio_memcpy_toio_3::ldv_func_arg1@2| () Int)
(declare-fun |ldv_check_context::x@5| () Int)
(assert (! (= |ldv_check_context::x@5| (*signed_int@7 (+ (|*(struct_mmc_host)*@1| (+ (|*(struct_mmc_card)*@1| (+ |ldv_sdio_memcpy_toio_3::ldv_func_arg1@2| 0)) 0)) 1310))) :named term_2147))
(push 1)
(declare-fun |ldv_check_context::x@5| () Int)
(declare-fun ldv_sdio_element@9 () Int)
(assert (! (not (= ldv_sdio_element@9 |ldv_check_context::x@5|)) :named term_2148))
(push 1)
(assert (! true :named term_2149))
(check-sat)
(get-interpolants term_2019 (and term_2020 term_2021 term_2022 term_2023 term_2024 term_2025 term_2026 term_2027 term_2028 term_2029 term_2030 term_2031 term_2032 term_2033 term_2034 term_2035 term_2036 term_2037 term_2038 term_2039 term_2040 term_2041 term_2042 term_2043 term_2044 term_2045 term_2046 term_2047 term_2048 term_2049 term_2050 term_2051 term_2052 term_2053 term_2054 term_2055 term_2056 term_2057 term_2058 term_2059 term_2060 term_2061 term_2062 term_2063 term_2064 term_2065 term_2066 term_2067 term_2068 term_2069 term_2070 term_2071 term_2072 term_2073 term_2074 term_2075 term_2076 term_2077 term_2078 term_2079 term_2080 term_2081 term_2082 term_2083 term_2084 term_2085 term_2086 term_2087 term_2088 term_2089 term_2090 term_2091 term_2092 term_2093 term_2094 term_2095 term_2096 term_2097 term_2098 term_2099 term_2100 term_2101 term_2102 term_2103 term_2104 term_2105 term_2106 term_2107 term_2108 term_2109 term_2110 term_2111 term_2112 term_2113 term_2114 term_2115 term_2116 term_2117 term_2118 term_2119 term_2120 term_2121 term_2122 term_2123 term_2124 term_2125 term_2126 term_2127 term_2128 term_2129 term_2130 term_2131 term_2132 term_2133 term_2134 term_2135 term_2136 term_2137 term_2138 term_2139 term_2140 term_2141 term_2142 term_2143 term_2144 term_2145 term_2146 term_2147 term_2148 term_2149))