(set-option :produce-interpolants true)
(set-info :source |printed by MathSAT|)
(declare-fun |*(struct_dummy)*@1| (Real) Real)
(declare-fun |main::i@3| () Real)
(declare-fun *int@2 (Real) Real)
(declare-fun |main::i@2| () Real)
(declare-fun |*(int)*@1| (Real) Real)
(declare-fun |main::dummies| () Real)
(declare-fun *int@1 (Real) Real)
(declare-fun |main::pa@3| () Real)
(declare-fun |main::cont$array@3| () Real)
(declare-fun |main::a| () Real)
(declare-fun |main::dummy| () Real)
(declare-fun |main::dummy$array@3| () Real)
(declare-fun |*(struct_dummy)*@2| (Real) Real)
(define-fun .def_295 () Real (* (to_real (- 1)) |main::i@3|))
(define-fun .def_70 () Real (* (to_real 4) |main::i@2|))
(define-fun .def_173 () Real (+ |main::dummies| .def_70))
(define-fun .def_174 () Real (+ .def_173 (to_real 4)))
(define-fun .def_176 () Real (|*(struct_dummy)*@2| .def_174))
(define-fun .def_287 () Real (|*(int)*@1| .def_176))
(define-fun .def_289 () Real (+ .def_287 (to_real 4)))
(define-fun .def_290 () Real (*int@2 .def_289))
(define-fun .def_296 () Real (+ .def_290 .def_295))
(define-fun .def_297 () Bool (= .def_296 (to_real 10)))
(define-fun .def_71 () Real (+ |main::a| .def_70))
(define-fun .def_73 () Real (*int@2 .def_71))
(define-fun .def_250 () Bool (<= .def_73 (to_real 0)))
(define-fun .def_251 () Bool (not .def_250))
(define-fun .def_252 () Int (ite .def_251 1 0))
(define-fun .def_253 () Bool (= .def_252 0))
(define-fun .def_254 () Bool (not .def_253))
(define-fun .def_244 () Real (* (to_real (- 1)) |main::pa@3|))
(define-fun .def_236 () Real (+ .def_70 |main::cont$array@3|))
(define-fun .def_237 () Real (|*(struct_dummy)*@2| .def_236))
(define-fun .def_238 () Real (|*(int)*@1| .def_237))
(define-fun .def_245 () Real (+ .def_238 .def_244))
(define-fun .def_246 () Bool (= .def_245 (to_real (- 4))))
(define-fun .def_232 () Real (* (to_real (- 1)) |main::cont$array@3|))
(define-fun .def_233 () Real (+ |main::dummies| .def_232))
(define-fun .def_234 () Bool (= .def_233 (to_real (- 4))))
(define-fun .def_177 () Bool (= |main::dummy| .def_176))
(define-fun .def_156 () Real (* (to_real (- 1)) |main::dummy$array@3|))
(define-fun .def_157 () Real (+ .def_70 .def_156))
(define-fun .def_158 () Real (+ |main::a| .def_157))
(define-fun .def_159 () Bool (= .def_158 (to_real 4)))
(define-fun .def_74 () Bool (= |main::i@2| .def_73))
(define-fun .def_160 () Bool (and .def_74 .def_159))
(define-fun .def_229 () Bool (and .def_160 .def_177))
(define-fun .def_235 () Bool (and .def_229 .def_234))
(define-fun .def_247 () Bool (and .def_235 .def_246))
(define-fun .def_225 () Real (|*(struct_dummy)*@1| |main::dummies|))
(define-fun .def_224 () Real (|*(struct_dummy)*@2| |main::dummies|))
(define-fun .def_226 () Bool (= .def_224 .def_225))
(define-fun .def_223 () Bool (= |main::i@2| (to_real (- 1))))
(define-fun .def_227 () Bool (or .def_223 .def_226))
(define-fun .def_12 () Real (+ |main::dummies| (to_real 4)))
(define-fun .def_219 () Real (|*(struct_dummy)*@1| .def_12))
(define-fun .def_218 () Real (|*(struct_dummy)*@2| .def_12))
(define-fun .def_220 () Bool (= .def_218 .def_219))
(define-fun .def_142 () Bool (= |main::i@2| (to_real 0)))
(define-fun .def_221 () Bool (or .def_142 .def_220))
(define-fun .def_14 () Real (+ |main::dummies| (to_real 8)))
(define-fun .def_214 () Real (|*(struct_dummy)*@1| .def_14))
(define-fun .def_213 () Real (|*(struct_dummy)*@2| .def_14))
(define-fun .def_215 () Bool (= .def_213 .def_214))
(define-fun .def_135 () Bool (= |main::i@2| (to_real 1)))
(define-fun .def_216 () Bool (or .def_135 .def_215))
(define-fun .def_16 () Real (+ |main::dummies| (to_real 12)))
(define-fun .def_209 () Real (|*(struct_dummy)*@1| .def_16))
(define-fun .def_208 () Real (|*(struct_dummy)*@2| .def_16))
(define-fun .def_210 () Bool (= .def_208 .def_209))
(define-fun .def_128 () Bool (= |main::i@2| (to_real 2)))
(define-fun .def_211 () Bool (or .def_128 .def_210))
(define-fun .def_18 () Real (+ |main::dummies| (to_real 16)))
(define-fun .def_204 () Real (|*(struct_dummy)*@1| .def_18))
(define-fun .def_203 () Real (|*(struct_dummy)*@2| .def_18))
(define-fun .def_205 () Bool (= .def_203 .def_204))
(define-fun .def_120 () Bool (= |main::i@2| (to_real 3)))
(define-fun .def_206 () Bool (or .def_120 .def_205))
(define-fun .def_20 () Real (+ |main::dummies| (to_real 20)))
(define-fun .def_199 () Real (|*(struct_dummy)*@1| .def_20))
(define-fun .def_198 () Real (|*(struct_dummy)*@2| .def_20))
(define-fun .def_200 () Bool (= .def_198 .def_199))
(define-fun .def_112 () Bool (= |main::i@2| (to_real 4)))
(define-fun .def_201 () Bool (or .def_112 .def_200))
(define-fun .def_22 () Real (+ |main::dummies| (to_real 24)))
(define-fun .def_194 () Real (|*(struct_dummy)*@1| .def_22))
(define-fun .def_193 () Real (|*(struct_dummy)*@2| .def_22))
(define-fun .def_195 () Bool (= .def_193 .def_194))
(define-fun .def_105 () Bool (= |main::i@2| (to_real 5)))
(define-fun .def_196 () Bool (or .def_105 .def_195))
(define-fun .def_24 () Real (+ |main::dummies| (to_real 28)))
(define-fun .def_189 () Real (|*(struct_dummy)*@1| .def_24))
(define-fun .def_188 () Real (|*(struct_dummy)*@2| .def_24))
(define-fun .def_190 () Bool (= .def_188 .def_189))
(define-fun .def_97 () Bool (= |main::i@2| (to_real 6)))
(define-fun .def_191 () Bool (or .def_97 .def_190))
(define-fun .def_26 () Real (+ |main::dummies| (to_real 32)))
(define-fun .def_184 () Real (|*(struct_dummy)*@1| .def_26))
(define-fun .def_183 () Real (|*(struct_dummy)*@2| .def_26))
(define-fun .def_185 () Bool (= .def_183 .def_184))
(define-fun .def_89 () Bool (= |main::i@2| (to_real 7)))
(define-fun .def_186 () Bool (or .def_89 .def_185))
(define-fun .def_28 () Real (+ |main::dummies| (to_real 36)))
(define-fun .def_179 () Real (|*(struct_dummy)*@1| .def_28))
(define-fun .def_178 () Real (|*(struct_dummy)*@2| .def_28))
(define-fun .def_180 () Bool (= .def_178 .def_179))
(define-fun .def_81 () Bool (= |main::i@2| (to_real 8)))
(define-fun .def_181 () Bool (or .def_81 .def_180))
(define-fun .def_162 () Real (|*(int)*@1| |main::dummy|))
(define-fun .def_163 () Bool (= |main::dummy$array@3| .def_162))
(define-fun .def_144 () Real (*int@1 |main::a|))
(define-fun .def_143 () Real (*int@2 |main::a|))
(define-fun .def_145 () Bool (= .def_143 .def_144))
(define-fun .def_146 () Bool (or .def_142 .def_145))
(define-fun .def_136 () Real (+ |main::a| (to_real 4)))
(define-fun .def_138 () Real (*int@1 .def_136))
(define-fun .def_137 () Real (*int@2 .def_136))
(define-fun .def_139 () Bool (= .def_137 .def_138))
(define-fun .def_140 () Bool (or .def_135 .def_139))
(define-fun .def_129 () Real (+ |main::a| (to_real 8)))
(define-fun .def_131 () Real (*int@1 .def_129))
(define-fun .def_130 () Real (*int@2 .def_129))
(define-fun .def_132 () Bool (= .def_130 .def_131))
(define-fun .def_133 () Bool (or .def_128 .def_132))
(define-fun .def_121 () Real (+ |main::a| (to_real 12)))
(define-fun .def_123 () Real (*int@1 .def_121))
(define-fun .def_122 () Real (*int@2 .def_121))
(define-fun .def_124 () Bool (= .def_122 .def_123))
(define-fun .def_125 () Bool (or .def_120 .def_124))
(define-fun .def_113 () Real (+ |main::a| (to_real 16)))
(define-fun .def_115 () Real (*int@1 .def_113))
(define-fun .def_114 () Real (*int@2 .def_113))
(define-fun .def_116 () Bool (= .def_114 .def_115))
(define-fun .def_117 () Bool (or .def_112 .def_116))
(define-fun .def_106 () Real (+ |main::a| (to_real 20)))
(define-fun .def_108 () Real (*int@1 .def_106))
(define-fun .def_107 () Real (*int@2 .def_106))
(define-fun .def_109 () Bool (= .def_107 .def_108))
(define-fun .def_110 () Bool (or .def_105 .def_109))
(define-fun .def_98 () Real (+ |main::a| (to_real 24)))
(define-fun .def_100 () Real (*int@1 .def_98))
(define-fun .def_99 () Real (*int@2 .def_98))
(define-fun .def_101 () Bool (= .def_99 .def_100))
(define-fun .def_102 () Bool (or .def_97 .def_101))
(define-fun .def_90 () Real (+ |main::a| (to_real 28)))
(define-fun .def_92 () Real (*int@1 .def_90))
(define-fun .def_91 () Real (*int@2 .def_90))
(define-fun .def_93 () Bool (= .def_91 .def_92))
(define-fun .def_94 () Bool (or .def_89 .def_93))
(define-fun .def_82 () Real (+ |main::a| (to_real 32)))
(define-fun .def_84 () Real (*int@1 .def_82))
(define-fun .def_83 () Real (*int@2 .def_82))
(define-fun .def_85 () Bool (= .def_83 .def_84))
(define-fun .def_86 () Bool (or .def_81 .def_85))
(define-fun .def_76 () Real (+ |main::a| (to_real 36)))
(define-fun .def_78 () Real (*int@1 .def_76))
(define-fun .def_77 () Real (*int@2 .def_76))
(define-fun .def_79 () Bool (= .def_77 .def_78))
(define-fun .def_75 () Bool (= |main::i@2| (to_real 9)))
(define-fun .def_80 () Bool (or .def_75 .def_79))
(define-fun .def_87 () Bool (and .def_80 .def_86))
(define-fun .def_95 () Bool (and .def_87 .def_94))
(define-fun .def_103 () Bool (and .def_95 .def_102))
(define-fun .def_111 () Bool (and .def_103 .def_110))
(define-fun .def_118 () Bool (and .def_111 .def_117))
(define-fun .def_126 () Bool (and .def_118 .def_125))
(define-fun .def_134 () Bool (and .def_126 .def_133))
(define-fun .def_141 () Bool (and .def_134 .def_140))
(define-fun .def_147 () Bool (and .def_141 .def_146))
(define-fun .def_164 () Bool (and .def_147 .def_163))
(define-fun .def_182 () Bool (and .def_164 .def_181))
(define-fun .def_187 () Bool (and .def_182 .def_186))
(define-fun .def_192 () Bool (and .def_187 .def_191))
(define-fun .def_197 () Bool (and .def_192 .def_196))
(define-fun .def_202 () Bool (and .def_197 .def_201))
(define-fun .def_207 () Bool (and .def_202 .def_206))
(define-fun .def_212 () Bool (and .def_207 .def_211))
(define-fun .def_217 () Bool (and .def_212 .def_216))
(define-fun .def_222 () Bool (and .def_217 .def_221))
(define-fun .def_228 () Bool (and .def_222 .def_227))
(define-fun .def_248 () Bool (and .def_228 .def_247))
(define-fun .def_62 () Bool (<= (to_real 9) |main::i@2|))
(define-fun .def_63 () Bool (not .def_62))
(define-fun .def_64 () Int (ite .def_63 1 0))
(define-fun .def_65 () Bool (= .def_64 0))
(define-fun .def_66 () Bool (not .def_65))
(define-fun .def_55 () Bool (<= |main::i@2| (to_real 0)))
(define-fun .def_56 () Bool (not .def_55))
(define-fun .def_58 () Int (ite .def_56 1 0))
(define-fun .def_59 () Bool (= .def_58 0))
(define-fun .def_60 () Bool (not .def_59))
(define-fun .def_67 () Bool (and .def_60 .def_66))
(define-fun .def_249 () Bool (and .def_67 .def_248))
(define-fun .def_255 () Bool (and .def_249 .def_254))
(define-fun .def_298 () Bool (and .def_255 .def_297))
(assert (! .def_298 :interpolation-group g1))
(declare-fun *int@2 (Real) Real)
(declare-fun |main::i@4| () Real)
(declare-fun |main::pa@3| () Real)
(declare-fun |main::i@3| () Real)
(define-fun .def_476 () Real (* (to_real (- 1)) |main::i@4|))
(define-fun .def_477 () Real (+ |main::i@3| .def_476))
(define-fun .def_478 () Bool (= .def_477 (to_real (- 1))))
(define-fun .def_299 () Real (*int@2 |main::pa@3|))
(define-fun .def_300 () Bool (<= .def_299 |main::i@3|))
(define-fun .def_301 () Bool (not .def_300))
(define-fun .def_302 () Int (ite .def_301 1 0))
(define-fun .def_303 () Bool (= .def_302 0))
(define-fun .def_304 () Bool (not .def_303))
(define-fun .def_479 () Bool (and .def_304 .def_478))
(assert (! .def_479 :interpolation-group g2))
(declare-fun *int@2 (Real) Real)
(declare-fun |main::i@5| () Real)
(declare-fun |main::i@4| () Real)
(declare-fun |main::pa@3| () Real)
(define-fun .def_571 () Real (* (to_real (- 1)) |main::i@5|))
(define-fun .def_572 () Real (+ |main::i@4| .def_571))
(define-fun .def_573 () Bool (= .def_572 (to_real (- 1))))
(define-fun .def_499 () Bool (<= .def_299 |main::i@4|))
(define-fun .def_500 () Bool (not .def_499))
(define-fun .def_501 () Int (ite .def_500 1 0))
(define-fun .def_502 () Bool (= .def_501 0))
(define-fun .def_503 () Bool (not .def_502))
(define-fun .def_574 () Bool (and .def_503 .def_573))
(assert (! .def_574 :interpolation-group g3))
(declare-fun *int@2 (Real) Real)
(declare-fun |main::i@5| () Real)
(declare-fun |main::i@6| () Real)
(declare-fun |main::pa@3| () Real)
(define-fun .def_699 () Real (* (to_real (- 1)) |main::i@6|))
(define-fun .def_700 () Real (+ |main::i@5| .def_699))
(define-fun .def_701 () Bool (= .def_700 (to_real (- 1))))
(define-fun .def_601 () Bool (<= .def_299 |main::i@5|))
(define-fun .def_602 () Bool (not .def_601))
(define-fun .def_603 () Int (ite .def_602 1 0))
(define-fun .def_604 () Bool (= .def_603 0))
(define-fun .def_605 () Bool (not .def_604))
(define-fun .def_702 () Bool (and .def_605 .def_701))
(assert (! .def_702 :interpolation-group g4))
(declare-fun *int@2 (Real) Real)
(declare-fun |main::i@6| () Real)
(declare-fun |main::i@7| () Real)
(declare-fun |main::pa@3| () Real)
(define-fun .def_867 () Real (* (to_real (- 1)) |main::i@7|))
(define-fun .def_868 () Real (+ |main::i@6| .def_867))
(define-fun .def_869 () Bool (= .def_868 (to_real (- 1))))
(define-fun .def_739 () Bool (<= .def_299 |main::i@6|))
(define-fun .def_740 () Bool (not .def_739))
(define-fun .def_741 () Int (ite .def_740 1 0))
(define-fun .def_742 () Bool (= .def_741 0))
(define-fun .def_743 () Bool (not .def_742))
(define-fun .def_870 () Bool (and .def_743 .def_869))
(assert (! .def_870 :interpolation-group g5))
(declare-fun |main::i@8| () Real)
(declare-fun *int@2 (Real) Real)
(declare-fun |main::i@7| () Real)
(declare-fun |main::pa@3| () Real)
(define-fun .def_1083 () Real (* (to_real (- 1)) |main::i@8|))
(define-fun .def_1084 () Real (+ |main::i@7| .def_1083))
(define-fun .def_1085 () Bool (= .def_1084 (to_real (- 1))))
(define-fun .def_918 () Bool (<= .def_299 |main::i@7|))
(define-fun .def_919 () Bool (not .def_918))
(define-fun .def_920 () Int (ite .def_919 1 0))
(define-fun .def_921 () Bool (= .def_920 0))
(define-fun .def_922 () Bool (not .def_921))
(define-fun .def_1086 () Bool (and .def_922 .def_1085))
(assert (! .def_1086 :interpolation-group g6))
(declare-fun |main::i@8| () Real)
(declare-fun |main::i@9| () Real)
(declare-fun *int@2 (Real) Real)
(declare-fun |main::pa@3| () Real)
(define-fun .def_1354 () Real (* (to_real (- 1)) |main::i@9|))
(define-fun .def_1355 () Real (+ |main::i@8| .def_1354))
(define-fun .def_1356 () Bool (= .def_1355 (to_real (- 1))))
(define-fun .def_1145 () Bool (<= .def_299 |main::i@8|))
(define-fun .def_1146 () Bool (not .def_1145))
(define-fun .def_1147 () Int (ite .def_1146 1 0))
(define-fun .def_1148 () Bool (= .def_1147 0))
(define-fun .def_1149 () Bool (not .def_1148))
(define-fun .def_1357 () Bool (and .def_1149 .def_1356))
(assert (! .def_1357 :interpolation-group g7))
(declare-fun |main::i@9| () Real)
(declare-fun *int@2 (Real) Real)
(declare-fun |main::i@10| () Real)
(declare-fun |main::pa@3| () Real)
(define-fun .def_1686 () Real (* (to_real (- 1)) |main::i@10|))
(define-fun .def_1687 () Real (+ |main::i@9| .def_1686))
(define-fun .def_1688 () Bool (= .def_1687 (to_real (- 1))))
(define-fun .def_1427 () Bool (<= .def_299 |main::i@9|))
(define-fun .def_1428 () Bool (not .def_1427))
(define-fun .def_1429 () Int (ite .def_1428 1 0))
(define-fun .def_1430 () Bool (= .def_1429 0))
(define-fun .def_1431 () Bool (not .def_1430))
(define-fun .def_1689 () Bool (and .def_1431 .def_1688))
(assert (! .def_1689 :interpolation-group g8))
(declare-fun *int@2 (Real) Real)
(declare-fun |main::i@10| () Real)
(declare-fun |main::pa@3| () Real)
(declare-fun |main::i@11| () Real)
(define-fun .def_2088 () Real (* (to_real (- 1)) |main::i@11|))
(define-fun .def_2089 () Real (+ |main::i@10| .def_2088))
(define-fun .def_2090 () Bool (= .def_2089 (to_real (- 1))))
(define-fun .def_1770 () Bool (<= .def_299 |main::i@10|))
(define-fun .def_1771 () Bool (not .def_1770))
(define-fun .def_1772 () Int (ite .def_1771 1 0))
(define-fun .def_1773 () Bool (= .def_1772 0))
(define-fun .def_1774 () Bool (not .def_1773))
(define-fun .def_2091 () Bool (and .def_1774 .def_2090))
(assert (! .def_2091 :interpolation-group g9))
(declare-fun *int@2 (Real) Real)
(declare-fun |main::pa@3| () Real)
(declare-fun |main::i@12| () Real)
(declare-fun |main::i@11| () Real)
(define-fun .def_2566 () Real (* (to_real (- 1)) |main::i@12|))
(define-fun .def_2567 () Real (+ |main::i@11| .def_2566))
(define-fun .def_2568 () Bool (= .def_2567 (to_real (- 1))))
(define-fun .def_2183 () Bool (<= .def_299 |main::i@11|))
(define-fun .def_2184 () Bool (not .def_2183))
(define-fun .def_2185 () Int (ite .def_2184 1 0))
(define-fun .def_2186 () Bool (= .def_2185 0))
(define-fun .def_2187 () Bool (not .def_2186))
(define-fun .def_2569 () Bool (and .def_2187 .def_2568))
(assert (! .def_2569 :interpolation-group g10))
(declare-fun *int@2 (Real) Real)
(declare-fun |main::i@13| () Real)
(declare-fun |main::pa@3| () Real)
(declare-fun |main::i@12| () Real)
(define-fun .def_3126 () Real (* (to_real (- 1)) |main::i@13|))
(define-fun .def_3127 () Real (+ |main::i@12| .def_3126))
(define-fun .def_3128 () Bool (= .def_3127 (to_real (- 1))))
(define-fun .def_2672 () Bool (<= .def_299 |main::i@12|))
(define-fun .def_2673 () Bool (not .def_2672))
(define-fun .def_2674 () Int (ite .def_2673 1 0))
(define-fun .def_2675 () Bool (= .def_2674 0))
(define-fun .def_2676 () Bool (not .def_2675))
(define-fun .def_3129 () Bool (and .def_2676 .def_3128))
(assert (! .def_3129 :interpolation-group g11))
(declare-fun |main::i@13| () Real)
(declare-fun *int@2 (Real) Real)
(declare-fun |check::pc@2| () Real)
(declare-fun |*(int)*@1| (Real) Real)
(declare-fun |main::dummies| () Real)
(declare-fun |main::cont| () Real)
(declare-fun |check::i@2| () Real)
(declare-fun |main::pa@3| () Real)
(declare-fun |*((struct_dummy)*)*@1| (Real) Real)
(declare-fun |main::cont$array@3| () Real)
(declare-fun |main::a| () Real)
(declare-fun |main::__CPAchecker_TMP_0@3| () Real)
(declare-fun |main::dummy| () Real)
(declare-fun |*(struct_dummy)*@2| (Real) Real)
(declare-fun |check::__retval__@2| () Real)
(define-fun .def_3248 () Bool (= |check::i@2| |main::i@13|))
(define-fun .def_319 () Bool (= |main::cont| |check::pc@2|))
(define-fun .def_3249 () Bool (and .def_319 .def_3248))
(define-fun .def_307 () Real (|*((struct_dummy)*)*@1| |main::cont|))
(define-fun .def_308 () Bool (= |main::cont$array@3| .def_307))
(define-fun .def_3250 () Bool (and .def_308 .def_3249))
(define-fun .def_3243 () Bool (<= .def_299 |main::i@13|))
(define-fun .def_3244 () Bool (not .def_3243))
(define-fun .def_3245 () Int (ite .def_3244 1 0))
(define-fun .def_3246 () Bool (= .def_3245 0))
(define-fun .def_3251 () Bool (and .def_3246 .def_3250))
(define-fun .def_326 () Real (|*((struct_dummy)*)*@1| |check::pc@2|))
(define-fun .def_327 () Real (* (to_real 4) |check::i@2|))
(define-fun .def_329 () Real (+ .def_327 .def_326))
(define-fun .def_330 () Real (|*(struct_dummy)*@2| .def_329))
(define-fun .def_331 () Real (|*(int)*@1| .def_330))
(define-fun .def_333 () Real (+ .def_331 (to_real 4)))
(define-fun .def_334 () Real (*int@2 .def_333))
(define-fun .def_335 () Bool (= |check::i@2| .def_334))
(define-fun .def_336 () Int (ite .def_335 1 0))
(define-fun .def_339 () Bool (= (to_real .def_336) |check::__retval__@2|))
(define-fun .def_3252 () Bool (and .def_339 .def_3251))
(define-fun .def_343 () Bool (= |check::__retval__@2| |main::__CPAchecker_TMP_0@3|))
(define-fun .def_3253 () Bool (and .def_343 .def_3252))
(define-fun .def_345 () Bool (= |main::__CPAchecker_TMP_0@3| (to_real 0)))
(define-fun .def_346 () Int (ite .def_345 1 0))
(define-fun .def_347 () Bool (= .def_346 0))
(define-fun .def_348 () Bool (not .def_347))
(define-fun .def_3254 () Bool (and .def_348 .def_3253))
(define-fun .def_312 () Real (* (to_real (- 1)) |main::cont|))
(define-fun .def_313 () Real (+ |main::dummy| .def_312))
(define-fun .def_314 () Bool (<= .def_313 (to_real (- 4))))
(define-fun .def_310 () Bool (<= |main::dummy| (to_real (- 4))))
(define-fun .def_311 () Bool (not .def_310))
(define-fun .def_315 () Bool (and .def_311 .def_314))
(define-fun .def_165 () Real (* (to_real (- 1)) |main::dummy|))
(define-fun .def_166 () Real (+ |main::dummies| .def_165))
(define-fun .def_167 () Bool (<= .def_166 (to_real (- 40))))
(define-fun .def_44 () Bool (<= |main::dummies| (to_real (- 40))))
(define-fun .def_45 () Bool (not .def_44))
(define-fun .def_168 () Bool (and .def_45 .def_167))
(define-fun .def_47 () Real (* (to_real (- 1)) |main::a|))
(define-fun .def_48 () Real (+ |main::dummies| .def_47))
(define-fun .def_49 () Bool (<= .def_48 (to_real (- 40))))
(define-fun .def_50 () Bool (and .def_45 .def_49))
(define-fun .def_29 () Bool (<= |main::dummies| (to_real 0)))
(define-fun .def_30 () Bool (not .def_29))
(define-fun .def_51 () Bool (and .def_30 .def_50))
(define-fun .def_169 () Bool (and .def_51 .def_168))
(define-fun .def_316 () Bool (and .def_169 .def_315))
(define-fun .def_3257 () Bool (and .def_316 .def_3254))
(assert (! .def_3257 :interpolation-group g12))
(check-sat)
(get-interpolant (g1))
(get-interpolant (g1 g2))