(set-option :produce-interpolants true)
(set-info :source |printed by MathSAT|)
(declare-fun |main::i@2| () Real)
(declare-fun *int@2 (Real) Real)
(declare-fun |main::i@3| () Real)
(declare-fun |main::pa@3| () Real)
(declare-fun |main::ad1| () Real)
(declare-fun |main::ad2@3| () Real)
(define-fun .def_81 () Real (* (to_real (- 1)) |main::i@3|))
(define-fun .def_61 () Real (* (to_real 8) |main::i@2|))
(define-fun .def_76 () Real (+ .def_61 |main::ad2@3|))
(define-fun .def_77 () Real (*int@2 .def_76))
(define-fun .def_82 () Real (+ .def_77 .def_81))
(define-fun .def_83 () Bool (= .def_82 (to_real 10)))
(define-fun .def_70 () Real (* (to_real (- 1)) |main::pa@3|))
(define-fun .def_71 () Real (+ .def_61 .def_70))
(define-fun .def_72 () Real (+ |main::ad1| .def_71))
(define-fun .def_73 () Bool (= .def_72 (to_real 0)))
(define-fun .def_62 () Real (+ |main::ad1| .def_61))
(define-fun .def_64 () Real (*int@2 .def_62))
(define-fun .def_65 () Bool (= |main::i@2| .def_64))
(define-fun .def_60 () Bool (= |main::ad1| |main::ad2@3|))
(define-fun .def_66 () Bool (and .def_60 .def_65))
(define-fun .def_74 () Bool (and .def_66 .def_73))
(define-fun .def_84 () Bool (and .def_74 .def_83))
(define-fun .def_50 () Bool (<= (to_real 10) |main::i@2|))
(define-fun .def_51 () Bool (not .def_50))
(define-fun .def_52 () Int (ite .def_51 1 0))
(define-fun .def_53 () Bool (= .def_52 0))
(define-fun .def_54 () Bool (not .def_53))
(define-fun .def_44 () Bool (<= (to_real 0) |main::i@2|))
(define-fun .def_46 () Int (ite .def_44 1 0))
(define-fun .def_47 () Bool (= .def_46 0))
(define-fun .def_48 () Bool (not .def_47))
(define-fun .def_55 () Bool (and .def_48 .def_54))
(define-fun .def_85 () Bool (and .def_55 .def_84))
(assert (! .def_85 :interpolation-group g1))
(declare-fun *int@2 (Real) Real)
(declare-fun |main::i@3| () Real)
(declare-fun |main::pa@3| () Real)
(declare-fun |main::i@4| () Real)
(define-fun .def_216 () Real (* (to_real (- 1)) |main::i@4|))
(define-fun .def_217 () Real (+ |main::i@3| .def_216))
(define-fun .def_218 () Bool (= .def_217 (to_real (- 1))))
(define-fun .def_86 () Real (*int@2 |main::pa@3|))
(define-fun .def_87 () Bool (<= .def_86 |main::i@3|))
(define-fun .def_88 () Bool (not .def_87))
(define-fun .def_89 () Int (ite .def_88 1 0))
(define-fun .def_90 () Bool (= .def_89 0))
(define-fun .def_91 () Bool (not .def_90))
(define-fun .def_219 () Bool (and .def_91 .def_218))
(assert (! .def_219 :interpolation-group g2))
(declare-fun |main::i@5| () Real)
(declare-fun *int@2 (Real) Real)
(declare-fun |main::pa@3| () Real)
(declare-fun |main::i@4| () Real)
(define-fun .def_308 () Real (* (to_real (- 1)) |main::i@5|))
(define-fun .def_309 () Real (+ |main::i@4| .def_308))
(define-fun .def_310 () Bool (= .def_309 (to_real (- 1))))
(define-fun .def_239 () Bool (<= .def_86 |main::i@4|))
(define-fun .def_240 () Bool (not .def_239))
(define-fun .def_241 () Int (ite .def_240 1 0))
(define-fun .def_242 () Bool (= .def_241 0))
(define-fun .def_243 () Bool (not .def_242))
(define-fun .def_311 () Bool (and .def_243 .def_310))
(assert (! .def_311 :interpolation-group g3))
(declare-fun |main::i@5| () Real)
(declare-fun *int@2 (Real) Real)
(declare-fun |main::pa@3| () Real)
(declare-fun |main::i@6| () Real)
(define-fun .def_431 () Real (* (to_real (- 1)) |main::i@6|))
(define-fun .def_432 () Real (+ |main::i@5| .def_431))
(define-fun .def_433 () Bool (= .def_432 (to_real (- 1))))
(define-fun .def_338 () Bool (<= .def_86 |main::i@5|))
(define-fun .def_339 () Bool (not .def_338))
(define-fun .def_340 () Int (ite .def_339 1 0))
(define-fun .def_341 () Bool (= .def_340 0))
(define-fun .def_342 () Bool (not .def_341))
(define-fun .def_434 () Bool (and .def_342 .def_433))
(assert (! .def_434 :interpolation-group g4))
(declare-fun |main::i@7| () Real)
(declare-fun *int@2 (Real) Real)
(declare-fun |main::pa@3| () Real)
(declare-fun |main::i@6| () Real)
(define-fun .def_596 () Real (* (to_real (- 1)) |main::i@7|))
(define-fun .def_597 () Real (+ |main::i@6| .def_596))
(define-fun .def_598 () Bool (= .def_597 (to_real (- 1))))
(define-fun .def_471 () Bool (<= .def_86 |main::i@6|))
(define-fun .def_472 () Bool (not .def_471))
(define-fun .def_473 () Int (ite .def_472 1 0))
(define-fun .def_474 () Bool (= .def_473 0))
(define-fun .def_475 () Bool (not .def_474))
(define-fun .def_599 () Bool (and .def_475 .def_598))
(assert (! .def_599 :interpolation-group g5))
(declare-fun |main::i@7| () Real)
(declare-fun |main::i@8| () Real)
(declare-fun *int@2 (Real) Real)
(declare-fun |main::pa@3| () Real)
(define-fun .def_809 () Real (* (to_real (- 1)) |main::i@8|))
(define-fun .def_810 () Real (+ |main::i@7| .def_809))
(define-fun .def_811 () Bool (= .def_810 (to_real (- 1))))
(define-fun .def_647 () Bool (<= .def_86 |main::i@7|))
(define-fun .def_648 () Bool (not .def_647))
(define-fun .def_649 () Int (ite .def_648 1 0))
(define-fun .def_650 () Bool (= .def_649 0))
(define-fun .def_651 () Bool (not .def_650))
(define-fun .def_812 () Bool (and .def_651 .def_811))
(assert (! .def_812 :interpolation-group g6))
(declare-fun |main::i@8| () Real)
(declare-fun *int@2 (Real) Real)
(declare-fun |main::i@9| () Real)
(declare-fun |main::pa@3| () Real)
(define-fun .def_1077 () Real (* (to_real (- 1)) |main::i@9|))
(define-fun .def_1078 () Real (+ |main::i@8| .def_1077))
(define-fun .def_1079 () Bool (= .def_1078 (to_real (- 1))))
(define-fun .def_871 () Bool (<= .def_86 |main::i@8|))
(define-fun .def_872 () Bool (not .def_871))
(define-fun .def_873 () Int (ite .def_872 1 0))
(define-fun .def_874 () Bool (= .def_873 0))
(define-fun .def_875 () Bool (not .def_874))
(define-fun .def_1080 () Bool (and .def_875 .def_1079))
(assert (! .def_1080 :interpolation-group g7))
(declare-fun |main::i@10| () Real)
(declare-fun *int@2 (Real) Real)
(declare-fun |main::i@9| () Real)
(declare-fun |main::pa@3| () Real)
(define-fun .def_1406 () Real (* (to_real (- 1)) |main::i@10|))
(define-fun .def_1407 () Real (+ |main::i@9| .def_1406))
(define-fun .def_1408 () Bool (= .def_1407 (to_real (- 1))))
(define-fun .def_1150 () Bool (<= .def_86 |main::i@9|))
(define-fun .def_1151 () Bool (not .def_1150))
(define-fun .def_1152 () Int (ite .def_1151 1 0))
(define-fun .def_1153 () Bool (= .def_1152 0))
(define-fun .def_1154 () Bool (not .def_1153))
(define-fun .def_1409 () Bool (and .def_1154 .def_1408))
(assert (! .def_1409 :interpolation-group g8))
(declare-fun |main::i@10| () Real)
(declare-fun |main::i@11| () Real)
(declare-fun *int@2 (Real) Real)
(declare-fun |main::pa@3| () Real)
(define-fun .def_1805 () Real (* (to_real (- 1)) |main::i@11|))
(define-fun .def_1806 () Real (+ |main::i@10| .def_1805))
(define-fun .def_1807 () Bool (= .def_1806 (to_real (- 1))))
(define-fun .def_1490 () Bool (<= .def_86 |main::i@10|))
(define-fun .def_1491 () Bool (not .def_1490))
(define-fun .def_1492 () Int (ite .def_1491 1 0))
(define-fun .def_1493 () Bool (= .def_1492 0))
(define-fun .def_1494 () Bool (not .def_1493))
(define-fun .def_1808 () Bool (and .def_1494 .def_1807))
(assert (! .def_1808 :interpolation-group g9))
(declare-fun |main::i@11| () Real)
(declare-fun *int@2 (Real) Real)
(declare-fun |main::pa@3| () Real)
(declare-fun |main::i@12| () Real)
(define-fun .def_2280 () Real (* (to_real (- 1)) |main::i@12|))
(define-fun .def_2281 () Real (+ |main::i@11| .def_2280))
(define-fun .def_2282 () Bool (= .def_2281 (to_real (- 1))))
(define-fun .def_1900 () Bool (<= .def_86 |main::i@11|))
(define-fun .def_1901 () Bool (not .def_1900))
(define-fun .def_1902 () Int (ite .def_1901 1 0))
(define-fun .def_1903 () Bool (= .def_1902 0))
(define-fun .def_1904 () Bool (not .def_1903))
(define-fun .def_2283 () Bool (and .def_1904 .def_2282))
(assert (! .def_2283 :interpolation-group g10))
(declare-fun |main::i@13| () Real)
(declare-fun *int@2 (Real) Real)
(declare-fun |main::pa@3| () Real)
(declare-fun |main::i@12| () Real)
(define-fun .def_2836 () Real (* (to_real (- 1)) |main::i@13|))
(define-fun .def_2837 () Real (+ |main::i@12| .def_2836))
(define-fun .def_2838 () Bool (= .def_2837 (to_real (- 1))))
(define-fun .def_2386 () Bool (<= .def_86 |main::i@12|))
(define-fun .def_2387 () Bool (not .def_2386))
(define-fun .def_2388 () Int (ite .def_2387 1 0))
(define-fun .def_2389 () Bool (= .def_2388 0))
(define-fun .def_2390 () Bool (not .def_2389))
(define-fun .def_2839 () Bool (and .def_2390 .def_2838))
(assert (! .def_2839 :interpolation-group g11))
(declare-fun |check::__retval__@2| () Real)
(declare-fun |main::i@13| () Real)
(declare-fun |check::ad1@2| () Real)
(declare-fun *int@2 (Real) Real)
(declare-fun |check::b@2| () Real)
(declare-fun |main::pa@3| () Real)
(declare-fun |main::__CPAchecker_TMP_0@3| () Real)
(declare-fun |main::ad1| () Real)
(define-fun .def_2958 () Bool (= |check::b@2| |main::i@13|))
(define-fun .def_95 () Bool (= |main::ad1| |check::ad1@2|))
(define-fun .def_2959 () Bool (and .def_95 .def_2958))
(define-fun .def_2953 () Bool (<= .def_86 |main::i@13|))
(define-fun .def_2954 () Bool (not .def_2953))
(define-fun .def_2955 () Int (ite .def_2954 1 0))
(define-fun .def_2956 () Bool (= .def_2955 0))
(define-fun .def_2960 () Bool (and .def_2956 .def_2959))
(define-fun .def_101 () Real (* (to_real 8) |check::b@2|))
(define-fun .def_102 () Real (+ |check::ad1@2| .def_101))
(define-fun .def_103 () Real (*int@2 .def_102))
(define-fun .def_104 () Bool (= |check::b@2| .def_103))
(define-fun .def_105 () Int (ite .def_104 1 0))
(define-fun .def_108 () Bool (= (to_real .def_105) |check::__retval__@2|))
(define-fun .def_2961 () Bool (and .def_108 .def_2960))
(define-fun .def_112 () Bool (= |check::__retval__@2| |main::__CPAchecker_TMP_0@3|))
(define-fun .def_2962 () Bool (and .def_112 .def_2961))
(define-fun .def_114 () Bool (= |main::__CPAchecker_TMP_0@3| (to_real 0)))
(define-fun .def_115 () Int (ite .def_114 1 0))
(define-fun .def_116 () Bool (= .def_115 0))
(define-fun .def_117 () Bool (not .def_116))
(define-fun .def_2963 () Bool (and .def_117 .def_2962))
(define-fun .def_38 () Bool (<= |main::ad1| (to_real 0)))
(define-fun .def_39 () Bool (not .def_38))
(define-fun .def_2966 () Bool (and .def_39 .def_2963))
(assert (! .def_2966 :interpolation-group g12))
(check-sat)
(get-interpolant (g1))
(get-interpolant (g1 g2))