(set-option :produce-interpolants true)
(set-info :source |printed by MathSAT|)
(declare-fun |main::i@2| () (_ BitVec 32))
(declare-fun |main::cont$array@3| () (_ BitVec 32))
(declare-fun |main::pa@3| () (_ BitVec 32))
(declare-fun |main::array| () (_ BitVec 32))
(declare-fun |main::i@3| () (_ BitVec 32))
(declare-fun *int@1 ((_ BitVec 32)) (_ BitVec 32))
(define-fun .def_120 () (_ BitVec 32) (bvshl |main::i@2| (_ bv3 32)))
(define-fun .def_121 () (_ BitVec 32) (bvadd |main::array| .def_120))
(define-fun .def_147 () (_ BitVec 32) (bvadd (_ bv4 32) .def_121))
(define-fun .def_148 () (_ BitVec 32) (*int@1 .def_147))
(define-fun .def_152 () (_ BitVec 32) (bvadd (_ bv4294967286 32) .def_148))
(define-fun .def_154 () Bool (= .def_152 |main::i@3|))
(define-fun .def_128 () (_ BitVec 32) (bvadd (_ bv4 32) |main::cont$array@3|))
(define-fun .def_129 () (_ BitVec 32) (*int@1 .def_128))
(define-fun .def_135 () Bool (bvslt (_ bv0 32) .def_129))
(define-fun .def_136 () (_ BitVec 32) (ite .def_135 (_ bv1 32) (_ bv0 32)))
(define-fun .def_137 () Bool (= .def_136 (_ bv0 32)))
(define-fun .def_138 () Bool (not .def_137))
(define-fun .def_132 () Bool (= .def_128 |main::pa@3|))
(define-fun .def_124 () Bool (= .def_121 |main::cont$array@3|))
(define-fun .def_133 () Bool (and .def_124 .def_132))
(define-fun .def_111 () Bool (bvslt |main::i@2| (_ bv10 32)))
(define-fun .def_112 () (_ BitVec 32) (ite .def_111 (_ bv1 32) (_ bv0 32)))
(define-fun .def_113 () Bool (= .def_112 (_ bv0 32)))
(define-fun .def_114 () Bool (not .def_113))
(define-fun .def_103 () (_ BitVec 1) ((_ extract 31 31) |main::i@2|))
(define-fun .def_104 () Bool (= .def_103 (_ bv1 1)))
(define-fun .def_105 () Bool (not .def_104))
(define-fun .def_107 () (_ BitVec 32) (ite .def_105 (_ bv1 32) (_ bv0 32)))
(define-fun .def_108 () Bool (= .def_107 (_ bv0 32)))
(define-fun .def_109 () Bool (not .def_108))
(define-fun .def_115 () Bool (and .def_109 .def_114))
(define-fun .def_134 () Bool (and .def_115 .def_133))
(define-fun .def_139 () Bool (and .def_134 .def_138))
(define-fun .def_155 () Bool (and .def_139 .def_154))
(assert (! .def_155 :interpolation-group g1))
(declare-fun |main::i@4| () (_ BitVec 32))
(declare-fun |main::pa@3| () (_ BitVec 32))
(declare-fun |main::i@3| () (_ BitVec 32))
(declare-fun *int@1 ((_ BitVec 32)) (_ BitVec 32))
(define-fun .def_314 () (_ BitVec 32) (bvadd (_ bv1 32) |main::i@3|))
(define-fun .def_316 () Bool (= .def_314 |main::i@4|))
(define-fun .def_156 () (_ BitVec 32) (*int@1 |main::pa@3|))
(define-fun .def_157 () Bool (bvslt |main::i@3| .def_156))
(define-fun .def_158 () (_ BitVec 32) (ite .def_157 (_ bv1 32) (_ bv0 32)))
(define-fun .def_159 () Bool (= .def_158 (_ bv0 32)))
(define-fun .def_160 () Bool (not .def_159))
(define-fun .def_317 () Bool (and .def_160 .def_316))
(assert (! .def_317 :interpolation-group g2))
(declare-fun |main::i@5| () (_ BitVec 32))
(declare-fun |main::i@4| () (_ BitVec 32))
(declare-fun |main::pa@3| () (_ BitVec 32))
(declare-fun *int@1 ((_ BitVec 32)) (_ BitVec 32))
(define-fun .def_407 () (_ BitVec 32) (bvadd (_ bv1 32) |main::i@4|))
(define-fun .def_428 () Bool (= .def_407 |main::i@5|))
(define-fun .def_320 () Bool (bvslt |main::i@4| .def_156))
(define-fun .def_337 () (_ BitVec 32) (ite .def_320 (_ bv1 32) (_ bv0 32)))
(define-fun .def_338 () Bool (= .def_337 (_ bv0 32)))
(define-fun .def_339 () Bool (not .def_338))
(define-fun .def_429 () Bool (and .def_339 .def_428))
(assert (! .def_429 :interpolation-group g3))
(declare-fun |main::i@5| () (_ BitVec 32))
(declare-fun |main::i@6| () (_ BitVec 32))
(declare-fun |main::pa@3| () (_ BitVec 32))
(declare-fun *int@1 ((_ BitVec 32)) (_ BitVec 32))
(define-fun .def_433 () (_ BitVec 32) (bvadd (_ bv1 32) |main::i@5|))
(define-fun .def_576 () Bool (= .def_433 |main::i@6|))
(define-fun .def_432 () Bool (bvslt |main::i@5| .def_156))
(define-fun .def_456 () (_ BitVec 32) (ite .def_432 (_ bv1 32) (_ bv0 32)))
(define-fun .def_457 () Bool (= .def_456 (_ bv0 32)))
(define-fun .def_458 () Bool (not .def_457))
(define-fun .def_577 () Bool (and .def_458 .def_576))
(assert (! .def_577 :interpolation-group g4))
(declare-fun |main::i@7| () (_ BitVec 32))
(declare-fun |main::i@6| () (_ BitVec 32))
(declare-fun |main::pa@3| () (_ BitVec 32))
(declare-fun *int@1 ((_ BitVec 32)) (_ BitVec 32))
(define-fun .def_581 () (_ BitVec 32) (bvadd (_ bv1 32) |main::i@6|))
(define-fun .def_816 () Bool (= .def_581 |main::i@7|))
(define-fun .def_580 () Bool (bvslt |main::i@6| .def_156))
(define-fun .def_627 () (_ BitVec 32) (ite .def_580 (_ bv1 32) (_ bv0 32)))
(define-fun .def_628 () Bool (= .def_627 (_ bv0 32)))
(define-fun .def_629 () Bool (not .def_628))
(define-fun .def_817 () Bool (and .def_629 .def_816))
(assert (! .def_817 :interpolation-group g5))
(declare-fun |main::i@7| () (_ BitVec 32))
(declare-fun |main::i@8| () (_ BitVec 32))
(declare-fun |main::pa@3| () (_ BitVec 32))
(declare-fun *int@1 ((_ BitVec 32)) (_ BitVec 32))
(define-fun .def_821 () (_ BitVec 32) (bvadd (_ bv1 32) |main::i@7|))
(define-fun .def_1144 () Bool (= .def_821 |main::i@8|))
(define-fun .def_820 () Bool (bvslt |main::i@7| .def_156))
(define-fun .def_884 () (_ BitVec 32) (ite .def_820 (_ bv1 32) (_ bv0 32)))
(define-fun .def_885 () Bool (= .def_884 (_ bv0 32)))
(define-fun .def_886 () Bool (not .def_885))
(define-fun .def_1145 () Bool (and .def_886 .def_1144))
(assert (! .def_1145 :interpolation-group g6))
(declare-fun |main::i@8| () (_ BitVec 32))
(declare-fun |main::pa@3| () (_ BitVec 32))
(declare-fun *int@1 ((_ BitVec 32)) (_ BitVec 32))
(declare-fun |main::i@9| () (_ BitVec 32))
(define-fun .def_1149 () (_ BitVec 32) (bvadd (_ bv1 32) |main::i@8|))
(define-fun .def_1586 () Bool (= .def_1149 |main::i@9|))
(define-fun .def_1148 () Bool (bvslt |main::i@8| .def_156))
(define-fun .def_1234 () (_ BitVec 32) (ite .def_1148 (_ bv1 32) (_ bv0 32)))
(define-fun .def_1235 () Bool (= .def_1234 (_ bv0 32)))
(define-fun .def_1236 () Bool (not .def_1235))
(define-fun .def_1587 () Bool (and .def_1236 .def_1586))
(assert (! .def_1587 :interpolation-group g7))
(declare-fun |main::pa@3| () (_ BitVec 32))
(declare-fun |main::i@10| () (_ BitVec 32))
(declare-fun *int@1 ((_ BitVec 32)) (_ BitVec 32))
(declare-fun |main::i@9| () (_ BitVec 32))
(define-fun .def_1591 () (_ BitVec 32) (bvadd (_ bv1 32) |main::i@9|))
(define-fun .def_2163 () Bool (= .def_1591 |main::i@10|))
(define-fun .def_1590 () Bool (bvslt |main::i@9| .def_156))
(define-fun .def_1697 () (_ BitVec 32) (ite .def_1590 (_ bv1 32) (_ bv0 32)))
(define-fun .def_1698 () Bool (= .def_1697 (_ bv0 32)))
(define-fun .def_1699 () Bool (not .def_1698))
(define-fun .def_2164 () Bool (and .def_1699 .def_2163))
(assert (! .def_2164 :interpolation-group g8))
(declare-fun |main::pa@3| () (_ BitVec 32))
(declare-fun |main::i@11| () (_ BitVec 32))
(declare-fun |main::i@10| () (_ BitVec 32))
(declare-fun *int@1 ((_ BitVec 32)) (_ BitVec 32))
(define-fun .def_2168 () (_ BitVec 32) (bvadd (_ bv1 32) |main::i@10|))
(define-fun .def_2910 () Bool (= .def_2168 |main::i@11|))
(define-fun .def_2167 () Bool (bvslt |main::i@10| .def_156))
(define-fun .def_2295 () (_ BitVec 32) (ite .def_2167 (_ bv1 32) (_ bv0 32)))
(define-fun .def_2296 () Bool (= .def_2295 (_ bv0 32)))
(define-fun .def_2297 () Bool (not .def_2296))
(define-fun .def_2911 () Bool (and .def_2297 .def_2910))
(assert (! .def_2911 :interpolation-group g9))
(declare-fun |main::i@12| () (_ BitVec 32))
(declare-fun |main::pa@3| () (_ BitVec 32))
(declare-fun |main::i@11| () (_ BitVec 32))
(declare-fun *int@1 ((_ BitVec 32)) (_ BitVec 32))
(define-fun .def_2915 () (_ BitVec 32) (bvadd (_ bv1 32) |main::i@11|))
(define-fun .def_3830 () Bool (= .def_2915 |main::i@12|))
(define-fun .def_2914 () Bool (bvslt |main::i@11| .def_156))
(define-fun .def_3063 () (_ BitVec 32) (ite .def_2914 (_ bv1 32) (_ bv0 32)))
(define-fun .def_3064 () Bool (= .def_3063 (_ bv0 32)))
(define-fun .def_3065 () Bool (not .def_3064))
(define-fun .def_3831 () Bool (and .def_3065 .def_3830))
(assert (! .def_3831 :interpolation-group g10))
(declare-fun |main::i@12| () (_ BitVec 32))
(declare-fun |main::i@13| () (_ BitVec 32))
(declare-fun |main::pa@3| () (_ BitVec 32))
(declare-fun *int@1 ((_ BitVec 32)) (_ BitVec 32))
(define-fun .def_3835 () (_ BitVec 32) (bvadd (_ bv1 32) |main::i@12|))
(define-fun .def_4964 () Bool (= .def_3835 |main::i@13|))
(define-fun .def_3834 () Bool (bvslt |main::i@12| .def_156))
(define-fun .def_4004 () (_ BitVec 32) (ite .def_3834 (_ bv1 32) (_ bv0 32)))
(define-fun .def_4005 () Bool (= .def_4004 (_ bv0 32)))
(define-fun .def_4006 () Bool (not .def_4005))
(define-fun .def_4965 () Bool (and .def_4006 .def_4964))
(assert (! .def_4965 :interpolation-group g11))
(declare-fun |check::__retval__@2| () (_ BitVec 32))
(declare-fun |main::i@13| () (_ BitVec 32))
(declare-fun |main::__CPAchecker_TMP_0@3| () (_ BitVec 32))
(declare-fun |*(struct_dummy)*@1| ((_ BitVec 32)) (_ BitVec 32))
(declare-fun |main::cont$array@3| () (_ BitVec 32))
(declare-fun |main::pa@3| () (_ BitVec 32))
(declare-fun |main::array| () (_ BitVec 32))
(declare-fun |main::cont| () (_ BitVec 32))
(declare-fun |check::pc@2| () (_ BitVec 32))
(declare-fun *int@1 ((_ BitVec 32)) (_ BitVec 32))
(declare-fun |check::i@2| () (_ BitVec 32))
(define-fun .def_5162 () Bool (= |check::i@2| |main::i@13|))
(define-fun .def_178 () Bool (= |main::cont| |check::pc@2|))
(define-fun .def_5163 () Bool (and .def_178 .def_5162))
(define-fun .def_165 () (_ BitVec 32) (|*(struct_dummy)*@1| |main::cont|))
(define-fun .def_166 () Bool (= |main::cont$array@3| .def_165))
(define-fun .def_5164 () Bool (and .def_166 .def_5163))
(define-fun .def_4968 () Bool (bvslt |main::i@13| .def_156))
(define-fun .def_5159 () (_ BitVec 32) (ite .def_4968 (_ bv1 32) (_ bv0 32)))
(define-fun .def_5160 () Bool (= .def_5159 (_ bv0 32)))
(define-fun .def_5165 () Bool (and .def_5160 .def_5164))
(define-fun .def_187 () (_ BitVec 32) (|*(struct_dummy)*@1| |check::pc@2|))
(define-fun .def_191 () (_ BitVec 32) (bvadd (_ bv4 32) .def_187))
(define-fun .def_192 () (_ BitVec 32) (*int@1 .def_191))
(define-fun .def_193 () Bool (= |check::i@2| .def_192))
(define-fun .def_194 () (_ BitVec 32) (ite .def_193 (_ bv1 32) (_ bv0 32)))
(define-fun .def_197 () Bool (= .def_194 |check::__retval__@2|))
(define-fun .def_5166 () Bool (and .def_197 .def_5165))
(define-fun .def_201 () Bool (= |check::__retval__@2| |main::__CPAchecker_TMP_0@3|))
(define-fun .def_5167 () Bool (and .def_201 .def_5166))
(define-fun .def_203 () Bool (= |main::__CPAchecker_TMP_0@3| (_ bv0 32)))
(define-fun .def_204 () (_ BitVec 32) (ite .def_203 (_ bv1 32) (_ bv0 32)))
(define-fun .def_205 () Bool (= .def_204 (_ bv0 32)))
(define-fun .def_206 () Bool (not .def_205))
(define-fun .def_5168 () Bool (and .def_206 .def_5167))
(define-fun .def_169 () (_ BitVec 32) (bvadd (_ bv80 32) |main::array|))
(define-fun .def_172 () Bool (bvslt |main::cont| .def_169))
(define-fun .def_173 () Bool (not .def_172))
(define-fun .def_170 () Bool (bvslt (_ bv0 32) .def_169))
(define-fun .def_174 () Bool (and .def_170 .def_173))
(define-fun .def_96 () Bool (bvslt (_ bv0 32) |main::array|))
(define-fun .def_175 () Bool (and .def_96 .def_174))
(define-fun .def_5171 () Bool (and .def_175 .def_5168))
(assert (! .def_5171 :interpolation-group g12))
(check-sat)
(get-interpolant (g1 g2 g3 g4 g5 g6))