Commit 1fc15b8f authored by Alain Mebsout's avatar Alain Mebsout
Browse files

Importing snapshot 2015-06-01

parents
Pipeline #55 skipped
(set-logic QF_UFLRA)
(set-info :source |CPAchecker with bounded model checking on SV-COMP14 program using MathSAT5, submitted by Philipp Wendler, http://cpachecker.sosy-lab.org|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(define-fun _2 () Bool false)
(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(exit)
(set-logic QF_UFLRA)
(set-info :source |CPAchecker with bounded model checking on SV-COMP14 program using MathSAT5, submitted by Philipp Wendler, http://cpachecker.sosy-lab.org|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(define-fun _2 () Bool false)
(declare-fun __ADDRESS_OF____pc () Real)
(declare-fun |__ADDRESS_OF_main::tmp___1| () Real)
(declare-fun |__ADDRESS_OF_main::tmp| () Real)
(declare-fun __ADDRESS_OF___this_module () Real)
(declare-fun |__ADDRESS_OF_init_teles_cs::tmp| () Real)
(declare-fun pcmcia_register_driver (Real) Real)
(declare-fun |__ADDRESS_OF_main::res_teles_probe_0| () Real)
(declare-fun |init_teles_cs::tmp@3| () Real)
(declare-fun __BASE_ADDRESS_OF__ (Real) Real)
(declare-fun __ADDRESS_OF_teles_cs_driver () Real)
(declare-fun ldv_spin@2 () Real)
(declare-fun __ADDRESS_OF_teles_ids () Real)
(declare-fun |main::ldv_s_teles_cs_driver_pcmcia_driver@3| () Real)
(declare-fun ___pc@4 () Real)
(declare-fun __ADDRESS_OF_ldv_spin () Real)
(declare-fun ___pc@3 () Real)
(declare-fun __ADDRESS_OF_protocol () Real)
(declare-fun |__ADDRESS_OF_main::ldv_s_teles_cs_driver_pcmcia_driver| () Real)
(declare-fun |init_teles_cs::__retval__@2| () Real)
(declare-fun |__ADDRESS_OF_main::tmp___0| () Real)
(declare-fun |__ADDRESS_OF_main::var_group1| () Real)
(declare-fun protocol@2 () Real)
(declare-fun |main::tmp@3| () Real)
(define-fun _7 () Real 0)
(define-fun _8 () Real __ADDRESS_OF____pc)
(define-fun _9 () Real (__BASE_ADDRESS_OF__ _8))
(define-fun _10 () Bool (= _8 _9))
(define-fun _11 () Real ___pc@3)
(define-fun _12 () Bool (= _11 _7))
(define-fun _13 () Bool (and _10 _12))
(define-fun _14 () Real 1)
(define-fun _16 () Bool (and _12 _13))
(define-fun _19 () Real __ADDRESS_OF___this_module)
(define-fun _20 () Real (__BASE_ADDRESS_OF__ _19))
(define-fun _21 () Bool (= _19 _20))
(define-fun _22 () Bool (<= _19 _7))
(define-fun _23 () Bool (not _22))
(define-fun _24 () Bool (and _21 _23))
(define-fun _25 () Bool (and _16 _24))
(define-fun _26 () Real __ADDRESS_OF_protocol)
(define-fun _27 () Real (__BASE_ADDRESS_OF__ _26))
(define-fun _28 () Bool (= _26 _27))
(define-fun _31 () Real (- 581))
(define-fun _32 () Bool (<= _19 _31))
(define-fun _33 () Bool (not _32))
(define-fun _34 () Real (- 1))
(define-fun _35 () Real (* (- 1) _26))
(define-fun _36 () Real (+ _19 _35))
(define-fun _37 () Bool (<= _36 _31))
(define-fun _38 () Bool (and _33 _37))
(define-fun _39 () Real 2)
(define-fun _40 () Real protocol@2)
(define-fun _41 () Bool (= _40 _39))
(define-fun _42 () Bool (and _28 _38))
(define-fun _43 () Bool (and _41 _42))
(define-fun _44 () Bool (and _25 _43))
(define-fun _45 () Real __ADDRESS_OF_teles_ids)
(define-fun _46 () Real (__BASE_ADDRESS_OF__ _45))
(define-fun _47 () Bool (= _45 _46))
(define-fun _50 () Real (- 4))
(define-fun _51 () Bool (<= _26 _50))
(define-fun _52 () Bool (not _51))
(define-fun _53 () Real (* (- 1) _45))
(define-fun _54 () Real (+ _26 _53))
(define-fun _55 () Bool (<= _54 _50))
(define-fun _56 () Bool (and _52 _55))
(define-fun _57 () Bool (and _47 _56))
(define-fun _58 () Bool (and _44 _57))
(define-fun _59 () Real __ADDRESS_OF_teles_cs_driver)
(define-fun _60 () Real (__BASE_ADDRESS_OF__ _59))
(define-fun _61 () Bool (= _59 _60))
(define-fun _64 () Real (- 146))
(define-fun _65 () Bool (<= _45 _64))
(define-fun _66 () Bool (not _65))
(define-fun _67 () Real (* (- 1) _59))
(define-fun _68 () Real (+ _45 _67))
(define-fun _69 () Bool (<= _68 _64))
(define-fun _70 () Bool (and _66 _69))
(define-fun _71 () Bool (and _61 _70))
(define-fun _72 () Bool (and _58 _71))
(define-fun _73 () Real __ADDRESS_OF_ldv_spin)
(define-fun _74 () Real (__BASE_ADDRESS_OF__ _73))
(define-fun _75 () Bool (= _73 _74))
(define-fun _76 () Real ldv_spin@2)
(define-fun _77 () Bool (= _76 _7))
(define-fun _78 () Bool (and _75 _77))
(define-fun _79 () Bool (and _72 _78))
(define-fun _80 () Real |__ADDRESS_OF_main::var_group1|)
(define-fun _81 () Real (__BASE_ADDRESS_OF__ _80))
(define-fun _82 () Bool (= _80 _81))
(define-fun _83 () Bool (and _79 _82))
(define-fun _84 () Real |__ADDRESS_OF_main::res_teles_probe_0|)
(define-fun _85 () Real (__BASE_ADDRESS_OF__ _84))
(define-fun _86 () Bool (= _84 _85))
(define-fun _87 () Bool (and _83 _86))
(define-fun _88 () Real |__ADDRESS_OF_main::ldv_s_teles_cs_driver_pcmcia_driver|)
(define-fun _89 () Real (__BASE_ADDRESS_OF__ _88))
(define-fun _90 () Bool (= _88 _89))
(define-fun _91 () Bool (and _87 _90))
(define-fun _92 () Real |__ADDRESS_OF_main::tmp|)
(define-fun _93 () Real (__BASE_ADDRESS_OF__ _92))
(define-fun _94 () Bool (= _92 _93))
(define-fun _95 () Bool (and _91 _94))
(define-fun _96 () Real |__ADDRESS_OF_main::tmp___0|)
(define-fun _97 () Real (__BASE_ADDRESS_OF__ _96))
(define-fun _98 () Bool (= _96 _97))
(define-fun _99 () Bool (and _95 _98))
(define-fun _100 () Real |__ADDRESS_OF_main::tmp___1|)
(define-fun _101 () Real (__BASE_ADDRESS_OF__ _100))
(define-fun _102 () Bool (= _100 _101))
(define-fun _103 () Bool (and _99 _102))
(define-fun _104 () Real |main::ldv_s_teles_cs_driver_pcmcia_driver@3|)
(define-fun _105 () Bool (= _104 _7))
(define-fun _106 () Bool (and _103 _105))
(define-fun _108 () Real |__ADDRESS_OF_init_teles_cs::tmp|)
(define-fun _109 () Real (__BASE_ADDRESS_OF__ _108))
(define-fun _110 () Bool (= _108 _109))
(define-fun _111 () Bool (and _106 _110))
(define-fun _112 () Real (pcmcia_register_driver _59))
(define-fun _113 () Real |init_teles_cs::tmp@3|)
(define-fun _114 () Bool (= _112 _113))
(define-fun _115 () Bool (and _111 _114))
(define-fun _116 () Real |init_teles_cs::__retval__@2|)
(define-fun _117 () Bool (= _113 _116))
(define-fun _118 () Bool (and _115 _117))
(define-fun _119 () Real |main::tmp@3|)
(define-fun _120 () Bool (= _116 _119))
(define-fun _121 () Bool (and _118 _120))
(define-fun _122 () Bool (= _119 _7))
(define-fun _126 () Bool (and _121 _122))
(define-fun _127 () Real ___pc@4)
(define-fun _128 () Bool (= _127 _14))
(define-fun _129 () Bool (and _126 _128))
(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(push 1)
(assert _129)
(set-info :status sat)
(check-sat)
(pop 1)
(exit)
(set-logic QF_UFLRA)
(set-info :source |CPAchecker with bounded model checking on SV-COMP14 program using MathSAT5, submitted by Philipp Wendler, http://cpachecker.sosy-lab.org|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(define-fun _2 () Bool false)
(declare-fun |__ADDRESS_OF_main::tmp___0| () Real)
(declare-fun |main::ldv_s_pca9633_driver_i2c_driver@3| () Real)
(declare-fun ldv_spin@2 () Real)
(declare-fun __ADDRESS_OF_ldv_spin () Real)
(declare-fun |__ADDRESS_OF_main::tmp| () Real)
(declare-fun ___pc@4 () Real)
(declare-fun ___pc@3 () Real)
(declare-fun |__ADDRESS_OF_main::var_group1| () Real)
(declare-fun __BASE_ADDRESS_OF__ (Real) Real)
(declare-fun |__ADDRESS_OF_main::res_pca9633_probe_2| () Real)
(declare-fun |__ADDRESS_OF_main::ldv_s_pca9633_driver_i2c_driver| () Real)
(declare-fun __ADDRESS_OF____pc () Real)
(define-fun _7 () Real 0)
(define-fun _8 () Real __ADDRESS_OF____pc)
(define-fun _9 () Real (__BASE_ADDRESS_OF__ _8))
(define-fun _10 () Bool (= _8 _9))
(define-fun _11 () Real ___pc@3)
(define-fun _12 () Bool (= _11 _7))
(define-fun _13 () Bool (and _10 _12))
(define-fun _14 () Real 1)
(define-fun _16 () Bool (and _12 _13))
(define-fun _19 () Real __ADDRESS_OF_ldv_spin)
(define-fun _20 () Real (__BASE_ADDRESS_OF__ _19))
(define-fun _21 () Bool (= _19 _20))
(define-fun _22 () Real ldv_spin@2)
(define-fun _23 () Bool (= _22 _7))
(define-fun _24 () Bool (and _21 _23))
(define-fun _25 () Bool (and _16 _24))
(define-fun _26 () Real |__ADDRESS_OF_main::var_group1|)
(define-fun _27 () Real (__BASE_ADDRESS_OF__ _26))
(define-fun _28 () Bool (= _26 _27))
(define-fun _29 () Bool (and _25 _28))
(define-fun _30 () Real |__ADDRESS_OF_main::res_pca9633_probe_2|)
(define-fun _31 () Real (__BASE_ADDRESS_OF__ _30))
(define-fun _32 () Bool (= _30 _31))
(define-fun _33 () Bool (and _29 _32))
(define-fun _34 () Real |__ADDRESS_OF_main::ldv_s_pca9633_driver_i2c_driver|)
(define-fun _35 () Real (__BASE_ADDRESS_OF__ _34))
(define-fun _36 () Bool (= _34 _35))
(define-fun _37 () Bool (and _33 _36))
(define-fun _38 () Real |__ADDRESS_OF_main::tmp|)
(define-fun _39 () Real (__BASE_ADDRESS_OF__ _38))
(define-fun _40 () Bool (= _38 _39))
(define-fun _41 () Bool (and _37 _40))
(define-fun _42 () Real |__ADDRESS_OF_main::tmp___0|)
(define-fun _43 () Real (__BASE_ADDRESS_OF__ _42))
(define-fun _44 () Bool (= _42 _43))
(define-fun _45 () Bool (and _41 _44))
(define-fun _46 () Real |main::ldv_s_pca9633_driver_i2c_driver@3|)
(define-fun _47 () Bool (= _46 _7))
(define-fun _48 () Bool (and _45 _47))
(define-fun _50 () Real ___pc@4)
(define-fun _51 () Bool (= _50 _14))
(define-fun _52 () Bool (and _48 _51))
(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(push 1)
(assert _52)
(set-info :status sat)
(check-sat)
(pop 1)
(exit)
(set-logic QF_UFLRA)
(set-info :source |CPAchecker with bounded model checking on SV-COMP14 program using MathSAT5, submitted by Philipp Wendler, http://cpachecker.sosy-lab.org|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(define-fun _2 () Bool false)
(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(exit)
(set-logic QF_UFLRA)
(set-info :source |CPAchecker with bounded model checking on SV-COMP14 program using MathSAT5, submitted by Philipp Wendler, http://cpachecker.sosy-lab.org|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(define-fun _2 () Bool false)
(declare-fun __ADDRESS_OF_pcc_device_ids () Real)
(declare-fun |__ADDRESS_OF_main::var_acpi_pcc_hotkey_notify_11_p1| () Real)
(declare-fun __ADDRESS_OF_pcc_backlight_ops () Real)
(declare-fun |acpi_pcc_init::result@4| () Real)
(declare-fun ___pc@3 () Real)
(declare-fun __ADDRESS_OF_panasonic_keymap () Real)
(declare-fun __ADDRESS_OF_ldv_spin () Real)
(declare-fun __ADDRESS_OF_acpi_disabled () Real)
(declare-fun |__ADDRESS_OF_main::tmp___0| () Real)
(declare-fun |__ADDRESS_OF_main::var_group1| () Real)
(declare-fun __ADDRESS_OF_dev_attr_sticky_key () Real)
(declare-fun __ADDRESS_OF_pcc_attr_group () Real)
(declare-fun __ADDRESS_OF_pcc_sysfs_entries () Real)
(declare-fun acpi_bus_register_driver (Real) Real)
(declare-fun |__ADDRESS_OF_main::tmp| () Real)
(declare-fun |__ADDRESS_OF_main::tmp___1| () Real)
(declare-fun |__ADDRESS_OF_acpi_pcc_init::result| () Real)
(declare-fun |acpi_pcc_init::__retval__@2| () Real)
(declare-fun |main::tmp@3| () Real)
(declare-fun __ADDRESS_OF____pc () Real)
(declare-fun ldv_spin@2 () Real)
(declare-fun ___pc@4 () Real)
(declare-fun |acpi_pcc_init::result@3| () Real)
(declare-fun __ADDRESS_OF_dev_attr_lcdtype () Real)
(declare-fun __ADDRESS_OF_dev_attr_numbatt () Real)
(declare-fun |__ADDRESS_OF_main::var_group2| () Real)
(declare-fun acpi_disabled@2 () Real)
(declare-fun __BASE_ADDRESS_OF__ (Real) Real)
(declare-fun __ADDRESS_OF_acpi_pcc_driver () Real)
(declare-fun __ADDRESS_OF_dev_attr_mute () Real)
(define-fun _7 () Real 0)
(define-fun _8 () Real __ADDRESS_OF____pc)
(define-fun _9 () Real (__BASE_ADDRESS_OF__ _8))
(define-fun _10 () Bool (= _8 _9))
(define-fun _11 () Real ___pc@3)
(define-fun _12 () Bool (= _11 _7))
(define-fun _13 () Bool (and _10 _12))
(define-fun _14 () Real 1)
(define-fun _16 () Bool (and _12 _13))
(define-fun _19 () Real __ADDRESS_OF_acpi_disabled)
(define-fun _20 () Real (__BASE_ADDRESS_OF__ _19))
(define-fun _21 () Bool (= _19 _20))
(define-fun _22 () Bool (and _16 _21))
(define-fun _23 () Real __ADDRESS_OF_pcc_device_ids)
(define-fun _24 () Real (__BASE_ADDRESS_OF__ _23))
(define-fun _25 () Bool (= _23 _24))
(define-fun _26 () Bool (<= _23 _7))
(define-fun _27 () Bool (not _26))
(define-fun _28 () Bool (and _25 _27))
(define-fun _29 () Bool (and _22 _28))
(define-fun _30 () Real __ADDRESS_OF_acpi_pcc_driver)
(define-fun _31 () Real (__BASE_ADDRESS_OF__ _30))
(define-fun _32 () Bool (= _30 _31))
(define-fun _35 () Real (- 120))
(define-fun _36 () Bool (<= _23 _35))
(define-fun _37 () Bool (not _36))
(define-fun _38 () Real (- 1))
(define-fun _39 () Real (* (- 1) _30))
(define-fun _40 () Real (+ _23 _39))
(define-fun _41 () Bool (<= _40 _35))
(define-fun _42 () Bool (and _37 _41))
(define-fun _43 () Bool (and _32 _42))
(define-fun _44 () Bool (and _29 _43))
(define-fun _45 () Real __ADDRESS_OF_panasonic_keymap)
(define-fun _46 () Real (__BASE_ADDRESS_OF__ _45))
(define-fun _47 () Bool (= _45 _46))
(define-fun _50 () Real (- 349))
(define-fun _51 () Bool (<= _30 _50))
(define-fun _52 () Bool (not _51))
(define-fun _53 () Real (* (- 1) _45))
(define-fun _54 () Real (+ _30 _53))
(define-fun _55 () Bool (<= _54 _50))
(define-fun _56 () Bool (and _52 _55))
(define-fun _57 () Bool (and _47 _56))
(define-fun _58 () Bool (and _44 _57))
(define-fun _59 () Real __ADDRESS_OF_pcc_backlight_ops)
(define-fun _60 () Real (__BASE_ADDRESS_OF__ _59))
(define-fun _61 () Bool (= _59 _60))
(define-fun _63 () Bool (<= _45 _35))
(define-fun _64 () Bool (not _63))
(define-fun _65 () Real (* (- 1) _59))
(define-fun _66 () Real (+ _45 _65))
(define-fun _67 () Bool (<= _66 _35))
(define-fun _68 () Bool (and _64 _67))
(define-fun _69 () Bool (and _61 _68))
(define-fun _70 () Bool (and _58 _69))
(define-fun _71 () Real __ADDRESS_OF_dev_attr_numbatt)
(define-fun _72 () Real (__BASE_ADDRESS_OF__ _71))
(define-fun _73 () Bool (= _71 _72))
(define-fun _76 () Real (- 28))
(define-fun _77 () Bool (<= _59 _76))
(define-fun _78 () Bool (not _77))
(define-fun _79 () Real (* (- 1) _71))
(define-fun _80 () Real (+ _59 _79))
(define-fun _81 () Bool (<= _80 _76))
(define-fun _82 () Bool (and _78 _81))
(define-fun _83 () Bool (and _73 _82))
(define-fun _84 () Bool (and _70 _83))
(define-fun _85 () Real __ADDRESS_OF_dev_attr_lcdtype)
(define-fun _86 () Real (__BASE_ADDRESS_OF__ _85))
(define-fun _87 () Bool (= _85 _86))
(define-fun _90 () Real (- 42))
(define-fun _91 () Bool (<= _71 _90))
(define-fun _92 () Bool (not _91))
(define-fun _93 () Real (* (- 1) _85))
(define-fun _94 () Real (+ _71 _93))
(define-fun _95 () Bool (<= _94 _90))
(define-fun _96 () Bool (and _92 _95))
(define-fun _97 () Bool (and _87 _96))
(define-fun _98 () Bool (and _84 _97))
(define-fun _99 () Real __ADDRESS_OF_dev_attr_mute)
(define-fun _100 () Real (__BASE_ADDRESS_OF__ _99))
(define-fun _101 () Bool (= _99 _100))
(define-fun _103 () Bool (<= _85 _90))
(define-fun _104 () Bool (not _103))
(define-fun _105 () Real (* (- 1) _99))
(define-fun _106 () Real (+ _85 _105))
(define-fun _107 () Bool (<= _106 _90))
(define-fun _108 () Bool (and _104 _107))
(define-fun _109 () Bool (and _101 _108))
(define-fun _110 () Bool (and _98 _109))
(define-fun _111 () Real __ADDRESS_OF_dev_attr_sticky_key)
(define-fun _112 () Real (__BASE_ADDRESS_OF__ _111))
(define-fun _113 () Bool (= _111 _112))
(define-fun _115 () Bool (<= _99 _90))
(define-fun _116 () Bool (not _115))
(define-fun _117 () Real (* (- 1) _111))
(define-fun _118 () Real (+ _99 _117))
(define-fun _119 () Bool (<= _118 _90))
(define-fun _120 () Bool (and _116 _119))
(define-fun _121 () Bool (and _113 _120))
(define-fun _122 () Bool (and _110 _121))
(define-fun _123 () Real __ADDRESS_OF_pcc_sysfs_entries)
(define-fun _124 () Real (__BASE_ADDRESS_OF__ _123))
(define-fun _125 () Bool (= _123 _124))
(define-fun _127 () Bool (<= _111 _90))
(define-fun _128 () Bool (not _127))
(define-fun _129 () Real (* (- 1) _123))
(define-fun _130 () Real (+ _111 _129))
(define-fun _131 () Bool (<= _130 _90))
(define-fun _132 () Bool (and _128 _131))
(define-fun _133 () Bool (and _125 _132))
(define-fun _134 () Bool (and _122 _133))
(define-fun _135 () Real __ADDRESS_OF_pcc_attr_group)
(define-fun _136 () Real (__BASE_ADDRESS_OF__ _135))
(define-fun _137 () Bool (= _135 _136))
(define-fun _140 () Real (- 40))
(define-fun _141 () Bool (<= _123 _140))
(define-fun _142 () Bool (not _141))
(define-fun _143 () Real (* (- 1) _135))
(define-fun _144 () Real (+ _123 _143))
(define-fun _145 () Bool (<= _144 _140))
(define-fun _146 () Bool (and _142 _145))
(define-fun _147 () Bool (and _137 _146))
(define-fun _148 () Bool (and _134 _147))
(define-fun _149 () Real __ADDRESS_OF_ldv_spin)
(define-fun _150 () Real (__BASE_ADDRESS_OF__ _149))
(define-fun _151 () Bool (= _149 _150))
(define-fun _152 () Real ldv_spin@2)
(define-fun _153 () Bool (= _152 _7))
(define-fun _154 () Bool (and _151 _153))
(define-fun _155 () Bool (and _148 _154))
(define-fun _156 () Real |__ADDRESS_OF_main::var_group1|)
(define-fun _157 () Real (__BASE_ADDRESS_OF__ _156))
(define-fun _158 () Bool (= _156 _157))
(define-fun _159 () Bool (and _155 _158))
(define-fun _160 () Real |__ADDRESS_OF_main::var_acpi_pcc_hotkey_notify_11_p1|)
(define-fun _161 () Real (__BASE_ADDRESS_OF__ _160))
(define-fun _162 () Bool (= _160 _161))
(define-fun _163 () Bool (and _159 _162))
(define-fun _164 () Real |__ADDRESS_OF_main::var_group2|)
(define-fun _165 () Real (__BASE_ADDRESS_OF__ _164))
(define-fun _166 () Bool (= _164 _165))
(define-fun _167 () Bool (and _163 _166))
(define-fun _168 () Real |__ADDRESS_OF_main::tmp|)
(define-fun _169 () Real (__BASE_ADDRESS_OF__ _168))
(define-fun _170 () Bool (= _168 _169))
(define-fun _171 () Bool (and _167 _170))
(define-fun _172 () Real |__ADDRESS_OF_main::tmp___0|)
(define-fun _173 () Real (__BASE_ADDRESS_OF__ _172))
(define-fun _174 () Bool (= _172 _173))
(define-fun _175 () Bool (and _171 _174))
(define-fun _176 () Real |__ADDRESS_OF_main::tmp___1|)
(define-fun _177 () Real (__BASE_ADDRESS_OF__ _176))
(define-fun _178 () Bool (= _176 _177))
(define-fun _179 () Bool (and _175 _178))
(define-fun _181 () Real |__ADDRESS_OF_acpi_pcc_init::result|)
(define-fun _182 () Real (__BASE_ADDRESS_OF__ _181))
(define-fun _183 () Bool (= _181 _182))
(define-fun _184 () Bool (and _179 _183))
(define-fun _185 () Real |acpi_pcc_init::result@3|)
(define-fun _186 () Bool (= _185 _7))
(define-fun _187 () Bool (and _184 _186))
(define-fun _188 () Real acpi_disabled@2)
(define-fun _189 () Bool (= _188 _7))
(define-fun _193 () Bool (and _187 _189))
(define-fun _194 () Real (acpi_bus_register_driver _30))
(define-fun _195 () Real |acpi_pcc_init::result@4|)
(define-fun _196 () Bool (= _194 _195))
(define-fun _197 () Bool (and _193 _196))
(define-fun _198 () Bool (<= _7 _195))
(define-fun _199 () Bool (not _198))
(define-fun _201 () Bool (and _197 _199))
(define-fun _202 () Bool (and _197 _198))
(define-fun _203 () Real |acpi_pcc_init::__retval__@2|)
(define-fun _204 () Bool (= _203 _7))
(define-fun _205 () Bool (and _202 _204))
(define-fun _206 () Real (- 19))
(define-fun _207 () Bool (= _203 _206))
(define-fun _208 () Bool (and _201 _207))
(define-fun _209 () Bool (or _205 _208))
(define-fun _210 () Real |main::tmp@3|)
(define-fun _211 () Bool (= _203 _210))
(define-fun _212 () Bool (and _209 _211))
(define-fun _213 () Bool (= _210 _7))
(define-fun _217 () Bool (and _212 _213))
(define-fun _218 () Real ___pc@4)
(define-fun _219 () Bool (= _218 _14))
(define-fun _220 () Bool (and _217 _219))
(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(push 1)
(assert _220)
(set-info :status sat)
(check-sat)
(pop 1)
(exit)