(benchmark B_32s.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_T4_c Int))
  :extrafuns ((BmainB_46_init_const_zPTC_b_676_c Int))
  :extrafuns ((BmainB_46_init_const_N1_c Int))
  :extrafuns ((BmainB_46_init_const_PITCH_c Int))
  :extrafuns ((BmainB_46_init_const_PITCH_650_c Int))
  :extrapreds ((BB_p0))
  :extrafuns ((BmainB_46_init_const_N1_643_c Int))
  :extrafuns ((BmainB_46_init_const_H_s_680_c Int))
  :extrafuns ((BmainB_46_init_const_s_680_c Int))
  :extrafuns ((BmainB_46_init_const_H_zPTC_b_676_c Int))
  :extrafuns ((BmainB_46_iBOT Int))
  :extrafuns ((BmainB_46_init_const_T4_645_c Int))
  :extrafuns ((BmainB_46_f_minus_1 Int Int Int))
  :extrafuns ((BmainB_46_f_minus_2 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_ge_1 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_8 (+ 1 ?cvcl_1)) (let (?cvcl_9 (+ 1 ?cvcl_8)) (let (?cvcl_0 (+ 1 ?cvcl_9)) (let (?cvcl_3 (+ 1 ?cvcl_0)) (let (?cvcl_2 (+ 1 ?cvcl_3)) (let (?cvcl_4 (BmainB_46_f_div_1 ?cvcl_2 ?cvcl_0)) (let (?cvcl_11 (+ 1 ?cvcl_2)) (let (?cvcl_39 (+ 1 ?cvcl_11)) (let (?cvcl_29 (BmainB_46_f_minus_1 ?cvcl_39 ?cvcl_3)) (let (?cvcl_5 BmainB_46_init_const_H_s_680_c) (let (?cvcl_15 (BmainB_46_f_plus_1 ?cvcl_5 ?cvcl_4)) (flet ($cvcl_7 (not (= ?cvcl_15 ?cvcl_1))) (let (?cvcl_14 (BmainB_46_f_minus_2 ?cvcl_5 ?cvcl_4)) (flet ($cvcl_6 (not (= ?cvcl_14 ?cvcl_1))) (let (?cvcl_10 BmainB_46_init_const_s_680_c) (flet ($cvcl_66 (not (= ?cvcl_5 ?cvcl_1))) (let (?cvcl_20 BmainB_46_init_const_T4_645_c) (let (?cvcl_22 BmainB_46_init_const_N1_643_c) (let (?cvcl_19 BmainB_46_init_const_T4_c) (let (?cvcl_21 BmainB_46_init_const_N1_c) (flet ($cvcl_27 (not (= ?cvcl_21 ?cvcl_1))) (let (?cvcl_23 BmainB_46_init_const_PITCH_c) (flet ($cvcl_62 (not (= ?cvcl_23 ?cvcl_1))) (let (?cvcl_24 BmainB_46_init_const_zPTC_b_676_c) (let (?cvcl_16 BmainB_46_init_const_H_zPTC_b_676_c) (flet ($cvcl_75 (not (= ?cvcl_16 ?cvcl_1))) (let (?cvcl_13 BmainB_46_init_const_PITCH_650_c) (let (?cvcl_25 (ite BB_p0 ?cvcl_8 ?cvcl_9)) (flet ($cvcl_12 (= ?cvcl_25 ?cvcl_9)) (let (?cvcl_17 (ite $cvcl_12 (ite $cvcl_12 (ite $cvcl_12 ?cvcl_13 (ite $cvcl_12 ?cvcl_14 ?cvcl_1)) (ite $cvcl_12 ?cvcl_15 ?cvcl_1)) ?cvcl_16)) (let (?cvcl_18 (ite (BmainB_46_f_lt_2 ?cvcl_11 ?cvcl_17) ?cvcl_11 ?cvcl_17)) (flet ($cvcl_26 (not (= ?cvcl_25 ?cvcl_1))) (flet ($cvcl_28 (and $cvcl_12 $cvcl_27)) (flet ($cvcl_30 (or $cvcl_28  $cvcl_26 )) (let (?cvcl_31 (ite $cvcl_30 (ite (= (ite $cvcl_28 (ite (BmainB_46_f_lt_1 ?cvcl_21 ?cvcl_29) ?cvcl_9 ?cvcl_8) ?cvcl_1) ?cvcl_9) ?cvcl_9 (ite $cvcl_30 ?cvcl_8 ?cvcl_1)) ?cvcl_1)) (flet ($cvcl_36 (and $cvcl_12 (= ?cvcl_31 ?cvcl_9))) (flet ($cvcl_37 (and $cvcl_12 (= ?cvcl_31 ?cvcl_8))) (flet ($cvcl_35 (or $cvcl_36  $cvcl_37 )) (flet ($cvcl_73 (not (= ?cvcl_9 ?cvcl_1))) (flet ($cvcl_32 (or $cvcl_26  $cvcl_73 )) (let (?cvcl_33 (ite $cvcl_32 (ite (= (ite $cvcl_26 ?cvcl_25 ?cvcl_1) ?cvcl_9) ?cvcl_9 (ite $cvcl_32 ?cvcl_8 ?cvcl_1)) ?cvcl_1)) (flet ($cvcl_34 (and $cvcl_35 (= ?cvcl_33 ?cvcl_9))) (flet ($cvcl_38 (and $cvcl_27 (= ?cvcl_33 ?cvcl_8))) (let (?cvcl_40 (ite (or $cvcl_34  $cvcl_38 ) (ite $cvcl_34 (ite $cvcl_35 (ite $cvcl_36 (ite $cvcl_12 (ite $cvcl_12 ?cvcl_8 ?cvcl_1) ?cvcl_1) (ite $cvcl_37 (ite $cvcl_12 (ite $cvcl_12 ?cvcl_9 ?cvcl_1) ?cvcl_1) ?cvcl_1)) ?cvcl_1) (ite $cvcl_38 (ite $cvcl_27 (ite (BmainB_46_f_ge_1 ?cvcl_21 ?cvcl_39) ?cvcl_9 ?cvcl_8) ?cvcl_1) ?cvcl_1)) ?cvcl_1)) (let (?cvcl_41 (ite $cvcl_26 (ite (or $cvcl_12  (= (ite $cvcl_26 (ite (and $cvcl_12 (= (ite (not (= ?cvcl_40 ?cvcl_1)) (ite (= ?cvcl_40 ?cvcl_8) ?cvcl_9 ?cvcl_8) ?cvcl_1) ?cvcl_9)) ?cvcl_9 ?cvcl_8) ?cvcl_1) ?cvcl_9) ) ?cvcl_9 ?cvcl_8) ?cvcl_1)) (flet ($cvcl_44 (= ?cvcl_40 ?cvcl_9)) (flet ($cvcl_53 (and $cvcl_12 $cvcl_44)) (let (?cvcl_42 (ite (not (= ?cvcl_41 ?cvcl_1)) (ite (or (= ?cvcl_41 ?cvcl_9)  (= (ite $cvcl_26 (ite $cvcl_53 ?cvcl_9 ?cvcl_8) ?cvcl_1) ?cvcl_9) ) ?cvcl_9 ?cvcl_8) ?cvcl_1)) (let (?cvcl_43 (ite (not (= ?cvcl_42 ?cvcl_1)) (ite (= ?cvcl_42 ?cvcl_9) ?cvcl_41 ?cvcl_25) ?cvcl_1)) (flet ($cvcl_63 (not (= ?cvcl_43 ?cvcl_1))) (flet ($cvcl_48 (= ?cvcl_25 ?cvcl_8)) (flet ($cvcl_49 (= (ite $cvcl_26 (ite $cvcl_48 ?cvcl_9 ?cvcl_8) ?cvcl_1) ?cvcl_9)) (flet ($cvcl_46 (= (ite $cvcl_26 (ite (and $cvcl_12 $cvcl_49) ?cvcl_9 ?cvcl_8) ?cvcl_1) ?cvcl_9)) (let (?cvcl_45 (ite $cvcl_26 (ite (and $cvcl_12 (and $cvcl_46 $cvcl_44)) ?cvcl_9 ?cvcl_8) ?cvcl_1)) (let (?cvcl_57 (ite $cvcl_26 (ite (and $cvcl_12 $cvcl_46) ?cvcl_9 ?cvcl_8) ?cvcl_1)) (flet ($cvcl_58 (= ?cvcl_57 ?cvcl_9)) (let (?cvcl_47 (ite (not (= ?cvcl_45 ?cvcl_1)) (ite (or (= ?cvcl_45 ?cvcl_9)  $cvcl_58 ) ?cvcl_9 ?cvcl_8) ?cvcl_1)) (let (?cvcl_50 (ite $cvcl_26 (ite (and $cvcl_12 (= (ite $cvcl_26 (ite (and $cvcl_48 $cvcl_49) ?cvcl_9 ?cvcl_8) ?cvcl_1) ?cvcl_9)) ?cvcl_9 ?cvcl_8) ?cvcl_1)) (flet ($cvcl_59 (= ?cvcl_50 ?cvcl_9)) (flet ($cvcl_55 (= (ite $cvcl_26 (ite $cvcl_12 ?cvcl_9 ?cvcl_8) ?cvcl_1) ?cvcl_9)) (let (?cvcl_51 (ite (not (= ?cvcl_47 ?cvcl_1)) (ite (or (= ?cvcl_47 ?cvcl_9)  (= (ite (not (= ?cvcl_50 ?cvcl_1)) (ite (or $cvcl_59  $cvcl_55 ) ?cvcl_9 ?cvcl_8) ?cvcl_1) ?cvcl_9) ) ?cvcl_9 ?cvcl_8) ?cvcl_1)) (let (?cvcl_52 (ite $cvcl_63 (ite (or (= ?cvcl_43 ?cvcl_9)  (= (ite (not (= ?cvcl_51 ?cvcl_1)) (ite (= ?cvcl_51 ?cvcl_9) ?cvcl_47 ?cvcl_25) ?cvcl_1) ?cvcl_9) ) ?cvcl_9 ?cvcl_8) ?cvcl_1)) (flet ($cvcl_64 (not (= ?cvcl_52 ?cvcl_1))) (flet ($cvcl_61 (= ?cvcl_52 ?cvcl_9)) (let (?cvcl_54 (ite $cvcl_26 (ite (and $cvcl_12 $cvcl_53) ?cvcl_9 ?cvcl_8) ?cvcl_1)) (let (?cvcl_56 (ite (not (= ?cvcl_54 ?cvcl_1)) (ite (or (= ?cvcl_54 ?cvcl_9)  $cvcl_55 ) ?cvcl_9 ?cvcl_8) ?cvcl_1)) (let (?cvcl_60 (ite (not (= ?cvcl_56 ?cvcl_1)) (ite (or (= ?cvcl_56 ?cvcl_9)  (= (ite (not (= ?cvcl_57 ?cvcl_1)) (ite (or $cvcl_58  $cvcl_59 ) ?cvcl_9 ?cvcl_8) ?cvcl_1) ?cvcl_9) ) ?cvcl_9 ?cvcl_8) ?cvcl_1)) (let (?cvcl_68 (ite $cvcl_64 (ite (or $cvcl_61  (= (ite (not (= ?cvcl_60 ?cvcl_1)) (ite (= ?cvcl_60 ?cvcl_9) ?cvcl_56 ?cvcl_25) ?cvcl_1) ?cvcl_9) ) ?cvcl_9 ?cvcl_8) ?cvcl_1)) (flet ($cvcl_70 (= ?cvcl_68 ?cvcl_9)) (flet ($cvcl_82 (and $cvcl_61 $cvcl_62)) (flet ($cvcl_65 (or $cvcl_63  $cvcl_64 )) (let (?cvcl_67 (ite $cvcl_65 (ite (= (ite $cvcl_63 ?cvcl_43 ?cvcl_1) ?cvcl_9) ?cvcl_9 (ite $cvcl_65 ?cvcl_8 ?cvcl_1)) ?cvcl_1)) (flet ($cvcl_81 (and $cvcl_82 (= ?cvcl_67 ?cvcl_9))) (flet ($cvcl_84 (and $cvcl_61 $cvcl_66)) (flet ($cvcl_83 (and $cvcl_84 (= ?cvcl_67 ?cvcl_8))) (flet ($cvcl_80 (and $cvcl_70 (or $cvcl_81  $cvcl_83 ))) (flet ($cvcl_72 (not (= ?cvcl_68 ?cvcl_1))) (flet ($cvcl_69 (or $cvcl_64  $cvcl_72 )) (let (?cvcl_71 (ite $cvcl_69 (ite (= (ite $cvcl_64 ?cvcl_52 ?cvcl_1) ?cvcl_9) ?cvcl_9 (ite $cvcl_69 ?cvcl_8 ?cvcl_1)) ?cvcl_1)) (flet ($cvcl_79 (and $cvcl_80 (= ?cvcl_71 ?cvcl_9))) (flet ($cvcl_86 (and $cvcl_70 $cvcl_66)) (flet ($cvcl_85 (and $cvcl_86 (= ?cvcl_71 ?cvcl_8))) (flet ($cvcl_78 (or $cvcl_79  $cvcl_85 )) (flet ($cvcl_74 (or $cvcl_72  $cvcl_73 )) (let (?cvcl_76 (ite $cvcl_74 (ite (= (ite $cvcl_72 ?cvcl_68 ?cvcl_1) ?cvcl_9) ?cvcl_9 (ite $cvcl_74 ?cvcl_8 ?cvcl_1)) ?cvcl_1)) (flet ($cvcl_77 (and $cvcl_78 (= ?cvcl_76 ?cvcl_9))) (flet ($cvcl_87 (and $cvcl_75 (= ?cvcl_76 ?cvcl_8))) (let (?cvcl_88 (ite (or $cvcl_77  $cvcl_87 ) (ite $cvcl_77 (ite $cvcl_78 (ite $cvcl_79 (ite $cvcl_80 (ite $cvcl_70 (ite $cvcl_81 (ite $cvcl_82 (ite $cvcl_61 ?cvcl_23 ?cvcl_1) ?cvcl_1) (ite $cvcl_83 (ite $cvcl_84 (ite $cvcl_61 ?cvcl_14 ?cvcl_1) ?cvcl_1) ?cvcl_1)) ?cvcl_1) ?cvcl_1) (ite $cvcl_85 (ite $cvcl_86 (ite $cvcl_70 ?cvcl_15 ?cvcl_1) ?cvcl_1) ?cvcl_1)) ?cvcl_1) (ite $cvcl_87 (ite $cvcl_75 ?cvcl_16 ?cvcl_1) ?cvcl_1)) ?cvcl_1)) (let (?cvcl_89 (ite (BmainB_46_f_lt_2 ?cvcl_11 ?cvcl_88) ?cvcl_11 ?cvcl_88)) (let (?cvcl_90 (ite (not (= ?cvcl_89 ?cvcl_1)) (ite (BmainB_46_f_lt_3 ?cvcl_89 ?cvcl_8) ?cvcl_8 ?cvcl_89) ?cvcl_1)) (flet ($cvcl_91 (not (= ?cvcl_90 ?cvcl_1))) (not (or (not (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?cvcl_4 ?cvcl_1)) (not (= ?cvcl_29 ?cvcl_1))) $cvcl_7) $cvcl_6) $cvcl_6) $cvcl_7) (not (= ?cvcl_10 ?cvcl_1))) $cvcl_66) (not (= ?cvcl_20 ?cvcl_1))) (not (= ?cvcl_22 ?cvcl_1))) (not (= ?cvcl_19 ?cvcl_1))) $cvcl_27) $cvcl_62) (not (= ?cvcl_24 ?cvcl_1))) $cvcl_75) (not (= ?cvcl_13 ?cvcl_1))) (and (and (and (and (and (and $cvcl_12 (= ?cvcl_10 (ite (BmainB_46_f_lt_3 ?cvcl_18 ?cvcl_8) ?cvcl_8 ?cvcl_18))) (= ?cvcl_5 ?cvcl_10)) (= ?cvcl_19 ?cvcl_20)) (= ?cvcl_21 ?cvcl_22)) (= ?cvcl_23 ?cvcl_13)) (= ?cvcl_16 ?cvcl_24))))  (and (and (= ?cvcl_10 (ite $cvcl_91 ?cvcl_90 ?cvcl_10)) (= ?cvcl_5 (ite $cvcl_91 ?cvcl_10 ?cvcl_1))) $cvcl_12) ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
)