(benchmark MULTIPLIER_PRIME_5.msat.smt
  :source {
Mathsat benchmarks available from http://mathsat.itc.it

This benchmark was automatically translated into SMT-LIB format from
CVC format using CVC Lite
}
  :status unknown
  :logic QF_LIA
  :extrafuns ((arg1 Int))
  :extrapreds ((ARG2_LSBRCK_0_RSBRCK_))
  :extrafuns ((arg2_LSBRCK_0_RSBRCK_ Int))
  :extrapreds ((ARG2_LSBRCK_1_RSBRCK_))
  :extrafuns ((arg2_LSBRCK_1_RSBRCK_ Int))
  :extrapreds ((ARG2_LSBRCK_2_RSBRCK_))
  :extrafuns ((arg2_LSBRCK_2_RSBRCK_ Int))
  :extrapreds ((ARG2_LSBRCK_3_RSBRCK_))
  :extrafuns ((arg2_LSBRCK_3_RSBRCK_ Int))
  :extrapreds ((ARG2_LSBRCK_4_RSBRCK_))
  :extrafuns ((arg2_LSBRCK_4_RSBRCK_ Int))
  :extrafuns ((arg2 Int))
  :extrafuns ((mul Int))
  :extrafuns ((mul_sum_LSBRCK_0_RSBRCK_ Int))
  :extrafuns ((mul_sum_LSBRCK_1_RSBRCK_ Int))
  :extrafuns ((mul_sum_LSBRCK_2_RSBRCK_ Int))
  :extrafuns ((mul_sum_LSBRCK_3_RSBRCK_ Int))
  :extrafuns ((mul_sum_LSBRCK_4_RSBRCK_ Int))
  :extrafuns ((mul_sum Int))
  :formula
(flet ($cvcl_0 (not ARG2_LSBRCK_0_RSBRCK_)) (flet ($cvcl_1 (not ARG2_LSBRCK_1_RSBRCK_)) (flet ($cvcl_2 (not ARG2_LSBRCK_2_RSBRCK_)) (flet ($cvcl_3 (not ARG2_LSBRCK_3_RSBRCK_)) (flet ($cvcl_4 (not ARG2_LSBRCK_4_RSBRCK_)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (>= arg2 0) (<= arg2 31)) (= (- (- (- (- (- arg2 arg2_LSBRCK_0_RSBRCK_) (* 2 arg2_LSBRCK_1_RSBRCK_)) (* 4 arg2_LSBRCK_2_RSBRCK_)) (* 8 arg2_LSBRCK_3_RSBRCK_)) (* 16 arg2_LSBRCK_4_RSBRCK_)) 0)) (>= arg2_LSBRCK_0_RSBRCK_ 0)) (<= arg2_LSBRCK_0_RSBRCK_ 1)) (or $cvcl_0  (= arg2_LSBRCK_0_RSBRCK_ 1) )) (or ARG2_LSBRCK_0_RSBRCK_  (= arg2_LSBRCK_0_RSBRCK_ 0) )) (>= arg2_LSBRCK_1_RSBRCK_ 0)) (<= arg2_LSBRCK_1_RSBRCK_ 1)) (or $cvcl_1  (= arg2_LSBRCK_1_RSBRCK_ 1) )) (or ARG2_LSBRCK_1_RSBRCK_  (= arg2_LSBRCK_1_RSBRCK_ 0) )) (>= arg2_LSBRCK_2_RSBRCK_ 0)) (<= arg2_LSBRCK_2_RSBRCK_ 1)) (or $cvcl_2  (= arg2_LSBRCK_2_RSBRCK_ 1) )) (or ARG2_LSBRCK_2_RSBRCK_  (= arg2_LSBRCK_2_RSBRCK_ 0) )) (>= arg2_LSBRCK_3_RSBRCK_ 0)) (<= arg2_LSBRCK_3_RSBRCK_ 1)) (or $cvcl_3  (= arg2_LSBRCK_3_RSBRCK_ 1) )) (or ARG2_LSBRCK_3_RSBRCK_  (= arg2_LSBRCK_3_RSBRCK_ 0) )) (>= arg2_LSBRCK_4_RSBRCK_ 0)) (<= arg2_LSBRCK_4_RSBRCK_ 1)) (or $cvcl_4  (= arg2_LSBRCK_4_RSBRCK_ 1) )) (or ARG2_LSBRCK_4_RSBRCK_  (= arg2_LSBRCK_4_RSBRCK_ 0) )) (>= mul_sum_LSBRCK_0_RSBRCK_ 0)) (<= mul_sum_LSBRCK_0_RSBRCK_ 31)) (>= arg1 0)) (<= arg1 31)) (or $cvcl_0  (= mul_sum_LSBRCK_0_RSBRCK_ arg1) )) (or ARG2_LSBRCK_0_RSBRCK_  (= mul_sum_LSBRCK_0_RSBRCK_ 0) )) (>= mul_sum_LSBRCK_1_RSBRCK_ 0)) (<= mul_sum_LSBRCK_1_RSBRCK_ 31)) (or $cvcl_1  (= mul_sum_LSBRCK_1_RSBRCK_ arg1) )) (or ARG2_LSBRCK_1_RSBRCK_  (= mul_sum_LSBRCK_1_RSBRCK_ 0) )) (>= mul_sum_LSBRCK_2_RSBRCK_ 0)) (<= mul_sum_LSBRCK_2_RSBRCK_ 31)) (or $cvcl_2  (= mul_sum_LSBRCK_2_RSBRCK_ arg1) )) (or ARG2_LSBRCK_2_RSBRCK_  (= mul_sum_LSBRCK_2_RSBRCK_ 0) )) (>= mul_sum_LSBRCK_3_RSBRCK_ 0)) (<= mul_sum_LSBRCK_3_RSBRCK_ 31)) (or $cvcl_3  (= mul_sum_LSBRCK_3_RSBRCK_ arg1) )) (or ARG2_LSBRCK_3_RSBRCK_  (= mul_sum_LSBRCK_3_RSBRCK_ 0) )) (>= mul_sum_LSBRCK_4_RSBRCK_ 0)) (<= mul_sum_LSBRCK_4_RSBRCK_ 31)) (or $cvcl_4  (= mul_sum_LSBRCK_4_RSBRCK_ arg1) )) (or ARG2_LSBRCK_4_RSBRCK_  (= mul_sum_LSBRCK_4_RSBRCK_ 0) )) (>= mul_sum 0)) (<= mul_sum 1023)) (= (- (- (- (- (- mul_sum mul_sum_LSBRCK_0_RSBRCK_) (* 2 mul_sum_LSBRCK_1_RSBRCK_)) (* 4 mul_sum_LSBRCK_2_RSBRCK_)) (* 8 mul_sum_LSBRCK_3_RSBRCK_)) (* 16 mul_sum_LSBRCK_4_RSBRCK_)) 0)) (>= mul 0)) (<= mul 1023)) (= mul mul_sum)) (= mul 961)))))))
)