(set-option :produce-interpolants true)
(set-info :source |printed by MathSAT|)
(declare-fun |main::i@2| () (_ BitVec 32))
(declare-fun |main::pd1@3| () (_ BitVec 32))
(declare-fun |get_dummy::__CPAchecker_TMP_0@5| () (_ BitVec 32))
(declare-fun *int@2 ((_ BitVec 32)) (_ BitVec 32))
(declare-fun |get_dummy::__retval__@3| () (_ BitVec 32))
(declare-fun |get_dummy::__retval__@2| () (_ BitVec 32))
(declare-fun |main::pa@3| () (_ BitVec 32))
(declare-fun |main::i@3| () (_ BitVec 32))
(declare-fun |main::pd2@3| () (_ BitVec 32))
(declare-fun |get_dummy::__CPAchecker_TMP_0@3| () (_ BitVec 32))
(define-fun .def_73 () (_ BitVec 32) (bvshl |main::i@2| (_ bv2 32)))
(define-fun .def_75 () (_ BitVec 32) (bvadd |main::pd2@3| .def_73))
(define-fun .def_76 () (_ BitVec 32) (bvadd (_ bv8 32) .def_75))
(define-fun .def_78 () (_ BitVec 32) (*int@2 .def_76))
(define-fun .def_94 () (_ BitVec 32) (bvadd (_ bv4294967286 32) .def_78))
(define-fun .def_96 () Bool (= .def_94 |main::i@3|))
(define-fun .def_84 () (_ BitVec 32) (bvadd |main::pd1@3| .def_73))
(define-fun .def_85 () (_ BitVec 32) (bvadd (_ bv8 32) .def_84))
(define-fun .def_89 () Bool (= .def_85 |main::pa@3|))
(define-fun .def_79 () Bool (= |main::i@2| .def_78))
(define-fun .def_90 () Bool (and .def_79 .def_89))
(define-fun .def_97 () Bool (and .def_90 .def_96))
(define-fun .def_60 () Bool (bvslt |main::i@2| (_ bv10 32)))
(define-fun .def_61 () (_ BitVec 32) (ite .def_60 (_ bv1 32) (_ bv0 32)))
(define-fun .def_62 () Bool (= .def_61 (_ bv0 32)))
(define-fun .def_63 () Bool (not .def_62))
(define-fun .def_50 () (_ BitVec 1) ((_ extract 31 31) |main::i@2|))
(define-fun .def_51 () Bool (= .def_50 (_ bv1 1)))
(define-fun .def_52 () Bool (not .def_51))
(define-fun .def_53 () (_ BitVec 32) (ite .def_52 (_ bv1 32) (_ bv0 32)))
(define-fun .def_54 () Bool (= .def_53 (_ bv0 32)))
(define-fun .def_55 () Bool (not .def_54))
(define-fun .def_39 () Bool (= |main::pd1@3| |main::pd2@3|))
(define-fun .def_40 () (_ BitVec 32) (ite .def_39 (_ bv1 32) (_ bv0 32)))
(define-fun .def_41 () Bool (= .def_40 (_ bv0 32)))
(define-fun .def_42 () Bool (not .def_41))
(define-fun .def_31 () Bool (= |main::pd1@3| (_ bv0 32)))
(define-fun .def_32 () Bool (not .def_31))
(define-fun .def_34 () (_ BitVec 32) (ite .def_32 (_ bv1 32) (_ bv0 32)))
(define-fun .def_35 () Bool (= .def_34 (_ bv0 32)))
(define-fun .def_36 () Bool (not .def_35))
(define-fun .def_26 () Bool (= |get_dummy::__retval__@3| |main::pd2@3|))
(define-fun .def_22 () Bool (= |get_dummy::__CPAchecker_TMP_0@5| |get_dummy::__retval__@3|))
(define-fun .def_17 () Bool (= |get_dummy::__retval__@2| |main::pd1@3|))
(define-fun .def_14 () Bool (= |get_dummy::__CPAchecker_TMP_0@3| |get_dummy::__retval__@2|))
(define-fun .def_18 () Bool (and .def_14 .def_17))
(define-fun .def_23 () Bool (and .def_18 .def_22))
(define-fun .def_27 () Bool (and .def_23 .def_26))
(define-fun .def_37 () Bool (and .def_27 .def_36))
(define-fun .def_43 () Bool (and .def_37 .def_42))
(define-fun .def_56 () Bool (and .def_43 .def_55))
(define-fun .def_64 () Bool (and .def_56 .def_63))
(define-fun .def_98 () Bool (and .def_64 .def_97))
(assert (! .def_98 :interpolation-group g1))
(declare-fun *int@2 ((_ BitVec 32)) (_ BitVec 32))
(declare-fun |main::i@4| () (_ BitVec 32))
(declare-fun |main::pa@3| () (_ BitVec 32))
(declare-fun |main::i@3| () (_ BitVec 32))
(define-fun .def_206 () (_ BitVec 32) (bvadd (_ bv1 32) |main::i@3|))
(define-fun .def_208 () Bool (= .def_206 |main::i@4|))
(define-fun .def_99 () (_ BitVec 32) (*int@2 |main::pa@3|))
(define-fun .def_100 () Bool (bvslt |main::i@3| .def_99))
(define-fun .def_101 () (_ BitVec 32) (ite .def_100 (_ bv1 32) (_ bv0 32)))
(define-fun .def_102 () Bool (= .def_101 (_ bv0 32)))
(define-fun .def_103 () Bool (not .def_102))
(define-fun .def_209 () Bool (and .def_103 .def_208))
(assert (! .def_209 :interpolation-group g2))
(declare-fun |main::i@5| () (_ BitVec 32))
(declare-fun *int@2 ((_ BitVec 32)) (_ BitVec 32))
(declare-fun |main::i@4| () (_ BitVec 32))
(declare-fun |main::pa@3| () (_ BitVec 32))
(define-fun .def_275 () (_ BitVec 32) (bvadd (_ bv1 32) |main::i@4|))
(define-fun .def_293 () Bool (= .def_275 |main::i@5|))
(define-fun .def_211 () Bool (bvslt |main::i@4| .def_99))
(define-fun .def_219 () (_ BitVec 32) (ite .def_211 (_ bv1 32) (_ bv0 32)))
(define-fun .def_220 () Bool (= .def_219 (_ bv0 32)))
(define-fun .def_221 () Bool (not .def_220))
(define-fun .def_294 () Bool (and .def_221 .def_293))
(assert (! .def_294 :interpolation-group g3))
(declare-fun |main::i@5| () (_ BitVec 32))
(declare-fun *int@2 ((_ BitVec 32)) (_ BitVec 32))
(declare-fun |main::pa@3| () (_ BitVec 32))
(declare-fun |main::i@6| () (_ BitVec 32))
(define-fun .def_297 () (_ BitVec 32) (bvadd (_ bv1 32) |main::i@5|))
(define-fun .def_406 () Bool (= .def_297 |main::i@6|))
(define-fun .def_296 () Bool (bvslt |main::i@5| .def_99))
(define-fun .def_309 () (_ BitVec 32) (ite .def_296 (_ bv1 32) (_ bv0 32)))
(define-fun .def_310 () Bool (= .def_309 (_ bv0 32)))
(define-fun .def_311 () Bool (not .def_310))
(define-fun .def_407 () Bool (and .def_311 .def_406))
(assert (! .def_407 :interpolation-group g4))
(declare-fun *int@2 ((_ BitVec 32)) (_ BitVec 32))
(declare-fun |main::i@7| () (_ BitVec 32))
(declare-fun |main::pa@3| () (_ BitVec 32))
(declare-fun |main::i@6| () (_ BitVec 32))
(define-fun .def_410 () (_ BitVec 32) (bvadd (_ bv1 32) |main::i@6|))
(define-fun .def_568 () Bool (= .def_410 |main::i@7|))
(define-fun .def_409 () Bool (bvslt |main::i@6| .def_99))
(define-fun .def_434 () (_ BitVec 32) (ite .def_409 (_ bv1 32) (_ bv0 32)))
(define-fun .def_435 () Bool (= .def_434 (_ bv0 32)))
(define-fun .def_436 () Bool (not .def_435))
(define-fun .def_569 () Bool (and .def_436 .def_568))
(assert (! .def_569 :interpolation-group g5))
(declare-fun *int@2 ((_ BitVec 32)) (_ BitVec 32))
(declare-fun |main::i@7| () (_ BitVec 32))
(declare-fun |main::i@8| () (_ BitVec 32))
(declare-fun |main::pa@3| () (_ BitVec 32))
(define-fun .def_572 () (_ BitVec 32) (bvadd (_ bv1 32) |main::i@7|))
(define-fun .def_787 () Bool (= .def_572 |main::i@8|))
(define-fun .def_571 () Bool (bvslt |main::i@7| .def_99))
(define-fun .def_614 () (_ BitVec 32) (ite .def_571 (_ bv1 32) (_ bv0 32)))
(define-fun .def_615 () Bool (= .def_614 (_ bv0 32)))
(define-fun .def_616 () Bool (not .def_615))
(define-fun .def_788 () Bool (and .def_616 .def_787))
(assert (! .def_788 :interpolation-group g6))
(declare-fun |main::i@9| () (_ BitVec 32))
(declare-fun *int@2 ((_ BitVec 32)) (_ BitVec 32))
(declare-fun |main::i@8| () (_ BitVec 32))
(declare-fun |main::pa@3| () (_ BitVec 32))
(define-fun .def_791 () (_ BitVec 32) (bvadd (_ bv1 32) |main::i@8|))
(define-fun .def_1069 () Bool (= .def_791 |main::i@9|))
(define-fun .def_790 () Bool (bvslt |main::i@8| .def_99))
(define-fun .def_845 () (_ BitVec 32) (ite .def_790 (_ bv1 32) (_ bv0 32)))
(define-fun .def_846 () Bool (= .def_845 (_ bv0 32)))
(define-fun .def_847 () Bool (not .def_846))
(define-fun .def_1070 () Bool (and .def_847 .def_1069))
(assert (! .def_1070 :interpolation-group g7))
(declare-fun |main::i@10| () (_ BitVec 32))
(declare-fun |main::i@9| () (_ BitVec 32))
(declare-fun *int@2 ((_ BitVec 32)) (_ BitVec 32))
(declare-fun |main::pa@3| () (_ BitVec 32))
(define-fun .def_1073 () (_ BitVec 32) (bvadd (_ bv1 32) |main::i@9|))
(define-fun .def_1424 () Bool (= .def_1073 |main::i@10|))
(define-fun .def_1072 () Bool (bvslt |main::i@9| .def_99))
(define-fun .def_1140 () (_ BitVec 32) (ite .def_1072 (_ bv1 32) (_ bv0 32)))
(define-fun .def_1141 () Bool (= .def_1140 (_ bv0 32)))
(define-fun .def_1142 () Bool (not .def_1141))
(define-fun .def_1425 () Bool (and .def_1142 .def_1424))
(assert (! .def_1425 :interpolation-group g8))
(declare-fun |main::i@11| () (_ BitVec 32))
(declare-fun |main::i@10| () (_ BitVec 32))
(declare-fun *int@2 ((_ BitVec 32)) (_ BitVec 32))
(declare-fun |main::pa@3| () (_ BitVec 32))
(define-fun .def_1428 () (_ BitVec 32) (bvadd (_ bv1 32) |main::i@10|))
(define-fun .def_1848 () Bool (= .def_1428 |main::i@11|))
(define-fun .def_1427 () Bool (bvslt |main::i@10| .def_99))
(define-fun .def_1508 () (_ BitVec 32) (ite .def_1427 (_ bv1 32) (_ bv0 32)))
(define-fun .def_1509 () Bool (= .def_1508 (_ bv0 32)))
(define-fun .def_1510 () Bool (not .def_1509))
(define-fun .def_1849 () Bool (and .def_1510 .def_1848))
(assert (! .def_1849 :interpolation-group g9))
(declare-fun |main::i@11| () (_ BitVec 32))
(declare-fun *int@2 ((_ BitVec 32)) (_ BitVec 32))
(declare-fun |main::pa@3| () (_ BitVec 32))
(declare-fun |main::i@12| () (_ BitVec 32))
(define-fun .def_1852 () (_ BitVec 32) (bvadd (_ bv1 32) |main::i@11|))
(define-fun .def_2360 () Bool (= .def_1852 |main::i@12|))
(define-fun .def_1851 () Bool (bvslt |main::i@11| .def_99))
(define-fun .def_1945 () (_ BitVec 32) (ite .def_1851 (_ bv1 32) (_ bv0 32)))
(define-fun .def_1946 () Bool (= .def_1945 (_ bv0 32)))
(define-fun .def_1947 () Bool (not .def_1946))
(define-fun .def_2361 () Bool (and .def_1947 .def_2360))
(assert (! .def_2361 :interpolation-group g10))
(declare-fun *int@2 ((_ BitVec 32)) (_ BitVec 32))
(declare-fun |main::i@13| () (_ BitVec 32))
(declare-fun |main::pa@3| () (_ BitVec 32))
(declare-fun |main::i@12| () (_ BitVec 32))
(define-fun .def_2364 () (_ BitVec 32) (bvadd (_ bv1 32) |main::i@12|))
(define-fun .def_2965 () Bool (= .def_2364 |main::i@13|))
(define-fun .def_2363 () Bool (bvslt |main::i@12| .def_99))
(define-fun .def_2470 () (_ BitVec 32) (ite .def_2363 (_ bv1 32) (_ bv0 32)))
(define-fun .def_2471 () Bool (= .def_2470 (_ bv0 32)))
(define-fun .def_2472 () Bool (not .def_2471))
(define-fun .def_2966 () Bool (and .def_2472 .def_2965))
(assert (! .def_2966 :interpolation-group g11))
(declare-fun |main::__CPAchecker_TMP_0@3| () (_ BitVec 32))
(declare-fun |check::s1@2| () (_ BitVec 32))
(declare-fun |check::__retval__@2| () (_ BitVec 32))
(declare-fun *int@2 ((_ BitVec 32)) (_ BitVec 32))
(declare-fun |main::i@13| () (_ BitVec 32))
(declare-fun |main::pd2@3| () (_ BitVec 32))
(declare-fun |main::pa@3| () (_ BitVec 32))
(declare-fun |check::i@2| () (_ BitVec 32))
(define-fun .def_3091 () Bool (= |check::i@2| |main::i@13|))
(define-fun .def_107 () Bool (= |main::pd2@3| |check::s1@2|))
(define-fun .def_3092 () Bool (and .def_107 .def_3091))
(define-fun .def_2968 () Bool (bvslt |main::i@13| .def_99))
(define-fun .def_3088 () (_ BitVec 32) (ite .def_2968 (_ bv1 32) (_ bv0 32)))
(define-fun .def_3089 () Bool (= .def_3088 (_ bv0 32)))
(define-fun .def_3093 () Bool (and .def_3089 .def_3092))
(define-fun .def_116 () (_ BitVec 32) (bvshl |check::i@2| (_ bv2 32)))
(define-fun .def_118 () (_ BitVec 32) (bvadd |check::s1@2| .def_116))
(define-fun .def_119 () (_ BitVec 32) (bvadd (_ bv8 32) .def_118))
(define-fun .def_120 () (_ BitVec 32) (*int@2 .def_119))
(define-fun .def_121 () Bool (= |check::i@2| .def_120))
(define-fun .def_122 () (_ BitVec 32) (ite .def_121 (_ bv1 32) (_ bv0 32)))
(define-fun .def_125 () Bool (= .def_122 |check::__retval__@2|))
(define-fun .def_3094 () Bool (and .def_125 .def_3093))
(define-fun .def_129 () Bool (= |check::__retval__@2| |main::__CPAchecker_TMP_0@3|))
(define-fun .def_3095 () Bool (and .def_129 .def_3094))
(define-fun .def_131 () Bool (= |main::__CPAchecker_TMP_0@3| (_ bv0 32)))
(define-fun .def_132 () (_ BitVec 32) (ite .def_131 (_ bv1 32) (_ bv0 32)))
(define-fun .def_133 () Bool (= .def_132 (_ bv0 32)))
(define-fun .def_134 () Bool (not .def_133))
(define-fun .def_3096 () Bool (and .def_134 .def_3095))
(assert (! .def_3096 :interpolation-group g12))
(check-sat)
(get-interpolant (g1))