(benchmark MULTIPLIER_PRIME_10.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))
  :extrapreds ((ARG2_LSBRCK_5_RSBRCK_))
  :extrafuns ((arg2_LSBRCK_5_RSBRCK_ Int))
  :extrapreds ((ARG2_LSBRCK_6_RSBRCK_))
  :extrafuns ((arg2_LSBRCK_6_RSBRCK_ Int))
  :extrapreds ((ARG2_LSBRCK_7_RSBRCK_))
  :extrafuns ((arg2_LSBRCK_7_RSBRCK_ Int))
  :extrapreds ((ARG2_LSBRCK_8_RSBRCK_))
  :extrafuns ((arg2_LSBRCK_8_RSBRCK_ Int))
  :extrapreds ((ARG2_LSBRCK_9_RSBRCK_))
  :extrafuns ((arg2_LSBRCK_9_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_LSBRCK_5_RSBRCK_ Int))
  :extrafuns ((mul_sum_LSBRCK_6_RSBRCK_ Int))
  :extrafuns ((mul_sum_LSBRCK_7_RSBRCK_ Int))
  :extrafuns ((mul_sum_LSBRCK_8_RSBRCK_ Int))
  :extrafuns ((mul_sum_LSBRCK_9_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_)) (flet ($cvcl_5 (not ARG2_LSBRCK_5_RSBRCK_)) (flet ($cvcl_6 (not ARG2_LSBRCK_6_RSBRCK_)) (flet ($cvcl_7 (not ARG2_LSBRCK_7_RSBRCK_)) (flet ($cvcl_8 (not ARG2_LSBRCK_8_RSBRCK_)) (flet ($cvcl_9 (not ARG2_LSBRCK_9_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 (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 1023)) (= (- (- (- (- (- (- (- (- (- (- 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_)) (* 32 arg2_LSBRCK_5_RSBRCK_)) (* 64 arg2_LSBRCK_6_RSBRCK_)) (* 128 arg2_LSBRCK_7_RSBRCK_)) (* 256 arg2_LSBRCK_8_RSBRCK_)) (* 512 arg2_LSBRCK_9_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) )) (>= arg2_LSBRCK_5_RSBRCK_ 0)) (<= arg2_LSBRCK_5_RSBRCK_ 1)) (or $cvcl_5  (= arg2_LSBRCK_5_RSBRCK_ 1) )) (or ARG2_LSBRCK_5_RSBRCK_  (= arg2_LSBRCK_5_RSBRCK_ 0) )) (>= arg2_LSBRCK_6_RSBRCK_ 0)) (<= arg2_LSBRCK_6_RSBRCK_ 1)) (or $cvcl_6  (= arg2_LSBRCK_6_RSBRCK_ 1) )) (or ARG2_LSBRCK_6_RSBRCK_  (= arg2_LSBRCK_6_RSBRCK_ 0) )) (>= arg2_LSBRCK_7_RSBRCK_ 0)) (<= arg2_LSBRCK_7_RSBRCK_ 1)) (or $cvcl_7  (= arg2_LSBRCK_7_RSBRCK_ 1) )) (or ARG2_LSBRCK_7_RSBRCK_  (= arg2_LSBRCK_7_RSBRCK_ 0) )) (>= arg2_LSBRCK_8_RSBRCK_ 0)) (<= arg2_LSBRCK_8_RSBRCK_ 1)) (or $cvcl_8  (= arg2_LSBRCK_8_RSBRCK_ 1) )) (or ARG2_LSBRCK_8_RSBRCK_  (= arg2_LSBRCK_8_RSBRCK_ 0) )) (>= arg2_LSBRCK_9_RSBRCK_ 0)) (<= arg2_LSBRCK_9_RSBRCK_ 1)) (or $cvcl_9  (= arg2_LSBRCK_9_RSBRCK_ 1) )) (or ARG2_LSBRCK_9_RSBRCK_  (= arg2_LSBRCK_9_RSBRCK_ 0) )) (>= mul_sum_LSBRCK_0_RSBRCK_ 0)) (<= mul_sum_LSBRCK_0_RSBRCK_ 1023)) (>= arg1 0)) (<= arg1 1023)) (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_ 1023)) (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_ 1023)) (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_ 1023)) (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_ 1023)) (or $cvcl_4  (= mul_sum_LSBRCK_4_RSBRCK_ arg1) )) (or ARG2_LSBRCK_4_RSBRCK_  (= mul_sum_LSBRCK_4_RSBRCK_ 0) )) (>= mul_sum_LSBRCK_5_RSBRCK_ 0)) (<= mul_sum_LSBRCK_5_RSBRCK_ 1023)) (or $cvcl_5  (= mul_sum_LSBRCK_5_RSBRCK_ arg1) )) (or ARG2_LSBRCK_5_RSBRCK_  (= mul_sum_LSBRCK_5_RSBRCK_ 0) )) (>= mul_sum_LSBRCK_6_RSBRCK_ 0)) (<= mul_sum_LSBRCK_6_RSBRCK_ 1023)) (or $cvcl_6  (= mul_sum_LSBRCK_6_RSBRCK_ arg1) )) (or ARG2_LSBRCK_6_RSBRCK_  (= mul_sum_LSBRCK_6_RSBRCK_ 0) )) (>= mul_sum_LSBRCK_7_RSBRCK_ 0)) (<= mul_sum_LSBRCK_7_RSBRCK_ 1023)) (or $cvcl_7  (= mul_sum_LSBRCK_7_RSBRCK_ arg1) )) (or ARG2_LSBRCK_7_RSBRCK_  (= mul_sum_LSBRCK_7_RSBRCK_ 0) )) (>= mul_sum_LSBRCK_8_RSBRCK_ 0)) (<= mul_sum_LSBRCK_8_RSBRCK_ 1023)) (or $cvcl_8  (= mul_sum_LSBRCK_8_RSBRCK_ arg1) )) (or ARG2_LSBRCK_8_RSBRCK_  (= mul_sum_LSBRCK_8_RSBRCK_ 0) )) (>= mul_sum_LSBRCK_9_RSBRCK_ 0)) (<= mul_sum_LSBRCK_9_RSBRCK_ 1023)) (or $cvcl_9  (= mul_sum_LSBRCK_9_RSBRCK_ arg1) )) (or ARG2_LSBRCK_9_RSBRCK_  (= mul_sum_LSBRCK_9_RSBRCK_ 0) )) (>= mul_sum 0)) (<= mul_sum 1048575)) (= (- (- (- (- (- (- (- (- (- (- 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_)) (* 32 mul_sum_LSBRCK_5_RSBRCK_)) (* 64 mul_sum_LSBRCK_6_RSBRCK_)) (* 128 mul_sum_LSBRCK_7_RSBRCK_)) (* 256 mul_sum_LSBRCK_8_RSBRCK_)) (* 512 mul_sum_LSBRCK_9_RSBRCK_)) 0)) (>= mul 0)) (<= mul 1048575)) (= mul mul_sum)) (= mul 1042441))))))))))))
)