(benchmark B_27s.smt
  :source {
UCLID benchmark suite.  See UCLID project: http://www.cs.cmu.edu/~uclid

This benchmark was automatically translated into SMT-LIB format from
CVC format using CVC Lite
}
  :status unsat
  :logic QF_UFIDL
  :extrafuns ((BmainB_46_init_const_N1_c Int))
  :extrapreds ((BB_p0))
  :extrafuns ((BmainB_46_init_const_N1_643_c Int))
  :extrafuns ((BmainB_46_init_const_H_zN1_693_c Int))
  :extrafuns ((BmainB_46_init_const_T1_644_c Int))
  :extrafuns ((BmainB_46_iBOT Int))
  :extrafuns ((BmainB_46_init_const_zN1_693_c Int))
  :extrafuns ((BmainB_46_init_const_T1_c Int))
  :extrafuns ((BmainB_46_sqrt Int Int))
  :extrafuns ((BmainB_46_f_mul_1 Int Int Int))
  :extrafuns ((BmainB_46_f_minus_1 Int Int Int))
  :extrafuns ((BmainB_46_f_minus_2 Int Int Int))
  :extrafuns ((BmainB_46_f_minus_3 Int Int Int))
  :extrafuns ((BmainB_46_f_minus_4 Int Int Int))
  :extrafuns ((BmainB_46_f_minus_5 Int Int Int))
  :extrapreds ((BmainB_46_f_lt_1 Int Int))
  :extrapreds ((BmainB_46_f_lt_2 Int Int))
  :extrapreds ((BmainB_46_f_lt_3 Int Int))
  :extrapreds ((BmainB_46_f_lt_4 Int Int))
  :extrapreds ((BmainB_46_f_ge_1 Int Int))
  :extrapreds ((BmainB_46_f_lt_5 Int Int))
  :extrapreds ((BmainB_46_f_ge_2 Int Int))
  :extrapreds ((BmainB_46_f_ge_3 Int Int))
  :extrapreds ((BmainB_46_f_ge_4 Int Int))
  :extrapreds ((BmainB_46_f_ge_5 Int Int))
  :extrapreds ((BmainB_46_f_ge_6 Int Int))
  :extrafuns ((BmainB_46_f_div_2 Int Int Int))
  :extrafuns ((BmainB_46_f_div_1 Int Int Int))
  :extrafuns ((BmainB_46_f_plus_1 Int Int Int))
  :formula
(let (?cvcl_1 BmainB_46_iBOT) (let (?cvcl_5 (+ 1 ?cvcl_1)) (let (?cvcl_10 (+ 1 ?cvcl_5)) (let (?cvcl_0 (+ 1 ?cvcl_10)) (let (?cvcl_2 (+ 1 ?cvcl_0)) (let (?cvcl_3 (+ 1 ?cvcl_2)) (let (?cvcl_31 (+ 1 ?cvcl_3)) (let (?cvcl_11 (+ 1 ?cvcl_31)) (let (?cvcl_43 (BmainB_46_f_minus_1 ?cvcl_11 ?cvcl_0)) (let (?cvcl_29 BmainB_46_init_const_T1_644_c) (let (?cvcl_4 (BmainB_46_f_plus_1 ?cvcl_2 ?cvcl_29)) (let (?cvcl_6 (BmainB_46_f_div_1 ?cvcl_3 ?cvcl_2)) (let (?cvcl_7 (BmainB_46_f_div_2 ?cvcl_3 ?cvcl_4)) (let (?cvcl_8 (BmainB_46_sqrt (ite (= ?cvcl_4 ?cvcl_5) ?cvcl_6 ?cvcl_7))) (let (?cvcl_9 BmainB_46_init_const_N1_643_c) (let (?cvcl_33 (BmainB_46_f_mul_1 ?cvcl_9 ?cvcl_8)) (let (?cvcl_30 (ite BB_p0 ?cvcl_5 ?cvcl_10)) (flet ($cvcl_15 (= ?cvcl_30 ?cvcl_10)) (let (?cvcl_16 BmainB_46_init_const_H_zN1_693_c) (let (?cvcl_12 (BmainB_46_f_minus_2 ?cvcl_9 (ite $cvcl_15 ?cvcl_9 ?cvcl_16))) (let (?cvcl_39 (BmainB_46_f_minus_3 ?cvcl_9 ?cvcl_0)) (let (?cvcl_38 (+ 1 ?cvcl_11)) (let (?cvcl_13 (+ 1 ?cvcl_38)) (let (?cvcl_37 (+ 1 ?cvcl_13)) (let (?cvcl_36 (BmainB_46_f_minus_4 ?cvcl_37 ?cvcl_0)) (let (?cvcl_32 (BmainB_46_f_minus_3 ?cvcl_12 ?cvcl_0)) (let (?cvcl_28 BmainB_46_init_const_T1_c) (let (?cvcl_18 (BmainB_46_f_plus_1 ?cvcl_2 ?cvcl_28)) (flet ($cvcl_19 (not (= ?cvcl_18 ?cvcl_1))) (let (?cvcl_34 (BmainB_46_f_minus_5 ?cvcl_13 ?cvcl_0)) (let (?cvcl_14 BmainB_46_init_const_N1_c) (let (?cvcl_102 (BmainB_46_f_minus_3 ?cvcl_14 ?cvcl_0)) (let (?cvcl_17 (BmainB_46_f_minus_2 ?cvcl_14 (ite $cvcl_15 ?cvcl_14 ?cvcl_16))) (flet ($cvcl_27 (not (= ?cvcl_14 ?cvcl_1))) (let (?cvcl_77 (ite $cvcl_27 ?cvcl_17 ?cvcl_1)) (let (?cvcl_66 (BmainB_46_f_minus_3 ?cvcl_77 ?cvcl_0)) (let (?cvcl_25 (BmainB_46_f_div_2 ?cvcl_3 ?cvcl_18)) (let (?cvcl_20 (ite $cvcl_19 (ite (= ?cvcl_18 ?cvcl_5) ?cvcl_10 ?cvcl_5) ?cvcl_1)) (flet ($cvcl_23 (= ?cvcl_20 ?cvcl_10)) (flet ($cvcl_21 (not (= ?cvcl_20 ?cvcl_1))) (flet ($cvcl_46 (not (= ?cvcl_10 ?cvcl_1))) (flet ($cvcl_22 (or $cvcl_21  $cvcl_46 )) (let (?cvcl_24 (ite $cvcl_22 (ite (= (ite $cvcl_21 ?cvcl_20 ?cvcl_1) ?cvcl_10) ?cvcl_10 (ite $cvcl_22 ?cvcl_5 ?cvcl_1)) ?cvcl_1)) (let (?cvcl_26 (BmainB_46_sqrt (ite (and $cvcl_23 (= ?cvcl_24 ?cvcl_10)) (ite $cvcl_23 ?cvcl_6 ?cvcl_1) (ite (= ?cvcl_24 ?cvcl_5) ?cvcl_25 ?cvcl_1)))) (let (?cvcl_79 (BmainB_46_f_mul_1 ?cvcl_14 ?cvcl_26)) (let (?cvcl_40 BmainB_46_init_const_zN1_693_c) (flet ($cvcl_55 (= ?cvcl_30 ?cvcl_5)) (flet ($cvcl_35 (not $cvcl_15)) (flet ($cvcl_41 (not (= ?cvcl_30 ?cvcl_1))) (flet ($cvcl_42 (and $cvcl_15 $cvcl_27)) (flet ($cvcl_44 (or $cvcl_42  $cvcl_41 )) (let (?cvcl_45 (ite $cvcl_44 (ite (= (ite $cvcl_42 (ite (BmainB_46_f_lt_1 ?cvcl_14 ?cvcl_43) ?cvcl_10 ?cvcl_5) ?cvcl_1) ?cvcl_10) ?cvcl_10 (ite $cvcl_44 ?cvcl_5 ?cvcl_1)) ?cvcl_1)) (flet ($cvcl_51 (and $cvcl_15 (= ?cvcl_45 ?cvcl_10))) (flet ($cvcl_52 (and $cvcl_15 (= ?cvcl_45 ?cvcl_5))) (flet ($cvcl_50 (or $cvcl_51  $cvcl_52 )) (flet ($cvcl_47 (or $cvcl_41  $cvcl_46 )) (let (?cvcl_48 (ite $cvcl_47 (ite (= (ite $cvcl_41 ?cvcl_30 ?cvcl_1) ?cvcl_10) ?cvcl_10 (ite $cvcl_47 ?cvcl_5 ?cvcl_1)) ?cvcl_1)) (flet ($cvcl_69 (= ?cvcl_48 ?cvcl_10)) (flet ($cvcl_49 (and $cvcl_50 $cvcl_69)) (flet ($cvcl_70 (= ?cvcl_48 ?cvcl_5)) (flet ($cvcl_53 (and $cvcl_27 $cvcl_70)) (let (?cvcl_74 (ite $cvcl_15 (ite $cvcl_15 ?cvcl_5 ?cvcl_1) ?cvcl_1)) (let (?cvcl_76 (ite $cvcl_15 (ite $cvcl_15 ?cvcl_10 ?cvcl_1) ?cvcl_1)) (let (?cvcl_54 (ite (or $cvcl_49  $cvcl_53 ) (ite $cvcl_49 (ite $cvcl_50 (ite $cvcl_51 ?cvcl_74 (ite $cvcl_52 ?cvcl_76 ?cvcl_1)) ?cvcl_1) (ite $cvcl_53 (ite $cvcl_27 (ite (BmainB_46_f_ge_1 ?cvcl_14 ?cvcl_11) ?cvcl_10 ?cvcl_5) ?cvcl_1) ?cvcl_1)) ?cvcl_1)) (let (?cvcl_60 (ite $cvcl_41 (ite $cvcl_55 ?cvcl_10 ?cvcl_5) ?cvcl_1)) (flet ($cvcl_56 (= ?cvcl_60 ?cvcl_10)) (let (?cvcl_61 (ite (and (and $cvcl_15 $cvcl_56) $cvcl_56) ?cvcl_10 ?cvcl_5)) (flet ($cvcl_58 (= (ite $cvcl_41 (ite (and $cvcl_15 (= (ite $cvcl_41 ?cvcl_61 ?cvcl_1) ?cvcl_10)) ?cvcl_10 ?cvcl_5) ?cvcl_1) ?cvcl_10)) (let (?cvcl_57 (ite $cvcl_41 (ite (or $cvcl_15  $cvcl_58 ) ?cvcl_10 ?cvcl_5) ?cvcl_1)) (let (?cvcl_59 (ite (not (= ?cvcl_57 ?cvcl_1)) (ite (or (= ?cvcl_57 ?cvcl_10)  $cvcl_58 ) ?cvcl_10 ?cvcl_5) ?cvcl_1)) (let (?cvcl_62 (ite (not (= ?cvcl_59 ?cvcl_1)) (ite (or (= ?cvcl_59 ?cvcl_10)  (= (ite $cvcl_41 (ite (and $cvcl_15 (= (ite (not (= ?cvcl_60 ?cvcl_1)) ?cvcl_61 ?cvcl_1) ?cvcl_10)) ?cvcl_10 ?cvcl_5) ?cvcl_1) ?cvcl_10) ) ?cvcl_10 ?cvcl_5) ?cvcl_1)) (let (?cvcl_100 (ite (not (= ?cvcl_62 ?cvcl_1)) (ite (= ?cvcl_62 ?cvcl_10) ?cvcl_59 ?cvcl_30) ?cvcl_1)) (let (?cvcl_63 (ite $cvcl_41 (ite (and $cvcl_15 (or (and $cvcl_15 (= (ite (not (= ?cvcl_54 ?cvcl_1)) (ite (= ?cvcl_54 ?cvcl_5) ?cvcl_10 ?cvcl_5) ?cvcl_1) ?cvcl_10))  (= ?cvcl_100 ?cvcl_10) )) ?cvcl_10 ?cvcl_5) ?cvcl_1)) (let (?cvcl_64 (ite (not (= ?cvcl_63 ?cvcl_1)) (ite (or (= ?cvcl_63 ?cvcl_10)  (= (ite $cvcl_41 (ite (and $cvcl_15 (BmainB_46_f_ge_2 ?cvcl_5 ?cvcl_14)) ?cvcl_10 ?cvcl_5) ?cvcl_1) ?cvcl_10) ) ?cvcl_10 ?cvcl_5) ?cvcl_1)) (let (?cvcl_65 (ite (not (= ?cvcl_64 ?cvcl_1)) (ite (= ?cvcl_64 ?cvcl_10) ?cvcl_63 ?cvcl_30) ?cvcl_1)) (flet ($cvcl_99 (= (ite $cvcl_41 (ite $cvcl_35 ?cvcl_10 ?cvcl_5) ?cvcl_1) ?cvcl_10)) (flet ($cvcl_67 (or $cvcl_15  $cvcl_41 )) (let (?cvcl_103 (ite $cvcl_67 ?cvcl_5 ?cvcl_1)) (let (?cvcl_68 (ite $cvcl_67 (ite (= (ite $cvcl_15 (ite (BmainB_46_f_lt_4 ?cvcl_31 ?cvcl_66) ?cvcl_10 ?cvcl_5) ?cvcl_1) ?cvcl_10) ?cvcl_10 ?cvcl_103) ?cvcl_1)) (flet ($cvcl_73 (and $cvcl_15 (= ?cvcl_68 ?cvcl_10))) (flet ($cvcl_75 (and $cvcl_15 (= ?cvcl_68 ?cvcl_5))) (flet ($cvcl_72 (or $cvcl_73  $cvcl_75 )) (flet ($cvcl_71 (and $cvcl_72 $cvcl_69)) (let (?cvcl_78 (ite (or $cvcl_71  $cvcl_70 ) (ite $cvcl_71 (ite $cvcl_72 (ite $cvcl_73 ?cvcl_74 (ite $cvcl_75 ?cvcl_76 ?cvcl_1)) ?cvcl_1) (ite $cvcl_70 (ite (BmainB_46_f_ge_5 ?cvcl_31 ?cvcl_77) ?cvcl_10 ?cvcl_5) ?cvcl_1)) ?cvcl_1)) (let (?cvcl_81 (ite $cvcl_27 ?cvcl_79 ?cvcl_1)) (flet ($cvcl_84 (not (= ?cvcl_81 ?cvcl_1))) (flet ($cvcl_80 (and $cvcl_15 $cvcl_84)) (flet ($cvcl_82 (or $cvcl_80  $cvcl_41 )) (let (?cvcl_92 (ite $cvcl_82 ?cvcl_5 ?cvcl_1)) (let (?cvcl_83 (ite $cvcl_82 (ite (= (ite $cvcl_80 (ite (BmainB_46_f_lt_5 ?cvcl_81 ?cvcl_34) ?cvcl_10 ?cvcl_5) ?cvcl_1) ?cvcl_10) ?cvcl_10 ?cvcl_92) ?cvcl_1)) (flet ($cvcl_87 (and $cvcl_15 (= ?cvcl_83 ?cvcl_10))) (flet ($cvcl_88 (and $cvcl_15 (= ?cvcl_83 ?cvcl_5))) (flet ($cvcl_86 (or $cvcl_87  $cvcl_88 )) (flet ($cvcl_85 (and $cvcl_86 $cvcl_69)) (let (?cvcl_91 (ite $cvcl_84 (ite (BmainB_46_f_ge_6 ?cvcl_81 ?cvcl_13) ?cvcl_10 ?cvcl_5) ?cvcl_1)) (flet ($cvcl_90 (not (= ?cvcl_91 ?cvcl_1))) (flet ($cvcl_89 (and $cvcl_90 $cvcl_70)) (let (?cvcl_93 (ite $cvcl_82 (ite (= (ite $cvcl_80 (ite (BmainB_46_f_lt_3 ?cvcl_81 ?cvcl_36) ?cvcl_10 ?cvcl_5) ?cvcl_1) ?cvcl_10) ?cvcl_10 ?cvcl_92) ?cvcl_1)) (flet ($cvcl_96 (and $cvcl_15 (= ?cvcl_93 ?cvcl_10))) (flet ($cvcl_97 (and $cvcl_15 (= ?cvcl_93 ?cvcl_5))) (flet ($cvcl_95 (or $cvcl_96  $cvcl_97 )) (flet ($cvcl_94 (and $cvcl_95 $cvcl_69)) (flet ($cvcl_98 (and $cvcl_84 $cvcl_70)) (let (?cvcl_101 (ite (not (= ?cvcl_100 ?cvcl_1)) (ite (= ?cvcl_100 ?cvcl_5) ?cvcl_10 ?cvcl_5) ?cvcl_1)) (let (?cvcl_104 (ite $cvcl_67 (ite (= (ite $cvcl_15 (ite (BmainB_46_f_lt_2 ?cvcl_38 ?cvcl_102) ?cvcl_10 ?cvcl_5) ?cvcl_1) ?cvcl_10) ?cvcl_10 ?cvcl_103) ?cvcl_1)) (flet ($cvcl_107 (and $cvcl_15 (= ?cvcl_104 ?cvcl_10))) (flet ($cvcl_108 (and $cvcl_15 (= ?cvcl_104 ?cvcl_5))) (flet ($cvcl_106 (or $cvcl_107  $cvcl_108 )) (flet ($cvcl_105 (and $cvcl_106 $cvcl_69)) (not (or (not (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?cvcl_43 ?cvcl_1)) (not (= ?cvcl_4 ?cvcl_1))) (not (= ?cvcl_6 ?cvcl_1))) (not (= ?cvcl_7 ?cvcl_1))) (not (= ?cvcl_8 ?cvcl_1))) (not (= ?cvcl_33 ?cvcl_1))) (not (= ?cvcl_12 ?cvcl_1))) (not (= ?cvcl_39 ?cvcl_1))) (not (= ?cvcl_36 ?cvcl_1))) (not (= ?cvcl_32 ?cvcl_1))) $cvcl_19) (not (= ?cvcl_34 ?cvcl_1))) (not (= ?cvcl_102 ?cvcl_1))) (not (= ?cvcl_17 ?cvcl_1))) (not (= ?cvcl_66 ?cvcl_1))) (not (= ?cvcl_25 ?cvcl_1))) (not (= ?cvcl_26 ?cvcl_1))) (not (= ?cvcl_79 ?cvcl_1))) $cvcl_27) (not (= ?cvcl_40 ?cvcl_1))) (not (= ?cvcl_16 ?cvcl_1))) (not (= ?cvcl_9 ?cvcl_1))) (not (= ?cvcl_28 ?cvcl_1))) (not (= ?cvcl_29 ?cvcl_1))) (and (and (and (and (and $cvcl_55 (= ?cvcl_30 (ite (and (or (and (or (and $cvcl_15 (not (BmainB_46_f_lt_4 ?cvcl_31 ?cvcl_32)))  (and $cvcl_35 (BmainB_46_f_ge_5 ?cvcl_31 ?cvcl_12)) ) (or (and $cvcl_15 (not (BmainB_46_f_lt_5 ?cvcl_33 ?cvcl_34)))  (and $cvcl_35 (BmainB_46_f_ge_6 ?cvcl_33 ?cvcl_13)) ))  (or (and $cvcl_15 (not (BmainB_46_f_lt_3 ?cvcl_33 ?cvcl_36)))  (and $cvcl_35 (BmainB_46_f_ge_4 ?cvcl_33 ?cvcl_37)) ) ) $cvcl_35) ?cvcl_10 ?cvcl_5))) (= ?cvcl_30 (ite (and $cvcl_35 (or (and $cvcl_15 (not (BmainB_46_f_lt_2 ?cvcl_38 ?cvcl_39)))  (and $cvcl_35 (BmainB_46_f_ge_3 ?cvcl_38 ?cvcl_9)) )) ?cvcl_10 ?cvcl_5))) (= ?cvcl_14 ?cvcl_9)) (= ?cvcl_16 ?cvcl_40)) (= ?cvcl_28 ?cvcl_29))))  (and (and (= ?cvcl_30 (ite (not (= ?cvcl_65 ?cvcl_1)) (ite (and (= ?cvcl_65 ?cvcl_10) $cvcl_99) ?cvcl_10 ?cvcl_5) ?cvcl_1)) (= ?cvcl_30 (ite (not (= ?cvcl_78 ?cvcl_1)) (ite (or (and (= ?cvcl_78 ?cvcl_10) (= (ite (or $cvcl_85  $cvcl_89 ) (ite $cvcl_85 (ite $cvcl_86 (ite $cvcl_87 ?cvcl_74 (ite $cvcl_88 ?cvcl_76 ?cvcl_1)) ?cvcl_1) (ite $cvcl_89 (ite $cvcl_90 ?cvcl_91 ?cvcl_1) ?cvcl_1)) ?cvcl_1) ?cvcl_10))  (and (= (ite (or $cvcl_94  $cvcl_98 ) (ite $cvcl_94 (ite $cvcl_95 (ite $cvcl_96 ?cvcl_74 (ite $cvcl_97 ?cvcl_76 ?cvcl_1)) ?cvcl_1) (ite $cvcl_98 (ite $cvcl_84 (ite (BmainB_46_f_ge_4 ?cvcl_81 ?cvcl_37) ?cvcl_10 ?cvcl_5) ?cvcl_1) ?cvcl_1)) ?cvcl_1) ?cvcl_10) $cvcl_99) ) ?cvcl_10 ?cvcl_5) ?cvcl_1))) (= ?cvcl_30 (ite (not (= ?cvcl_101 ?cvcl_1)) (ite (and (= ?cvcl_101 ?cvcl_10) (= (ite (or $cvcl_105  $cvcl_70 ) (ite $cvcl_105 (ite $cvcl_106 (ite $cvcl_107 ?cvcl_74 (ite $cvcl_108 ?cvcl_76 ?cvcl_1)) ?cvcl_1) (ite $cvcl_70 (ite (BmainB_46_f_ge_3 ?cvcl_38 ?cvcl_14) ?cvcl_10 ?cvcl_5) ?cvcl_1)) ?cvcl_1) ?cvcl_10)) ?cvcl_10 ?cvcl_5) ?cvcl_1))) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
)