(set-option :produce-interpolants true)
(set-info :source |printed by MathSAT|)
(declare-fun |main::data@3| () Real)
(declare-fun |main::__cil_tmp9@3| () Real)
(define-fun .def_32 () Bool (= |main::__cil_tmp9@3| |main::data@3|))
(define-fun .def_29 () Bool (= |main::__cil_tmp9@3| (to_real 0)))
(define-fun .def_33 () Bool (and .def_29 .def_32))
(assert (! .def_33 :interpolation-group g1))
(declare-fun |main::node@3| () Real)
(declare-fun |main::__cil_tmp12@3| () Real)
(declare-fun |main::__cil_tmp14@3| () Real)
(declare-fun |main::data@4| () Real)
(declare-fun |main::__cil_tmp10@3| () Real)
(declare-fun |__VERIFIER_successful_alloc_*(void)*@3| () Real)
(declare-fun |main::__cil_tmp15@3| () Real)
(declare-fun |main::tmp@3| () Real)
(declare-fun |main::tmp___0@3| () Real)
(declare-fun |*(struct_node)*@2| (Real) Real)
(declare-fun |main::__cil_tmp11@3| () Real)
(declare-fun |main::item@3| () Real)
(declare-fun |main::data@3| () Real)
(declare-fun |__VERIFIER_successful_alloc_*(void)*@2| () Real)
(declare-fun |main::tmp___1@3| () Real)
(declare-fun |main::__cil_tmp13@3| () Real)
(declare-fun |*(struct_node)*@3| (Real) Real)
(declare-fun |*(struct_list)*@2| (Real) Real)
(define-fun .def_131 () Bool (= |main::item@3| |main::data@4|))
(define-fun .def_127 () Real (|*(struct_list)*@2| |main::__cil_tmp15@3|))
(define-fun .def_128 () Bool (= |main::data@3| .def_127))
(define-fun .def_122 () Real (* (to_real (- 1)) |main::__cil_tmp15@3|))
(define-fun .def_123 () Real (+ |main::__cil_tmp14@3| .def_122))
(define-fun .def_124 () Bool (= .def_123 (to_real (- 4))))
(define-fun .def_117 () Bool (= |main::item@3| |main::__cil_tmp14@3|))
(define-fun .def_113 () Real (|*(struct_node)*@3| |main::item@3|))
(define-fun .def_114 () Bool (= |main::node@3| .def_113))
(define-fun .def_118 () Bool (and .def_114 .def_117))
(define-fun .def_125 () Bool (and .def_118 .def_124))
(define-fun .def_129 () Bool (and .def_125 .def_128))
(define-fun .def_132 () Bool (and .def_129 .def_131))
(define-fun .def_105 () Bool (= |main::item@3| (to_real 0)))
(define-fun .def_106 () Int (ite .def_105 1 0))
(define-fun .def_107 () Bool (= .def_106 0))
(define-fun .def_102 () Bool (= |main::tmp___0@3| |main::item@3|))
(define-fun .def_98 () Bool (= |__VERIFIER_successful_alloc_*(void)*@3| |main::tmp___0@3|))
(define-fun .def_85 () Bool (= |main::__cil_tmp13@3| (to_real 8)))
(define-fun .def_78 () Real (* (to_real (- 1)) |main::__cil_tmp12@3|))
(define-fun .def_79 () Real (+ |main::__cil_tmp11@3| .def_78))
(define-fun .def_80 () Bool (= .def_79 (to_real (- 4))))
(define-fun .def_70 () Bool (= |main::node@3| |main::__cil_tmp11@3|))
(define-fun .def_66 () Real (|*(struct_node)*@2| |main::node@3|))
(define-fun .def_67 () Bool (= |main::node@3| .def_66))
(define-fun .def_71 () Bool (and .def_67 .def_70))
(define-fun .def_81 () Bool (and .def_71 .def_80))
(define-fun .def_86 () Bool (and .def_81 .def_85))
(define-fun .def_99 () Bool (and .def_86 .def_98))
(define-fun .def_103 () Bool (and .def_99 .def_102))
(define-fun .def_57 () Bool (= |main::node@3| (to_real 0)))
(define-fun .def_58 () Int (ite .def_57 1 0))
(define-fun .def_59 () Bool (= .def_58 0))
(define-fun .def_54 () Bool (= |main::tmp@3| |main::node@3|))
(define-fun .def_50 () Bool (= |__VERIFIER_successful_alloc_*(void)*@2| |main::tmp@3|))
(define-fun .def_44 () Bool (= |main::__cil_tmp10@3| (to_real 8)))
(define-fun .def_51 () Bool (and .def_44 .def_50))
(define-fun .def_55 () Bool (and .def_51 .def_54))
(define-fun .def_36 () Bool (= |main::tmp___1@3| (to_real 0)))
(define-fun .def_38 () Int (ite .def_36 1 0))
(define-fun .def_39 () Bool (= .def_38 0))
(define-fun .def_56 () Bool (and .def_39 .def_55))
(define-fun .def_62 () Bool (and .def_56 .def_59))
(define-fun .def_60 () Bool (not .def_59))
(define-fun .def_61 () Bool (and .def_56 .def_60))
(define-fun .def_64 () Bool (or .def_61 .def_62))
(define-fun .def_104 () Bool (and .def_64 .def_103))
(define-fun .def_110 () Bool (and .def_104 .def_107))
(define-fun .def_108 () Bool (not .def_107))
(define-fun .def_109 () Bool (and .def_104 .def_108))
(define-fun .def_111 () Bool (or .def_109 .def_110))
(define-fun .def_133 () Bool (and .def_111 .def_132))
(assert (! .def_133 :interpolation-group g2))
(declare-fun |main::data@4| () Real)
(declare-fun |main::tmp___1@4| () Real)
(declare-fun |inspect_before::shape@2| () Real)
(define-fun .def_745 () Bool (= |main::data@4| |inspect_before::shape@2|))
(define-fun .def_561 () Bool (= |main::tmp___1@4| (to_real 0)))
(define-fun .def_562 () Int (ite .def_561 1 0))
(define-fun .def_563 () Bool (= .def_562 0))
(define-fun .def_564 () Bool (not .def_563))
(define-fun .def_371 () Bool (= |main::data@4| (to_real 0)))
(define-fun .def_372 () Int (ite .def_371 1 0))
(define-fun .def_373 () Bool (= .def_372 0))
(define-fun .def_741 () Bool (and .def_373 .def_564))
(define-fun .def_746 () Bool (and .def_741 .def_745))
(define-fun .def_172 () Bool (= |inspect_before::shape@2| (to_real 0)))
(define-fun .def_173 () Int (ite .def_172 1 0))
(define-fun .def_174 () Bool (= .def_173 0))
(define-fun .def_748 () Bool (and .def_174 .def_746))
(assert (! .def_748 :interpolation-group g3))
(declare-fun |inspect_before::__cil_tmp6@3| () Real)
(declare-fun |inspect_before::__cil_tmp7@3| () Real)
(declare-fun |__VERIFIER_successful_alloc_*(void)*@3| () Real)
(declare-fun |inspect_before::shape@2| () Real)
(declare-fun |inspect_before::__cil_tmp10@3| () Real)
(declare-fun |inspect_before::__cil_tmp12@3| () Real)
(declare-fun |inspect_before::__cil_tmp3@3| () Real)
(declare-fun |inspect_before::__cil_tmp9@3| () Real)
(declare-fun |inspect_before::__cil_tmp2@3| () Real)
(declare-fun |__VERIFIER_successful_alloc_*(void)*@2| () Real)
(declare-fun |inspect_before::__cil_tmp4@3| () Real)
(declare-fun |inspect_before::__cil_tmp13@3| () Real)
(declare-fun |*(struct_node)*@3| (Real) Real)
(declare-fun |*(struct_list)*@2| (Real) Real)
(declare-fun |inspect_before::__cil_tmp8@3| () Real)
(declare-fun |inspect_before::__cil_tmp5@3| () Real)
(declare-fun |inspect_before::__cil_tmp11@3| () Real)
(define-fun .def_970 () Bool (= |inspect_before::__cil_tmp13@3| (to_real 0)))
(define-fun .def_971 () Int (ite .def_970 1 0))
(define-fun .def_972 () Bool (= .def_971 0))
(define-fun .def_973 () Bool (not .def_972))
(define-fun .def_964 () Bool (= |inspect_before::__cil_tmp9@3| |inspect_before::__cil_tmp12@3|))
(define-fun .def_965 () Int (ite .def_964 1 0))
(define-fun .def_967 () Bool (= (to_real .def_965) |inspect_before::__cil_tmp13@3|))
(define-fun .def_962 () Bool (= |inspect_before::__cil_tmp11@3| |inspect_before::__cil_tmp12@3|))
(define-fun .def_955 () Real (|*(struct_node)*@3| |inspect_before::__cil_tmp10@3|))
(define-fun .def_958 () Bool (= .def_955 |inspect_before::__cil_tmp11@3|))
(define-fun .def_817 () Real (|*(struct_node)*@3| |inspect_before::shape@2|))
(define-fun .def_953 () Bool (= .def_817 |inspect_before::__cil_tmp10@3|))
(define-fun .def_949 () Bool (= |inspect_before::__cil_tmp8@3| |inspect_before::__cil_tmp9@3|))
(define-fun .def_946 () Bool (= |inspect_before::__cil_tmp8@3| (to_real 0)))
(define-fun .def_950 () Bool (and .def_946 .def_949))
(define-fun .def_954 () Bool (and .def_950 .def_953))
(define-fun .def_959 () Bool (and .def_954 .def_958))
(define-fun .def_963 () Bool (and .def_959 .def_962))
(define-fun .def_968 () Bool (and .def_963 .def_967))
(define-fun .def_818 () Bool (= |inspect_before::__cil_tmp7@3| .def_817))
(define-fun .def_790 () Real (|*(struct_list)*@2| |inspect_before::__cil_tmp5@3|))
(define-fun .def_791 () Bool (= |inspect_before::__cil_tmp6@3| .def_790))
(define-fun .def_465 () Real (* (to_real (- 1)) |inspect_before::__cil_tmp5@3|))
(define-fun .def_466 () Real (+ |inspect_before::__cil_tmp4@3| .def_465))
(define-fun .def_467 () Bool (= .def_466 (to_real (- 4))))
(define-fun .def_461 () Bool (= |inspect_before::shape@2| |inspect_before::__cil_tmp4@3|))
(define-fun .def_468 () Bool (and .def_461 .def_467))
(define-fun .def_792 () Bool (and .def_468 .def_791))
(define-fun .def_768 () Real (|*(struct_list)*@2| |inspect_before::__cil_tmp3@3|))
(define-fun .def_769 () Bool (= .def_768 (to_real 0)))
(define-fun .def_770 () Int (ite .def_769 1 0))
(define-fun .def_771 () Bool (= .def_770 0))
(define-fun .def_190 () Real (* (to_real (- 1)) |inspect_before::__cil_tmp3@3|))
(define-fun .def_191 () Real (+ |inspect_before::__cil_tmp2@3| .def_190))
(define-fun .def_192 () Bool (= .def_191 (to_real (- 4))))
(define-fun .def_186 () Bool (= |inspect_before::shape@2| |inspect_before::__cil_tmp2@3|))
(define-fun .def_193 () Bool (and .def_186 .def_192))
(define-fun .def_774 () Bool (and .def_193 .def_771))
(define-fun .def_776 () Bool (and .def_174 .def_774))
(define-fun .def_793 () Bool (and .def_776 .def_792))
(define-fun .def_474 () Bool (= |inspect_before::__cil_tmp6@3| (to_real 0)))
(define-fun .def_475 () Int (ite .def_474 1 0))
(define-fun .def_476 () Bool (= .def_475 0))
(define-fun .def_795 () Bool (and .def_476 .def_793))
(define-fun .def_819 () Bool (and .def_795 .def_818))
(define-fun .def_511 () Bool (= |inspect_before::__cil_tmp7@3| (to_real 0)))
(define-fun .def_512 () Int (ite .def_511 1 0))
(define-fun .def_513 () Bool (= .def_512 0))
(define-fun .def_821 () Bool (and .def_513 .def_819))
(define-fun .def_969 () Bool (and .def_821 .def_968))
(define-fun .def_974 () Bool (and .def_969 .def_973))
(define-fun .def_91 () Real (* (to_real (- 1)) |__VERIFIER_successful_alloc_*(void)*@3|))
(define-fun .def_92 () Real (+ |__VERIFIER_successful_alloc_*(void)*@2| .def_91))
(define-fun .def_93 () Bool (<= .def_92 (to_real (- 4))))
(define-fun .def_89 () Bool (<= |__VERIFIER_successful_alloc_*(void)*@2| (to_real (- 4))))
(define-fun .def_90 () Bool (not .def_89))
(define-fun .def_94 () Bool (and .def_90 .def_93))
(define-fun .def_46 () Bool (<= |__VERIFIER_successful_alloc_*(void)*@2| (to_real 0)))
(define-fun .def_47 () Bool (not .def_46))
(define-fun .def_95 () Bool (and .def_47 .def_94))
(define-fun .def_976 () Bool (and .def_95 .def_974))
(assert (! .def_976 :interpolation-group g4))
(check-sat)
(get-interpolant (g1))
(get-interpolant (g1 g2))
(get-interpolant (g1 g2 g3))