slow.smt2

;;; generated by SMT-LIB2 driver
;;; SMT-LIB2 driver: bit-vectors, common part
;;; SMT-LIB2: integer arithmetic
;;; SMT-LIB2: real arithmetic
(declare-sort uni 0)

(declare-sort ty 0)

(declare-fun sort (ty uni) Bool)

(declare-fun witness (ty) uni)

;; witness_sort
  (assert (forall ((a ty)) (sort a (witness a))))

(declare-fun int () ty)

(declare-fun real () ty)

(declare-fun bool () ty)

(declare-fun match_bool (ty Bool uni uni) uni)

;; match_bool_sort
  (assert
  (forall ((a ty))
  (forall ((x Bool) (x1 uni) (x2 uni)) (sort a (match_bool a x x1 x2)))))

;; match_bool_True
  (assert
  (forall ((a ty))
  (forall ((z uni) (z1 uni)) (=> (sort a z) (= (match_bool a true z z1) z)))))

;; match_bool_False
  (assert
  (forall ((a ty))
  (forall ((z uni) (z1 uni))
  (=> (sort a z1) (= (match_bool a false z z1) z1)))))

(declare-fun index_bool (Bool) Int)

;; index_bool_True
  (assert (= (index_bool true) 0))

;; index_bool_False
  (assert (= (index_bool false) 1))

(declare-fun tuple0 () ty)

(declare-fun Tuple0 () uni)

;; Tuple0_sort
  (assert (sort tuple0 Tuple0))

(declare-fun qtmark () ty)

(declare-fun ref (ty) ty)

(declare-fun mk_ref (ty uni) uni)

;; mk ref_sort
  (assert (forall ((a ty)) (forall ((x uni)) (sort (ref a) (mk_ref a x)))))

(declare-fun contents (ty uni) uni)

;; contents_sort
  (assert (forall ((a ty)) (forall ((x uni)) (sort a (contents a x)))))

;; contents_def
  (assert
  (forall ((a ty))
  (forall ((u uni)) (=> (sort a u) (= (contents a (mk_ref a u)) u)))))

(declare-fun us__ignore (ty uni) uni)

;; ___ignore_sort
  (assert
  (forall ((a ty)) (forall ((x uni)) (sort tuple0 (us__ignore a x)))))

(declare-fun us_private () ty)

(declare-fun us_null_ext__ () uni)

;; __null_ext___sort
  (assert (sort us_private us_null_ext__))

(declare-fun us_type_of_heap () ty)

(declare-fun us_image () ty)

(declare-fun power (Real Int) Real)

;; Power_0
  (assert (forall ((x Real)) (= (power x 0) 1.0)))

;; Power_s
  (assert
  (forall ((x Real) (n Int))
  (=> (<= 0 n) (= (power x (+ n 1)) (* x (power x n))))))

;; Power_s_alt
  (assert
  (forall ((x Real) (n Int))
  (=> (< 0 n) (= (power x n) (* x (power x (- n 1)))))))

;; Power_1
  (assert (forall ((x Real)) (= (power x 1) x)))

;; Power_sum
  (assert
  (forall ((x Real) (n Int) (m Int))
  (=> (<= 0 n)
  (=> (<= 0 m) (= (power x (+ n m)) (* (power x n) (power x m)))))))

;; Power_mult
  (assert
  (forall ((x Real) (n Int) (m Int))
  (=> (<= 0 n) (=> (<= 0 m) (= (power x (* n m)) (power (power x n) m))))))

;; Power_mult2
  (assert
  (forall ((x Real) (y Real) (n Int))
  (=> (<= 0 n) (= (power (* x y) n) (* (power x n) (power y n))))))

;; Pow_ge_one
  (assert
  (forall ((x Real) (n Int))
  (=> (and (<= 0 n) (<= 1.0 x)) (<= 1.0 (power x n)))))

(declare-sort mode 0)

(declare-fun mode1 () ty)

(declare-fun NearestTiesToEven () mode)

(declare-fun ToZero () mode)

(declare-fun Up () mode)

(declare-fun Down () mode)

(declare-fun NearestTiesToAway () mode)

(declare-fun match_mode (ty mode uni uni uni uni uni) uni)

;; match_mode_sort
  (assert
  (forall ((a ty))
  (forall ((x mode) (x1 uni) (x2 uni) (x3 uni) (x4 uni) (x5 uni)) (sort a
  (match_mode a x x1 x2 x3 x4 x5)))))

;; match_mode_NearestTiesToEven
  (assert
  (forall ((a ty))
  (forall ((z uni) (z1 uni) (z2 uni) (z3 uni) (z4 uni))
  (=> (sort a z) (= (match_mode a NearestTiesToEven z z1 z2 z3 z4) z)))))

;; match_mode_ToZero
  (assert
  (forall ((a ty))
  (forall ((z uni) (z1 uni) (z2 uni) (z3 uni) (z4 uni))
  (=> (sort a z1) (= (match_mode a ToZero z z1 z2 z3 z4) z1)))))

;; match_mode_Up
  (assert
  (forall ((a ty))
  (forall ((z uni) (z1 uni) (z2 uni) (z3 uni) (z4 uni))
  (=> (sort a z2) (= (match_mode a Up z z1 z2 z3 z4) z2)))))

;; match_mode_Down
  (assert
  (forall ((a ty))
  (forall ((z uni) (z1 uni) (z2 uni) (z3 uni) (z4 uni))
  (=> (sort a z3) (= (match_mode a Down z z1 z2 z3 z4) z3)))))

;; match_mode_NearestTiesToAway
  (assert
  (forall ((a ty))
  (forall ((z uni) (z1 uni) (z2 uni) (z3 uni) (z4 uni))
  (=> (sort a z4) (= (match_mode a NearestTiesToAway z z1 z2 z3 z4) z4)))))

(declare-fun index_mode (mode) Int)

;; index_mode_NearestTiesToEven
  (assert (= (index_mode NearestTiesToEven) 0))

;; index_mode_ToZero
  (assert (= (index_mode ToZero) 1))

;; index_mode_Up
  (assert (= (index_mode Up) 2))

;; index_mode_Down
  (assert (= (index_mode Down) 3))

;; index_mode_NearestTiesToAway
  (assert (= (index_mode NearestTiesToAway) 4))

(declare-sort single 0)

(declare-fun single1 () ty)

(declare-fun round (mode Real) Real)

(declare-fun value (single) Real)

(declare-fun exact (single) Real)

(declare-fun model (single) Real)

(declare-fun round_error (single) Real)

;; round_error_def
  (assert
  (forall ((x single))
  (! (= (round_error x) (ite (>= (- (value x) (exact x)) 0.0) (- (value x) 
  (exact x)) (- (- (value x) (exact x))))) :pattern ((round_error x)) )))

(declare-fun total_error (single) Real)

;; total_error_def
  (assert
  (forall ((x single))
  (! (= (total_error x) (ite (>= (- (value x) (model x)) 0.0) (- (value x) 
  (model x)) (- (- (value x) (model x))))) :pattern ((total_error x)) )))

(declare-fun no_overflow (mode Real) Bool)

;; no_overflow_def
  (assert
  (forall ((m mode) (x Real))
  (! (= (no_overflow m x)
     (<= (ite (>= (round m x) 0.0) (round m x) (- (round m x))) 340282346638528859811704183484516925440.0)) :pattern ((no_overflow
  m x)) )))

;; Bounded_real_no_overflow
  (assert
  (forall ((m mode) (x Real))
  (=> (<= (ite (>= x 0.0) x (- x)) 340282346638528859811704183484516925440.0)
  (no_overflow m x))))

;; Round_monotonic
  (assert
  (forall ((m mode) (x Real) (y Real))
  (=> (<= x y) (<= (round m x) (round m y)))))

;; Round_idempotent
  (assert
  (forall ((m1 mode) (m2 mode) (x Real))
  (= (round m1 (round m2 x)) (round m2 x))))

;; Round_value
  (assert (forall ((m mode) (x single)) (= (round m (value x)) (value x))))

;; Bounded_value
  (assert
  (forall ((x single))
  (<= (ite (>= (value x) 0.0) (value x) (- (value x))) 340282346638528859811704183484516925440.0)))

;; Exact_rounding_for_integers
  (assert
  (forall ((m mode) (i4 Int))
  (=> (and (<= (- 16777216) i4) (<= i4 16777216))
  (= (round m (to_real i4)) (to_real i4)))))

;; Round_down_le
  (assert (forall ((x Real)) (<= (round Down x) x)))

;; Round_up_ge
  (assert (forall ((x Real)) (<= x (round Up x))))

;; Round_down_neg
  (assert (forall ((x Real)) (= (round Down (- x)) (- (round Up x)))))

;; Round_up_neg
  (assert (forall ((x Real)) (= (round Up (- x)) (- (round Down x)))))

(declare-fun round_logic (mode Real) single)

;; Round_logic_def
  (assert
  (forall ((m mode) (x Real))
  (=> (no_overflow m x) (= (value (round_logic m x)) (round m x)))))

(declare-fun of_real_post (mode Real single) Bool)

;; of_real_post_def
  (assert
  (forall ((m mode) (x Real) (res single))
  (! (= (of_real_post m x res)
     (and (= (value res) (round m x))
     (and (= (exact res) x) (= (model res) x)))) :pattern ((of_real_post
  m x res)) )))

(declare-fun add_post (mode single single single) Bool)

;; add_post_def
  (assert
  (forall ((m mode) (x single) (y single) (res single))
  (! (= (add_post m x y res)
     (and (= (value res) (round m (+ (value x) (value y))))
     (and (= (exact res) (+ (exact x) (exact y)))
     (= (model res) (+ (model x) (model y)))))) :pattern ((add_post
  m x y res)) )))

(declare-fun sub_post (mode single single single) Bool)

;; sub_post_def
  (assert
  (forall ((m mode) (x single) (y single) (res single))
  (! (= (sub_post m x y res)
     (and (= (value res) (round m (- (value x) (value y))))
     (and (= (exact res) (- (exact x) (exact y)))
     (= (model res) (- (model x) (model y)))))) :pattern ((sub_post
  m x y res)) )))

(declare-fun mul_post (mode single single single) Bool)

;; mul_post_def
  (assert
  (forall ((m mode) (x single) (y single) (res single))
  (! (= (mul_post m x y res)
     (and (= (value res) (round m (* (value x) (value y))))
     (and (= (exact res) (* (exact x) (exact y)))
     (= (model res) (* (model x) (model y)))))) :pattern ((mul_post
  m x y res)) )))

(declare-fun div_post (mode single single single) Bool)

;; div_post_def
  (assert
  (forall ((m mode) (x single) (y single) (res single))
  (! (= (div_post m x y res)
     (and (= (value res) (round m (/ (value x) (value y))))
     (and (= (exact res) (/ (exact x) (exact y)))
     (= (model res) (/ (model x) (model y)))))) :pattern ((div_post
  m x y res)) )))

(declare-fun neg_post (single single) Bool)

;; neg_post_def
  (assert
  (forall ((x single) (res single))
  (! (= (neg_post x res)
     (and (= (value res) (- (value x)))
     (and (= (exact res) (- (exact x))) (= (model res) (- (model x)))))) :pattern ((neg_post
  x res)) )))

(declare-fun lt (single single) Bool)

;; lt_def
  (assert
  (forall ((x single) (y single))
  (! (= (lt x y) (< (value x) (value y))) :pattern ((lt x y)) )))

(declare-fun gt (single single) Bool)

;; gt_def
  (assert
  (forall ((x single) (y single))
  (! (= (gt x y) (< (value y) (value x))) :pattern ((gt x y)) )))

(declare-sort double 0)

(declare-fun double1 () ty)

(declare-fun round1 (mode Real) Real)

(declare-fun value1 (double) Real)

(declare-fun exact1 (double) Real)

(declare-fun model1 (double) Real)

(declare-fun round_error1 (double) Real)

;; round_error_def
  (assert
  (forall ((x double))
  (! (= (round_error1 x) (ite (>= (- (value1 x) (exact1 x)) 0.0) (- (value1
                                                                    x) 
  (exact1 x)) (- (- (value1 x) (exact1 x))))) :pattern ((round_error1 x)) )))

(declare-fun total_error1 (double) Real)

;; total_error_def
  (assert
  (forall ((x double))
  (! (= (total_error1 x) (ite (>= (- (value1 x) (model1 x)) 0.0) (- (value1
                                                                    x) 
  (model1 x)) (- (- (value1 x) (model1 x))))) :pattern ((total_error1 x)) )))

(declare-fun no_overflow1 (mode Real) Bool)

;; no_overflow_def
  (assert
  (forall ((m mode) (x Real))
  (! (= (no_overflow1 m x)
     (<= (ite (>= (round1 m x) 0.0) (round1 m x) (- (round1 m x))) 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0)) :pattern ((no_overflow1
  m x)) )))

;; Bounded_real_no_overflow
  (assert
  (forall ((m mode) (x Real))
  (=>
  (<= (ite (>= x 0.0) x (- x)) 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0)
  (no_overflow1 m x))))

;; Round_monotonic
  (assert
  (forall ((m mode) (x Real) (y Real))
  (=> (<= x y) (<= (round1 m x) (round1 m y)))))

;; Round_idempotent
  (assert
  (forall ((m1 mode) (m2 mode) (x Real))
  (= (round1 m1 (round1 m2 x)) (round1 m2 x))))

;; Round_value
  (assert
  (forall ((m mode) (x double)) (= (round1 m (value1 x)) (value1 x))))

;; Bounded_value
  (assert
  (forall ((x double))
  (<= (ite (>= (value1 x) 0.0) (value1 x) (- (value1 x))) 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0)))

;; Exact_rounding_for_integers
  (assert
  (forall ((m mode) (i4 Int))
  (=> (and (<= (- 9007199254740992) i4) (<= i4 9007199254740992))
  (= (round1 m (to_real i4)) (to_real i4)))))

;; Round_down_le
  (assert (forall ((x Real)) (<= (round1 Down x) x)))

;; Round_up_ge
  (assert (forall ((x Real)) (<= x (round1 Up x))))

;; Round_down_neg
  (assert (forall ((x Real)) (= (round1 Down (- x)) (- (round1 Up x)))))

;; Round_up_neg
  (assert (forall ((x Real)) (= (round1 Up (- x)) (- (round1 Down x)))))

(declare-fun round_logic1 (mode Real) double)

;; Round_logic_def
  (assert
  (forall ((m mode) (x Real))
  (=> (no_overflow1 m x) (= (value1 (round_logic1 m x)) (round1 m x)))))

(declare-fun of_real_post1 (mode Real double) Bool)

;; of_real_post_def
  (assert
  (forall ((m mode) (x Real) (res double))
  (! (= (of_real_post1 m x res)
     (and (= (value1 res) (round1 m x))
     (and (= (exact1 res) x) (= (model1 res) x)))) :pattern ((of_real_post1
  m x res)) )))

(declare-fun add_post1 (mode double double double) Bool)

;; add_post_def
  (assert
  (forall ((m mode) (x double) (y double) (res double))
  (! (= (add_post1 m x y res)
     (and (= (value1 res) (round1 m (+ (value1 x) (value1 y))))
     (and (= (exact1 res) (+ (exact1 x) (exact1 y)))
     (= (model1 res) (+ (model1 x) (model1 y)))))) :pattern ((add_post1
  m x y res)) )))

(declare-fun sub_post1 (mode double double double) Bool)

;; sub_post_def
  (assert
  (forall ((m mode) (x double) (y double) (res double))
  (! (= (sub_post1 m x y res)
     (and (= (value1 res) (round1 m (- (value1 x) (value1 y))))
     (and (= (exact1 res) (- (exact1 x) (exact1 y)))
     (= (model1 res) (- (model1 x) (model1 y)))))) :pattern ((sub_post1
  m x y res)) )))

(declare-fun mul_post1 (mode double double double) Bool)

;; mul_post_def
  (assert
  (forall ((m mode) (x double) (y double) (res double))
  (! (= (mul_post1 m x y res)
     (and (= (value1 res) (round1 m (* (value1 x) (value1 y))))
     (and (= (exact1 res) (* (exact1 x) (exact1 y)))
     (= (model1 res) (* (model1 x) (model1 y)))))) :pattern ((mul_post1
  m x y res)) )))

(declare-fun div_post1 (mode double double double) Bool)

;; div_post_def
  (assert
  (forall ((m mode) (x double) (y double) (res double))
  (! (= (div_post1 m x y res)
     (and (= (value1 res) (round1 m (/ (value1 x) (value1 y))))
     (and (= (exact1 res) (/ (exact1 x) (exact1 y)))
     (= (model1 res) (/ (model1 x) (model1 y)))))) :pattern ((div_post1
  m x y res)) )))

(declare-fun neg_post1 (double double) Bool)

;; neg_post_def
  (assert
  (forall ((x double) (res double))
  (! (= (neg_post1 x res)
     (and (= (value1 res) (- (value1 x)))
     (and (= (exact1 res) (- (exact1 x))) (= (model1 res) (- (model1 x)))))) :pattern ((neg_post1
  x res)) )))

(declare-fun lt1 (double double) Bool)

;; lt_def
  (assert
  (forall ((x double) (y double))
  (! (= (lt1 x y) (< (value1 x) (value1 y))) :pattern ((lt1 x y)) )))

(declare-fun gt1 (double double) Bool)

;; gt_def
  (assert
  (forall ((x double) (y double))
  (! (= (gt1 x y) (< (value1 y) (value1 x))) :pattern ((gt1 x y)) )))

;; round_single_bound
  (assert
  (forall ((x Real))
  (! (and
     (<= (- (- x (* (/ 1.0 16777216.0) (ite (>= x 0.0) x (- x)))) (/ 1.0 1427247692705959881058285969449495136382746624.0)) 
     (round NearestTiesToEven x))
     (<= (round NearestTiesToEven x) (+ (+ x (* (/ 1.0 16777216.0) (ite (>= x 0.0) x (- x)))) (/ 1.0 1427247692705959881058285969449495136382746624.0)))) :pattern (
  (round NearestTiesToEven x)) )))

;; round_double_bound
  (assert
  (forall ((x Real))
  (! (and
     (<= (- (- x (* (/ 1.0 9007199254740992.0) (ite (>= x 0.0) x (- x)))) (/ 1.0 404804506614621236704990693437834614099113299528284236713802716054860679135990693783920767402874248990374155728633623822779617474771586953734026799881477019843034848553132722728933815484186432682479535356945490137124014966849385397236206711298319112681620113024717539104666829230461005064372655017292012526615415482186989568.0)) 
     (round1 NearestTiesToEven x))
     (<= (round1 NearestTiesToEven x) (+ (+ x (* (/ 1.0 9007199254740992.0) (ite (>= x 0.0) x (- x)))) (/ 1.0 404804506614621236704990693437834614099113299528284236713802716054860679135990693783920767402874248990374155728633623822779617474771586953734026799881477019843034848553132722728933815484186432682479535356945490137124014966849385397236206711298319112681620113024717539104666829230461005064372655017292012526615415482186989568.0)))) :pattern (
  (round1 NearestTiesToEven x)) )))

;; round_double_single
  (assert
  (forall ((x Real))
  (! (= (round1 NearestTiesToEven (round NearestTiesToEven x)) (round
                                                               NearestTiesToEven
                                                               x)) :pattern (
  (round NearestTiesToEven x)) )))

(declare-fun bool_lt1 (Real Real) Bool)

(declare-fun bool_le1 (Real Real) Bool)

(declare-fun bool_gt1 (Real Real) Bool)

(declare-fun bool_ge1 (Real Real) Bool)

(declare-fun bool_eq4 (Real Real) Bool)

(declare-fun bool_neq (Real Real) Bool)

;; Bool_real__lt_axiom
  (assert
  (forall ((x Real)) (forall ((y Real)) (= (= (bool_lt1 x y) true) (< x y)))))

;; Bool_real__le_axiom
  (assert
  (forall ((x Real))
  (forall ((y Real)) (= (= (bool_le1 x y) true) (<= x y)))))

;; Bool_real__gt_axiom
  (assert
  (forall ((x Real)) (forall ((y Real)) (= (= (bool_gt1 x y) true) (< y x)))))

;; Bool_real__ge_axiom
  (assert
  (forall ((x Real))
  (forall ((y Real)) (= (= (bool_ge1 x y) true) (<= y x)))))

;; Bool_real__eq_axiom
  (assert
  (forall ((x Real)) (forall ((y Real)) (= (= (bool_eq4 x y) true) (= x y)))))

;; Bool_real__neq_axiom
  (assert
  (forall ((x Real))
  (forall ((y Real)) (= (= (bool_neq x y) true) (not (= x y))))))

(declare-fun round2 (Real) Int)

;; Round_down
  (assert
  (forall ((x Real))
  (=> (< (- x (to_real (to_int x))) (/ 5.0 10.0)) (= (round2 x) (to_int x)))))

;; Round_up
  (assert
  (forall ((x Real))
  (=> (< (- (to_real (- 1 (to_int (- 1.0 x)))) x) (/ 5.0 10.0))
  (= (round2 x) (- 1 (to_int (- 1.0 x)))))))

;; Round_neg_tie
  (assert
  (forall ((x Real))
  (=> (and (= (- x (to_real (to_int x))) (/ 5.0 10.0)) (< x 0.0))
  (= (round2 x) (to_int x)))))

;; Round_pos_tie
  (assert
  (forall ((x Real))
  (=>
  (and (= (- (to_real (- 1 (to_int (- 1.0 x)))) x) (/ 5.0 10.0)) (< 0.0 x))
  (= (round2 x) (- 1 (to_int (- 1.0 x)))))))

;; Round_int
  (assert
  (forall ((i4 Int))
  (! (= (round2 (to_real i4)) i4) :pattern ((round2 (to_real i4))) )))

;; Round_near_int
  (assert
  (forall ((i4 Int))
  (forall ((x Real))
  (=> (and (< (- (/ 5.0 10.0)) x) (< x (/ 5.0 10.0)))
  (= (round2 (+ (to_real i4) x)) i4)))))

;; Round_monotonic
  (assert
  (forall ((x Real) (y Real)) (=> (<= x y) (<= (round2 x) (round2 y)))))

;; Round_monotonic_int1
  (assert
  (forall ((x Real) (i4 Int)) (=> (<= x (to_real i4)) (<= (round2 x) i4))))

;; Round_monotonic_int2
  (assert
  (forall ((x Real) (i4 Int)) (=> (<= (to_real i4) x) (<= i4 (round2 x)))))

;; Round_bound
  (assert
  (forall ((x Real))
  (and (<= (- x (/ 5.0 10.0)) (to_real (round2 x)))
  (<= (to_real (round2 x)) (+ x (/ 5.0 10.0))))))

(declare-sort float 0)

(declare-fun float1 () ty)

(declare-fun in_range3 (Real) Bool)

;; in_range_def
  (assert
  (forall ((x Real))
  (! (= (in_range3 x)
     (and (<= (- 340282346638528859811704183484516925440.0) x)
     (<= x 340282346638528859811704183484516925440.0))) :pattern ((in_range3
  x)) )))

(declare-fun bool_eq5 (Real Real) Bool)

;; bool_eq_def
  (assert
  (forall ((x Real) (y Real))
  (! (ite (= x y) (= (bool_eq5 x y) true) (= (bool_eq5 x y) false)) :pattern (
  (bool_eq5 x y)) )))

(declare-fun to_real1 (float) Real)

(declare-fun of_real (Real) float)

(declare-fun user_eq2 (float float) Bool)

(declare-fun next_representable (Real) Real)

(declare-fun prev_representable (Real) Real)

;; next_representable_def
  (assert
  (forall ((x Real))
  (! (< x (next_representable x)) :pattern ((next_representable x)) )))

;; prev_representable_def
  (assert
  (forall ((x Real))
  (! (< (prev_representable x) x) :pattern ((prev_representable x)) )))

(declare-fun attr__ATTRIBUTE_IMAGE3 (Real) uni)

;; attr__ATTRIBUTE_IMAGE_sort
  (assert (forall ((x Real)) (sort us_image (attr__ATTRIBUTE_IMAGE3 x))))

(declare-fun attr__ATTRIBUTE_VALUE__pre_check3 (uni) Bool)

(declare-fun attr__ATTRIBUTE_VALUE3 (uni) Real)

(declare-fun dummy2 () float)

;; inversion_axiom
  (assert
  (forall ((x float))
  (! (= (of_real (to_real1 x)) x) :pattern ((to_real1 x)) )))

;; representable_first
  (assert
  (= (round NearestTiesToEven (- 340282346638528859811704183484516925440.0)) (- 340282346638528859811704183484516925440.0)))

;; representable_last
  (assert
  (= (round NearestTiesToEven 340282346638528859811704183484516925440.0) 340282346638528859811704183484516925440.0))

;; range_axiom
  (assert (forall ((x float)) (in_range3 (to_real1 x))))

(declare-sort tinteger_16B 0)

(declare-fun tinteger_16B1 () ty)

(declare-fun in_range11 (Int) Bool)

;; in_range_def
  (assert
  (forall ((x Int))
  (! (= (in_range11 x) (and (<= (- 32768) x) (<= x 32767))) :pattern ((in_range11
  x)) )))

(declare-fun bool_eq1 (Int Int) Bool)

(declare-fun bool_ne (Int Int) Bool)

(declare-fun bool_lt (Int Int) Bool)

(declare-fun bool_le (Int Int) Bool)

(declare-fun bool_gt (Int Int) Bool)

(declare-fun bool_ge (Int Int) Bool)

;; bool_eq_axiom
  (assert
  (forall ((x Int)) (forall ((y Int)) (= (= (bool_eq1 x y) true) (= x y)))))

;; bool_ne_axiom
  (assert
  (forall ((x Int))
  (forall ((y Int)) (= (= (bool_ne x y) true) (not (= x y))))))

;; bool_lt_axiom
  (assert
  (forall ((x Int)) (forall ((y Int)) (= (= (bool_lt x y) true) (< x y)))))

;; bool_int__le_axiom
  (assert
  (forall ((x Int)) (forall ((y Int)) (= (= (bool_le x y) true) (<= x y)))))

;; bool_gt_axiom
  (assert
  (forall ((x Int)) (forall ((y Int)) (= (= (bool_gt x y) true) (< y x)))))

;; bool_ge_axiom
  (assert
  (forall ((x Int)) (forall ((y Int)) (= (= (bool_ge x y) true) (<= y x)))))

(declare-fun bool_eq14 (Int Int) Bool)

;; bool_eq_def
  (assert
  (forall ((x Int) (y Int))
  (! (ite (= x y) (= (bool_eq14 x y) true) (= (bool_eq14 x y) false)) :pattern (
  (bool_eq14 x y)) )))

(declare-fun attr__ATTRIBUTE_IMAGE11 (Int) uni)

;; attr__ATTRIBUTE_IMAGE_sort
  (assert (forall ((x Int)) (sort us_image (attr__ATTRIBUTE_IMAGE11 x))))

(declare-fun attr__ATTRIBUTE_VALUE__pre_check11 (uni) Bool)

(declare-fun attr__ATTRIBUTE_VALUE11 (uni) Int)

(declare-fun to_rep8 (tinteger_16B) Int)

(declare-fun of_rep8 (Int) tinteger_16B)

(declare-fun user_eq10 (tinteger_16B tinteger_16B) Bool)

(declare-fun dummy10 () tinteger_16B)

;; inversion_axiom
  (assert
  (forall ((x tinteger_16B))
  (! (= (of_rep8 (to_rep8 x)) x) :pattern ((to_rep8 x)) )))

;; range_axiom
  (assert
  (forall ((x tinteger_16B)) (! (in_range11
  (to_rep8 x)) :pattern ((to_rep8 x)) )))

;; coerce_axiom
  (assert
  (forall ((x Int))
  (! (=> (in_range11 x) (= (to_rep8 (of_rep8 x)) x)) :pattern ((to_rep8
                                                               (of_rep8 x))) )))

(declare-sort integer_16 0)

(declare-fun integer_161 () ty)

(declare-fun in_range4 (Int) Bool)

;; in_range_def
  (assert
  (forall ((x Int))
  (! (= (in_range4 x) (and (<= (- 32768) x) (<= x 32767))) :pattern ((in_range4
  x)) )))

(declare-fun bool_eq6 (Int Int) Bool)

;; bool_eq_def
  (assert
  (forall ((x Int) (y Int))
  (! (ite (= x y) (= (bool_eq6 x y) true) (= (bool_eq6 x y) false)) :pattern (
  (bool_eq6 x y)) )))

(declare-fun attr__ATTRIBUTE_IMAGE4 (Int) uni)

;; attr__ATTRIBUTE_IMAGE_sort
  (assert (forall ((x Int)) (sort us_image (attr__ATTRIBUTE_IMAGE4 x))))

(declare-fun attr__ATTRIBUTE_VALUE__pre_check4 (uni) Bool)

(declare-fun attr__ATTRIBUTE_VALUE4 (uni) Int)

(declare-fun to_rep2 (integer_16) Int)

(declare-fun of_rep2 (Int) integer_16)

(declare-fun user_eq3 (integer_16 integer_16) Bool)

(declare-fun dummy3 () integer_16)

;; inversion_axiom
  (assert
  (forall ((x integer_16))
  (! (= (of_rep2 (to_rep2 x)) x) :pattern ((to_rep2 x)) )))

;; range_axiom
  (assert
  (forall ((x integer_16)) (! (in_range4
  (to_rep2 x)) :pattern ((to_rep2 x)) )))

;; coerce_axiom
  (assert
  (forall ((x Int))
  (! (=> (in_range4 x) (= (to_rep2 (of_rep2 x)) x)) :pattern ((to_rep2
                                                              (of_rep2 x))) )))

(declare-fun left9 () Int)

(declare-fun right9 () Int)

(assert
;; WP_parameter_def12
 ;; File "/tmp/tmp-test-N320-031__thales1_ada_flat-13302/src/gnatprove/simulink_functions/../simulink_functions.mlw", line 21726, characters 5-8
  (not
  (forall ((o Int) (o1 Int))
  (=> (and (in_range4 left9) (in_range4 right9))
  (=> (not (= right9 0))
  (=>
  (and
  (and
  (= o (to_int (round NearestTiesToEven
               (/ (round NearestTiesToEven (to_real left9)) (round
                                                            NearestTiesToEven
                                                            (to_real 
                                                            right9))))))
  (in_range4
  (to_int (round NearestTiesToEven
          (/ (round NearestTiesToEven (to_real left9)) (round
                                                       NearestTiesToEven
                                                       (to_real right9)))))))
  (= o1 (* o right9))) (in_range11 o1)))))))
(check-sat)