source: vis_dev/cusp-1.1/examples/BinarySearch_live_blmc000/BinarySearch_live_blmc000.smt @ 12

(benchmark BinarySearch_live_blmc000.smt
  :source {The Averest Framework (http://www.averest.org)}
  :status sat
  :difficulty { 0 }
  :category { industrial }
  :logic QF_IDL
  :extrafuns ((cvclZero Int))
  :extrafuns ((F14 Int))
  :extrafuns ((F16 Int))
  :extrafuns ((F18 Int))
  :extrafuns ((F20 Int))
  :extrafuns ((F22 Int))
  :extrafuns ((F36 Int))
  :extrafuns ((F37 Int))
  :extrafuns ((F38 Int))
  :extrafuns ((F39 Int))
  :extrafuns ((F40 Int))
  :extrafuns ((F43 Int))
  :extrafuns ((F44 Int))
  :extrafuns ((F45 Int))
  :extrafuns ((F46 Int))
  :extrafuns ((F47 Int))
  :extrafuns ((F54 Int))
  :extrafuns ((F55 Int))
  :extrafuns ((F56 Int))
  :extrafuns ((F57 Int))
  :extrafuns ((F58 Int))
  :extrafuns ((F61 Int))
  :extrafuns ((F62 Int))
  :extrafuns ((F63 Int))
  :extrafuns ((F64 Int))
  :extrafuns ((F65 Int))
  :extrafuns ((F74 Int))
  :extrafuns ((F75 Int))
  :extrafuns ((F76 Int))
  :extrafuns ((F77 Int))
  :extrafuns ((F78 Int))
  :extrafuns ((F85 Int))
  :extrafuns ((F86 Int))
  :extrafuns ((F87 Int))
  :extrafuns ((F88 Int))
  :extrafuns ((F89 Int))
  :extrafuns ((F92 Int))
  :extrafuns ((F93 Int))
  :extrafuns ((F94 Int))
  :extrafuns ((F95 Int))
  :extrafuns ((F96 Int))
  :extrapreds ((P10))
  :extrapreds ((P12))
  :extrapreds ((P24))
  :extrapreds ((P26))
  :extrapreds ((P28))
  :extrapreds ((P30))
  :extrapreds ((P32))
  :extrapreds ((P34))
  :extrapreds ((P41))
  :extrapreds ((P42))
  :extrapreds ((P48))
  :extrapreds ((P49))
  :extrapreds ((P50))
  :extrapreds ((P51))
  :extrapreds ((P52))
  :extrapreds ((P53))
  :extrapreds ((P59))
  :extrapreds ((P60))
  :extrapreds ((P66))
  :extrapreds ((P67))
  :extrapreds ((P68))
  :extrapreds ((P69))
  :extrapreds ((P70))
  :extrapreds ((P71))
  :extrapreds ((P72))
  :extrapreds ((P73))
  :extrapreds ((P79))
  :extrapreds ((P80))
  :extrapreds ((P81))
  :extrapreds ((P82))
  :extrapreds ((P83))
  :extrapreds ((P84))
  :extrapreds ((P90))
  :extrapreds ((P91))
  :extrapreds ((P97))
  :extrapreds ((P98))
  :extrapreds ((P99))
  :extrapreds ((P100))
  :extrapreds ((P101))
  :extrapreds ((P102))
  :formula
(flet ($cvcl_0 (not P90)) (flet ($cvcl_2 (or (and P100 P90)  $cvcl_0 )) (flet ($cvcl_6 (and P98 P90)) (flet ($cvcl_3 (iff $cvcl_2 $cvcl_6)) (flet ($cvcl_1 (or (and P99 P90)  $cvcl_0 )) (flet ($cvcl_7 (and P97 P90)) (flet ($cvcl_11 (not (iff $cvcl_1 $cvcl_7))) (flet ($cvcl_8 (not $cvcl_3)) (flet ($cvcl_4 (or (and $cvcl_3 (and $cvcl_1 $cvcl_11))  (and $cvcl_2 $cvcl_8) )) (flet ($cvcl_5 (and $cvcl_4 P91)) (flet ($cvcl_14 (not $cvcl_5)) (flet ($cvcl_10 (and $cvcl_1 $cvcl_7)) (flet ($cvcl_9 (or (and $cvcl_2 $cvcl_6)  (and $cvcl_10 $cvcl_8) )) (flet ($cvcl_17 (or (and (or (and $cvcl_14 P102)  (and $cvcl_5 $cvcl_9) ) P90)  (and $cvcl_9 $cvcl_0) )) (flet ($cvcl_12 (not (iff $cvcl_10 $cvcl_8))) (flet ($cvcl_13 (not $cvcl_9)) (flet ($cvcl_15 (or (and $cvcl_12 $cvcl_13)  (and (or (and $cvcl_9 $cvcl_11)  (and (not (iff $cvcl_9 $cvcl_11)) $cvcl_9) ) (not (iff $cvcl_12 $cvcl_13))) )) (flet ($cvcl_16 (or (and (or (and $cvcl_5 $cvcl_15)  (and P101 $cvcl_14) ) P90)  (and $cvcl_15 $cvcl_0) )) (flet ($cvcl_18 (and $cvcl_16 $cvcl_0)) (flet ($cvcl_24 (not $cvcl_17)) (flet ($cvcl_22 (and $cvcl_18 $cvcl_24)) (flet ($cvcl_21 (not $cvcl_16)) (flet ($cvcl_25 (and $cvcl_21 $cvcl_0)) (flet ($cvcl_20 (and $cvcl_17 $cvcl_25)) (flet ($cvcl_19 (and $cvcl_17 $cvcl_18)) (flet ($cvcl_23 (and $cvcl_16 P90)) (flet ($cvcl_27 (and $cvcl_17 $cvcl_23)) (flet ($cvcl_26 (and $cvcl_21 P90)) (flet ($cvcl_28 (and $cvcl_17 $cvcl_26)) (flet ($cvcl_29 (and $cvcl_23 $cvcl_24)) (flet ($cvcl_30 (and $cvcl_25 $cvcl_24)) (flet ($cvcl_31 (and $cvcl_24 $cvcl_26)) (flet ($cvcl_40 (not (iff $cvcl_16 $cvcl_17))) (flet ($cvcl_44 (not P59)) (flet ($cvcl_43 (or (and P59 P68)  $cvcl_44 )) (flet ($cvcl_48 (and P59 P66)) (flet ($cvcl_54 (not (iff $cvcl_43 $cvcl_48))) (flet ($cvcl_46 (or (and P59 P69)  $cvcl_44 )) (flet ($cvcl_47 (and P59 P67)) (flet ($cvcl_45 (iff $cvcl_46 $cvcl_47)) (flet ($cvcl_49 (not $cvcl_45)) (flet ($cvcl_51 (or (and (and $cvcl_54 $cvcl_43) $cvcl_45)  (and $cvcl_49 $cvcl_46) )) (flet ($cvcl_53 (and $cvcl_43 $cvcl_48)) (flet ($cvcl_50 (or (and $cvcl_46 $cvcl_47)  (and $cvcl_53 $cvcl_49) )) (flet ($cvcl_52 (and $cvcl_51 P60)) (flet ($cvcl_57 (not $cvcl_52)) (flet ($cvcl_60 (or (and $cvcl_50 $cvcl_44)  (and (or (and $cvcl_50 $cvcl_52)  (and $cvcl_57 P71) ) P59) )) (flet ($cvcl_55 (not (iff $cvcl_53 $cvcl_49))) (flet ($cvcl_56 (not $cvcl_50)) (flet ($cvcl_58 (or (and $cvcl_55 $cvcl_56)  (and (or (and $cvcl_50 $cvcl_54)  (and $cvcl_50 (not (iff $cvcl_50 $cvcl_54))) ) (not (iff $cvcl_55 $cvcl_56))) )) (flet ($cvcl_61 (or (and P59 (or (and $cvcl_52 $cvcl_58)  (and $cvcl_57 P70) ))  (and $cvcl_58 $cvcl_44) )) (flet ($cvcl_59 (not $cvcl_61)) (flet ($cvcl_66 (and $cvcl_59 $cvcl_44)) (flet ($cvcl_62 (not $cvcl_60)) (flet ($cvcl_63 (and $cvcl_66 $cvcl_62)) (flet ($cvcl_64 (and $cvcl_61 $cvcl_44)) (flet ($cvcl_68 (and $cvcl_60 $cvcl_64)) (flet ($cvcl_65 (and $cvcl_59 P59)) (flet ($cvcl_74 (and $cvcl_65 $cvcl_62)) (flet ($cvcl_67 (and $cvcl_61 P59)) (flet ($cvcl_73 (and $cvcl_62 $cvcl_67)) (flet ($cvcl_72 (and $cvcl_62 $cvcl_64)) (flet ($cvcl_71 (and $cvcl_60 $cvcl_65)) (flet ($cvcl_70 (and $cvcl_66 $cvcl_60)) (flet ($cvcl_69 (and $cvcl_60 $cvcl_67)) (flet ($cvcl_80 (not (iff $cvcl_60 $cvcl_61))) (flet ($cvcl_88 (not P41)) (flet ($cvcl_86 (or (and P41 P51)  $cvcl_88 )) (flet ($cvcl_92 (and P49 P41)) (flet ($cvcl_87 (iff $cvcl_92 $cvcl_86)) (flet ($cvcl_90 (not $cvcl_87)) (flet ($cvcl_89 (or $cvcl_88  (and P41 P50) )) (flet ($cvcl_91 (and P41 P48)) (flet ($cvcl_97 (not (iff $cvcl_91 $cvcl_89))) (flet ($cvcl_94 (or (and $cvcl_86 $cvcl_90)  (and $cvcl_87 (and $cvcl_89 $cvcl_97)) )) (flet ($cvcl_96 (and $cvcl_91 $cvcl_89)) (flet ($cvcl_93 (or (and $cvcl_90 $cvcl_96)  (and $cvcl_92 $cvcl_86) )) (flet ($cvcl_95 (and $cvcl_94 P42)) (flet ($cvcl_101 (not $cvcl_95)) (flet ($cvcl_102 (or (and $cvcl_88 $cvcl_93)  (and P41 (or (and $cvcl_93 $cvcl_95)  (and P53 $cvcl_101) )) )) (flet ($cvcl_98 (not $cvcl_93)) (flet ($cvcl_99 (not (iff $cvcl_90 $cvcl_96))) (flet ($cvcl_100 (or (and (not (iff $cvcl_98 $cvcl_99)) (or (and $cvcl_93 (not (iff $cvcl_97 $cvcl_93)))  (and $cvcl_97 $cvcl_93) ))  (and $cvcl_98 $cvcl_99) )) (flet ($cvcl_103 (or (and $cvcl_88 $cvcl_100)  (and P41 (or (and $cvcl_95 $cvcl_100)  (and P52 $cvcl_101) )) )) (flet ($cvcl_104 (not $cvcl_102)) (flet ($cvcl_105 (not $cvcl_103)) (flet ($cvcl_106 (and P41 $cvcl_105)) (flet ($cvcl_110 (and $cvcl_104 $cvcl_106)) (flet ($cvcl_107 (and $cvcl_88 $cvcl_105)) (flet ($cvcl_111 (and $cvcl_104 $cvcl_107)) (flet ($cvcl_108 (and P41 $cvcl_103)) (flet ($cvcl_112 (and $cvcl_104 $cvcl_108)) (flet ($cvcl_109 (and $cvcl_88 $cvcl_103)) (flet ($cvcl_113 (and $cvcl_104 $cvcl_109)) (flet ($cvcl_114 (and $cvcl_102 $cvcl_106)) (flet ($cvcl_115 (and $cvcl_102 $cvcl_107)) (flet ($cvcl_116 (and $cvcl_102 $cvcl_108)) (flet ($cvcl_117 (and $cvcl_102 $cvcl_109)) (flet ($cvcl_123 (not (iff $cvcl_102 $cvcl_103))) (flet ($cvcl_32 (or (or (or (or (and (and $cvcl_22 P90) (> (- F96 F88) 0))  (or (or (and (and $cvcl_20 P90) (> (- F96 F87) 0))  (or (or (and (> (- F96 F86) 0) (and $cvcl_19 P90))  (or (or (or (or (or (or (or (and (< (- F86 F85) 0) (and $cvcl_19 $cvcl_0))  (and (< (- F92 F85) 0) (and $cvcl_27 $cvcl_0)) )  (and (< (- F87 F85) 0) (and $cvcl_20 $cvcl_0)) )  (and (< (- F93 F85) 0) (and $cvcl_28 $cvcl_0)) )  (and (< (- F88 F85) 0) (and $cvcl_22 $cvcl_0)) )  (and (< (- F94 F85) 0) (and $cvcl_29 $cvcl_0)) )  (and (< (- F89 F85) 0) (and $cvcl_30 $cvcl_0)) )  (and (< (- F95 F85) 0) (and $cvcl_31 $cvcl_0)) ) )  (and (> (- F96 F92) 0) (and $cvcl_27 P90)) ) )  (and (> (- F96 F93) 0) (and $cvcl_28 P90)) ) )  (and (> (- F96 F94) 0) (and $cvcl_29 P90)) )  (and (> (- F96 F89) 0) (and $cvcl_30 P90)) )  (and (> (- F96 F95) 0) (and $cvcl_31 P90)) )) (flet ($cvcl_34 (and $cvcl_32 $cvcl_0)) (flet ($cvcl_41 (not $cvcl_34)) (flet ($cvcl_33 (and $cvcl_5 $cvcl_32)) (flet ($cvcl_42 (not $cvcl_33)) (flet ($cvcl_35 (not $cvcl_32)) (flet ($cvcl_37 (and $cvcl_0 $cvcl_35)) (flet ($cvcl_38 (not $cvcl_37)) (flet ($cvcl_36 (and $cvcl_5 $cvcl_35)) (flet ($cvcl_39 (not $cvcl_36)) (flet ($cvcl_81 (or (or (and (and $cvcl_63 P59) (> (- F65 F58) 0))  (or (or (or (or (or (or (and (and P59 $cvcl_68) (> (- F65 F55) 0))  (or (and (and $cvcl_74 $cvcl_44) (< (- F64 F54) 0))  (or (and (and $cvcl_63 $cvcl_44) (< (- F58 F54) 0))  (or (and (and $cvcl_44 $cvcl_73) (< (- F63 F54) 0))  (or (and (and $cvcl_44 $cvcl_72) (< (- F57 F54) 0))  (or (and (and $cvcl_44 $cvcl_71) (< (- F62 F54) 0))  (or (and (and $cvcl_44 $cvcl_70) (< (- F56 F54) 0))  (or (and (and $cvcl_44 $cvcl_69) (< (- F61 F54) 0))  (and (and $cvcl_44 $cvcl_68) (< (- F55 F54) 0)) ) ) ) ) ) ) ) )  (and (and P59 $cvcl_69) (> (- F65 F61) 0)) )  (and (and P59 $cvcl_70) (> (- F65 F56) 0)) )  (and (and P59 $cvcl_71) (> (- F65 F62) 0)) )  (and (and P59 $cvcl_72) (> (- F65 F57) 0)) )  (and (and P59 $cvcl_73) (> (- F65 F63) 0)) ) )  (and (and $cvcl_74 P59) (> (- F65 F64) 0)) )) (flet ($cvcl_76 (not $cvcl_81)) (flet ($cvcl_75 (and $cvcl_44 $cvcl_76)) (flet ($cvcl_78 (not $cvcl_75)) (flet ($cvcl_77 (and $cvcl_52 $cvcl_76)) (flet ($cvcl_79 (not $cvcl_77)) (flet ($cvcl_83 (and $cvcl_44 $cvcl_81)) (flet ($cvcl_84 (not $cvcl_83)) (flet ($cvcl_82 (and $cvcl_52 $cvcl_81)) (flet ($cvcl_85 (not $cvcl_82)) (flet ($cvcl_118 (or (and (and P41 $cvcl_110) (> (- F47 F46) 0))  (or (and (and P41 $cvcl_111) (> (- F47 F40) 0))  (or (and (and P41 $cvcl_112) (> (- F47 F45) 0))  (or (and (> (- F47 F39) 0) (and P41 $cvcl_113))  (or (and (and $cvcl_114 P41) (> (- F47 F44) 0))  (or (and (and P41 $cvcl_115) (> (- F47 F38) 0))  (or (and (and P41 $cvcl_116) (> (- F47 F43) 0))  (or (and (and P41 $cvcl_117) (> (- F47 F37) 0))  (or (and (and $cvcl_88 $cvcl_110) (< (- F46 F36) 0))  (or (and (and $cvcl_88 $cvcl_111) (< (- F40 F36) 0))  (or (and (and $cvcl_88 $cvcl_112) (< (- F45 F36) 0))  (or (and (and $cvcl_88 $cvcl_113) (< (- F39 F36) 0))  (or (and (and $cvcl_114 $cvcl_88) (< (- F44 F36) 0))  (or (and (and $cvcl_88 $cvcl_115) (< (- F38 F36) 0))  (or (and (and $cvcl_88 $cvcl_116) (< (- F43 F36) 0))  (and (and $cvcl_88 $cvcl_117) (< (- F37 F36) 0)) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )) (flet ($cvcl_120 (and $cvcl_88 $cvcl_118)) (flet ($cvcl_119 (and $cvcl_95 $cvcl_118)) (flet ($cvcl_121 (not $cvcl_119)) (flet ($cvcl_122 (not $cvcl_120)) (flet ($cvcl_124 (not $cvcl_118)) (flet ($cvcl_126 (and $cvcl_124 $cvcl_88)) (flet ($cvcl_125 (and $cvcl_124 $cvcl_95)) (flet ($cvcl_128 (not $cvcl_125)) (flet ($cvcl_127 (not $cvcl_126)) (not (or (not (and (and (and (and (not (and (not $cvcl_4) P91)) (and (and (and (not P101) (and (and (not P99) (and (and (and (= (- cvclZero F96) 0) (and (= (- cvclZero F95) 0) (and (= (- cvclZero F94) 0) (and (= (- cvclZero F93) 0) (and (= (- cvclZero F92) 0) (and (not P91) $cvcl_0)))))) (not P97)) (not P98))) (not P100))) (not P102)) (and (and (or (and (<= (- F88 F87) 0) $cvcl_0)  (and (<= (- F94 F93) 0) P90) ) (or (and (<= (- F87 F86) 0) $cvcl_0)  (and (<= (- F93 F92) 0) P90) )) (or (and (<= (- F89 F88) 0) $cvcl_0)  (and (<= (- F95 F94) 0) P90) )))) (and (iff $cvcl_17 P71) (and (iff $cvcl_16 P70) (and (and (iff (or (and $cvcl_41 (or (and $cvcl_16 $cvcl_33)  (and $cvcl_42 $cvcl_1) ))  (and $cvcl_16 $cvcl_34) ) P68) (and (and (iff (or (and $cvcl_38 (or (and $cvcl_21 $cvcl_36)  (and $cvcl_39 $cvcl_7) ))  (and $cvcl_21 $cvcl_37) ) P66) (and (and (or (and (= (- F89 F64) 0) $cvcl_0)  (and (= (- F95 F64) 0) P90) ) (and (or (and (= (- F94 F63) 0) P90)  (and (= (- F88 F63) 0) $cvcl_0) ) (and (and (and (iff (or $cvcl_5  $cvcl_0 ) P60) P59) (or (and (= (- F86 F61) 0) $cvcl_0)  (and (= (- F92 F61) 0) P90) )) (or (and (= (- F87 F62) 0) $cvcl_0)  (and (= (- F93 F62) 0) P90) )))) (or (and (= (- F85 F65) 0) $cvcl_0)  (and (= (- F96 F65) 0) P90) ))) (iff (or (and $cvcl_38 (or (and $cvcl_39 $cvcl_6)  (and $cvcl_36 $cvcl_40) ))  (and $cvcl_40 $cvcl_37) ) P67))) (iff (or (and $cvcl_41 (or (and $cvcl_17 $cvcl_33)  (and $cvcl_42 $cvcl_2) ))  (and $cvcl_17 $cvcl_34) ) P69))))) (not (and (not $cvcl_51) P60))) (and (iff P84 $cvcl_60) (and (and (and (and (and (and (and (or (and (= (- F77 F64) 0) P59)  (and (= (- F77 F58) 0) $cvcl_44) ) (and (and (and (or (and (= (- F74 F61) 0) P59)  (and (= (- F74 F55) 0) $cvcl_44) ) (and (iff P73 (or $cvcl_52  $cvcl_44 )) P72)) (or (and (= (- F75 F56) 0) $cvcl_44)  (and (= (- F75 F62) 0) P59) )) (or (and (= (- F76 F57) 0) $cvcl_44)  (and (= (- F76 F63) 0) P59) ))) (or (and (= (- F78 F54) 0) $cvcl_44)  (and (= (- F78 F65) 0) P59) )) (iff P79 (or (and $cvcl_59 $cvcl_75)  (and $cvcl_78 (or (and $cvcl_48 $cvcl_79)  (and $cvcl_59 $cvcl_77) )) ))) (iff P80 (or (and $cvcl_78 (or (and $cvcl_77 $cvcl_80)  (and $cvcl_47 $cvcl_79) ))  (and $cvcl_80 $cvcl_75) ))) (iff P81 (or (and $cvcl_84 (or (and $cvcl_82 $cvcl_61)  (and $cvcl_43 $cvcl_85) ))  (and $cvcl_61 $cvcl_83) ))) (iff P82 (or (and $cvcl_60 $cvcl_83)  (and $cvcl_84 (or (and $cvcl_46 $cvcl_85)  (and $cvcl_82 $cvcl_60) )) ))) (iff P83 $cvcl_61)))))  (not (and (and (not (and (not $cvcl_94) P42)) (and (and (or (and P41 (<= (- F46 F45) 0))  (and $cvcl_88 (<= (- F40 F39) 0)) ) (and (or (and P41 (<= (- F44 F43) 0))  (and $cvcl_88 (<= (- F38 F37) 0)) ) (or (and P41 (<= (- F45 F44) 0))  (and $cvcl_88 (<= (- F39 F38) 0)) ))) (and (not P53) (and (not P52) (and (not P51) (and (not P50) (and (not P49) (and (not P48) (and (and (and (and (= (- cvclZero F44) 0) (and (and $cvcl_88 (not P42)) (= (- cvclZero F43) 0))) (= (- cvclZero F45) 0)) (= (- cvclZero F46) 0)) (= (- cvclZero F47) 0)))))))))) (and (iff P34 $cvcl_102) (and (iff P32 $cvcl_103) (and (iff (or (and $cvcl_102 $cvcl_120)  (and (or (and $cvcl_86 $cvcl_121)  (and $cvcl_102 $cvcl_119) ) $cvcl_122) ) P30) (and (iff (or (and $cvcl_103 $cvcl_120)  (and (or (and $cvcl_89 $cvcl_121)  (and $cvcl_103 $cvcl_119) ) $cvcl_122) ) P28) (and (iff P26 (or (and $cvcl_123 $cvcl_126)  (and (or (and $cvcl_123 $cvcl_125)  (and $cvcl_128 $cvcl_92) ) $cvcl_127) )) (and (iff P24 (or (and $cvcl_126 $cvcl_105)  (and $cvcl_127 (or (and $cvcl_128 $cvcl_91)  (and $cvcl_125 $cvcl_105) )) )) (and (or (and $cvcl_88 (= (- F36 F22) 0))  (and P41 (= (- F47 F22) 0)) ) (and (or (and P41 (= (- F46 F20) 0))  (and $cvcl_88 (= (- F40 F20) 0)) ) (and (or (and P41 (= (- F45 F18) 0))  (and $cvcl_88 (= (- F39 F18) 0)) ) (and (or (and P41 (= (- F44 F16) 0))  (and $cvcl_88 (= (- F38 F16) 0)) ) (and (or (and P41 (= (- F43 F14) 0))  (and $cvcl_88 (= (- F37 F14) 0)) ) (and P10 (iff P12 (or $cvcl_88  $cvcl_95 )))))))))))))))) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
)