(set-option :produce-interpolants true)
(set-info :source |printed by MathSAT|)
(declare-fun |main::__cil_tmp9@3| () Real)
(declare-fun |main::data@3| () Real)
(define-fun .def_33 () Bool (= |main::__cil_tmp9@3| |main::data@3|))
(define-fun .def_30 () Bool (= |main::__cil_tmp9@3| (to_real 0)))
(define-fun .def_34 () Bool (and .def_30 .def_33))
(assert (! .def_34 :interpolation-group g1))
(declare-fun |main::__cil_tmp12@3| () Real)
(declare-fun |__VERIFIER_successful_alloc_*(void)*@2| () Real)
(declare-fun |main::data@3| () Real)
(declare-fun |main::tmp___1@3| () Real)
(declare-fun |main::__cil_tmp10@3| () Real)
(declare-fun |main::__cil_tmp16@3| () Real)
(declare-fun |main::__cil_tmp11@3| () Real)
(declare-fun |main::tmp___0@3| () Real)
(declare-fun |main::__cil_tmp13@3| () Real)
(declare-fun |main::tmp@3| () Real)
(declare-fun |main::__cil_tmp15@3| () Real)
(declare-fun |*(struct_list)*@2| (Real) Real)
(declare-fun |main::item@3| () Real)
(declare-fun |main::node@3| () Real)
(declare-fun |__VERIFIER_successful_alloc_*(void)*@3| () Real)
(declare-fun |*(struct_node)*@3| (Real) Real)
(declare-fun |main::data@4| () Real)
(declare-fun |*(struct_node)*@2| (Real) Real)
(declare-fun |main::__cil_tmp14@3| () Real)
(define-fun .def_136 () Bool (= |main::item@3| |main::data@4|))
(define-fun .def_132 () Real (|*(struct_list)*@2| |main::__cil_tmp16@3|))
(define-fun .def_133 () Bool (= |main::data@3| .def_132))
(define-fun .def_127 () Real (* (to_real (- 1)) |main::__cil_tmp16@3|))
(define-fun .def_128 () Real (+ |main::__cil_tmp15@3| .def_127))
(define-fun .def_129 () Bool (= .def_128 (to_real (- 4))))
(define-fun .def_122 () Bool (= |main::item@3| |main::__cil_tmp15@3|))
(define-fun .def_118 () Real (|*(struct_node)*@3| |main::item@3|))
(define-fun .def_119 () Bool (= |main::node@3| .def_118))
(define-fun .def_123 () Bool (and .def_119 .def_122))
(define-fun .def_130 () Bool (and .def_123 .def_129))
(define-fun .def_134 () Bool (and .def_130 .def_133))
(define-fun .def_137 () Bool (and .def_134 .def_136))
(define-fun .def_110 () Bool (= |main::item@3| (to_real 0)))
(define-fun .def_111 () Int (ite .def_110 1 0))
(define-fun .def_112 () Bool (= .def_111 0))
(define-fun .def_107 () Bool (= |main::tmp___0@3| |main::item@3|))
(define-fun .def_103 () Bool (= |__VERIFIER_successful_alloc_*(void)*@3| |main::tmp___0@3|))
(define-fun .def_90 () Bool (= |main::__cil_tmp14@3| (to_real 8)))
(define-fun .def_83 () Real (* (to_real (- 1)) |main::__cil_tmp13@3|))
(define-fun .def_84 () Real (+ |main::__cil_tmp12@3| .def_83))
(define-fun .def_85 () Bool (= .def_84 (to_real (- 4))))
(define-fun .def_75 () Bool (= |main::node@3| |main::__cil_tmp12@3|))
(define-fun .def_70 () Real (|*(struct_node)*@2| |main::node@3|))
(define-fun .def_71 () Bool (= |main::__cil_tmp11@3| .def_70))
(define-fun .def_68 () Bool (= |main::__cil_tmp11@3| (to_real 0)))
(define-fun .def_72 () Bool (and .def_68 .def_71))
(define-fun .def_76 () Bool (and .def_72 .def_75))
(define-fun .def_86 () Bool (and .def_76 .def_85))
(define-fun .def_91 () Bool (and .def_86 .def_90))
(define-fun .def_104 () Bool (and .def_91 .def_103))
(define-fun .def_108 () Bool (and .def_104 .def_107))
(define-fun .def_58 () Bool (= |main::node@3| (to_real 0)))
(define-fun .def_59 () Int (ite .def_58 1 0))
(define-fun .def_60 () Bool (= .def_59 0))
(define-fun .def_55 () Bool (= |main::tmp@3| |main::node@3|))
(define-fun .def_51 () Bool (= |__VERIFIER_successful_alloc_*(void)*@2| |main::tmp@3|))
(define-fun .def_45 () Bool (= |main::__cil_tmp10@3| (to_real 8)))
(define-fun .def_52 () Bool (and .def_45 .def_51))
(define-fun .def_56 () Bool (and .def_52 .def_55))
(define-fun .def_37 () Bool (= |main::tmp___1@3| (to_real 0)))
(define-fun .def_39 () Int (ite .def_37 1 0))
(define-fun .def_40 () Bool (= .def_39 0))
(define-fun .def_57 () Bool (and .def_40 .def_56))
(define-fun .def_63 () Bool (and .def_57 .def_60))
(define-fun .def_61 () Bool (not .def_60))
(define-fun .def_62 () Bool (and .def_57 .def_61))
(define-fun .def_65 () Bool (or .def_62 .def_63))
(define-fun .def_109 () Bool (and .def_65 .def_108))
(define-fun .def_115 () Bool (and .def_109 .def_112))
(define-fun .def_113 () Bool (not .def_112))
(define-fun .def_114 () Bool (and .def_109 .def_113))
(define-fun .def_116 () Bool (or .def_114 .def_115))
(define-fun .def_138 () Bool (and .def_116 .def_137))
(assert (! .def_138 :interpolation-group g2))
(declare-fun |main::data@4| () Real)
(declare-fun |inspect_before::shape@2| () Real)
(declare-fun |main::tmp___1@4| () Real)
(define-fun .def_757 () Bool (= |main::data@4| |inspect_before::shape@2|))
(define-fun .def_568 () Bool (= |main::tmp___1@4| (to_real 0)))
(define-fun .def_569 () Int (ite .def_568 1 0))
(define-fun .def_570 () Bool (= .def_569 0))
(define-fun .def_571 () Bool (not .def_570))
(define-fun .def_377 () Bool (= |main::data@4| (to_real 0)))
(define-fun .def_378 () Int (ite .def_377 1 0))
(define-fun .def_379 () Bool (= .def_378 0))
(define-fun .def_753 () Bool (and .def_379 .def_571))
(define-fun .def_758 () Bool (and .def_753 .def_757))
(define-fun .def_177 () Bool (= |inspect_before::shape@2| (to_real 0)))
(define-fun .def_178 () Int (ite .def_177 1 0))
(define-fun .def_179 () Bool (= .def_178 0))
(define-fun .def_760 () Bool (and .def_179 .def_758))
(assert (! .def_760 :interpolation-group g3))
(declare-fun |inspect_before::__cil_tmp10@3| () Real)
(declare-fun |inspect_before::__cil_tmp12@3| () Real)
(declare-fun |inspect_before::__cil_tmp5@3| () Real)
(declare-fun |__VERIFIER_successful_alloc_*(void)*@2| () Real)
(declare-fun |inspect_before::__cil_tmp3@3| () Real)
(declare-fun |inspect_before::__cil_tmp8@3| () Real)
(declare-fun |inspect_before::__cil_tmp13@3| () Real)
(declare-fun |inspect_before::__cil_tmp2@3| () Real)
(declare-fun |*(struct_list)*@2| (Real) Real)
(declare-fun |__VERIFIER_successful_alloc_*(void)*@3| () Real)
(declare-fun |inspect_before::__cil_tmp4@3| () Real)
(declare-fun |*(struct_node)*@3| (Real) Real)
(declare-fun |inspect_before::__cil_tmp11@3| () Real)
(declare-fun |inspect_before::shape@2| () Real)
(declare-fun |inspect_before::__cil_tmp9@3| () Real)
(declare-fun |inspect_before::__cil_tmp7@3| () Real)
(declare-fun |inspect_before::__cil_tmp6@3| () Real)
(define-fun .def_982 () Bool (= |inspect_before::__cil_tmp13@3| (to_real 0)))
(define-fun .def_983 () Int (ite .def_982 1 0))
(define-fun .def_984 () Bool (= .def_983 0))
(define-fun .def_985 () Bool (not .def_984))
(define-fun .def_976 () Bool (= |inspect_before::__cil_tmp9@3| |inspect_before::__cil_tmp12@3|))
(define-fun .def_977 () Int (ite .def_976 1 0))
(define-fun .def_979 () Bool (= (to_real .def_977) |inspect_before::__cil_tmp13@3|))
(define-fun .def_974 () Bool (= |inspect_before::__cil_tmp11@3| |inspect_before::__cil_tmp12@3|))
(define-fun .def_967 () Real (|*(struct_node)*@3| |inspect_before::__cil_tmp10@3|))
(define-fun .def_970 () Bool (= .def_967 |inspect_before::__cil_tmp11@3|))
(define-fun .def_829 () Real (|*(struct_node)*@3| |inspect_before::shape@2|))
(define-fun .def_965 () Bool (= .def_829 |inspect_before::__cil_tmp10@3|))
(define-fun .def_961 () Bool (= |inspect_before::__cil_tmp8@3| |inspect_before::__cil_tmp9@3|))
(define-fun .def_958 () Bool (= |inspect_before::__cil_tmp8@3| (to_real 0)))
(define-fun .def_962 () Bool (and .def_958 .def_961))
(define-fun .def_966 () Bool (and .def_962 .def_965))
(define-fun .def_971 () Bool (and .def_966 .def_970))
(define-fun .def_975 () Bool (and .def_971 .def_974))
(define-fun .def_980 () Bool (and .def_975 .def_979))
(define-fun .def_830 () Bool (= |inspect_before::__cil_tmp7@3| .def_829))
(define-fun .def_802 () Real (|*(struct_list)*@2| |inspect_before::__cil_tmp5@3|))
(define-fun .def_803 () Bool (= |inspect_before::__cil_tmp6@3| .def_802))
(define-fun .def_472 () Real (* (to_real (- 1)) |inspect_before::__cil_tmp5@3|))
(define-fun .def_473 () Real (+ |inspect_before::__cil_tmp4@3| .def_472))
(define-fun .def_474 () Bool (= .def_473 (to_real (- 4))))
(define-fun .def_468 () Bool (= |inspect_before::shape@2| |inspect_before::__cil_tmp4@3|))
(define-fun .def_475 () Bool (and .def_468 .def_474))
(define-fun .def_804 () Bool (and .def_475 .def_803))
(define-fun .def_780 () Real (|*(struct_list)*@2| |inspect_before::__cil_tmp3@3|))
(define-fun .def_781 () Bool (= .def_780 (to_real 0)))
(define-fun .def_782 () Int (ite .def_781 1 0))
(define-fun .def_783 () Bool (= .def_782 0))
(define-fun .def_195 () Real (* (to_real (- 1)) |inspect_before::__cil_tmp3@3|))
(define-fun .def_196 () Real (+ |inspect_before::__cil_tmp2@3| .def_195))
(define-fun .def_197 () Bool (= .def_196 (to_real (- 4))))
(define-fun .def_191 () Bool (= |inspect_before::shape@2| |inspect_before::__cil_tmp2@3|))
(define-fun .def_198 () Bool (and .def_191 .def_197))
(define-fun .def_786 () Bool (and .def_198 .def_783))
(define-fun .def_788 () Bool (and .def_179 .def_786))
(define-fun .def_805 () Bool (and .def_788 .def_804))
(define-fun .def_481 () Bool (= |inspect_before::__cil_tmp6@3| (to_real 0)))
(define-fun .def_482 () Int (ite .def_481 1 0))
(define-fun .def_483 () Bool (= .def_482 0))
(define-fun .def_807 () Bool (and .def_483 .def_805))
(define-fun .def_831 () Bool (and .def_807 .def_830))
(define-fun .def_518 () Bool (= |inspect_before::__cil_tmp7@3| (to_real 0)))
(define-fun .def_519 () Int (ite .def_518 1 0))
(define-fun .def_520 () Bool (= .def_519 0))
(define-fun .def_833 () Bool (and .def_520 .def_831))
(define-fun .def_981 () Bool (and .def_833 .def_980))
(define-fun .def_986 () Bool (and .def_981 .def_985))
(define-fun .def_96 () Real (* (to_real (- 1)) |__VERIFIER_successful_alloc_*(void)*@3|))
(define-fun .def_97 () Real (+ |__VERIFIER_successful_alloc_*(void)*@2| .def_96))
(define-fun .def_98 () Bool (<= .def_97 (to_real (- 4))))
(define-fun .def_94 () Bool (<= |__VERIFIER_successful_alloc_*(void)*@2| (to_real (- 4))))
(define-fun .def_95 () Bool (not .def_94))
(define-fun .def_99 () Bool (and .def_95 .def_98))
(define-fun .def_47 () Bool (<= |__VERIFIER_successful_alloc_*(void)*@2| (to_real 0)))
(define-fun .def_48 () Bool (not .def_47))
(define-fun .def_100 () Bool (and .def_48 .def_99))
(define-fun .def_988 () Bool (and .def_100 .def_986))
(assert (! .def_988 :interpolation-group g4))
(check-sat)
(get-interpolant (g1))
(get-interpolant (g1 g2))
(get-interpolant (g1 g2 g3))