Skip to content

Instantly share code, notes, and snippets.

@kanigsson

kanigsson/crash.smt2

Created June 23, 2015 07:06
Show Gist options
  • Save kanigsson/bc38fe18e38604a22d8e to your computer and use it in GitHub Desktop.
Save kanigsson/bc38fe18e38604a22d8e to your computer and use it in GitHub Desktop.
Download ZIP
Raw
crash.smt2
;;; generated by SMT-LIB2 driver
;;; SMT-LIB2 driver: bit-vectors, common part
;;; SMT-LIB2: integer 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-sort ref1 1)
(declare-fun ref (ty) ty)
(declare-fun t2 () 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 mk_ref2 ((_ BitVec 64)) (ref1 (_ BitVec 64)))
(declare-fun contents (ty uni) uni)
;; contents_sort
(assert (forall ((a ty)) (forall ((x uni)) (sort a (contents a x)))))
(declare-fun t2tb7 ((ref1 (_ BitVec 64))) uni)
;; t2tb_sort
(assert (forall ((x (ref1 (_ BitVec 64)))) (sort (ref t2) (t2tb7 x))))
(declare-fun tb2t7 (uni) (ref1 (_ BitVec 64)))
;; BridgeL
(assert
(forall ((i (ref1 (_ BitVec 64))))
(! (= (tb2t7 (t2tb7 i)) i) :pattern ((t2tb7 i)) )))
;; BridgeR
(assert
(forall ((j uni))
(! (=> (sort (ref t2) j) (= (t2tb7 (tb2t7 j)) j)) :pattern ((t2tb7
(tb2t7 j))) )))
(declare-fun t2tb ((_ BitVec 64)) uni)
;; t2tb_sort
(assert (forall ((x (_ BitVec 64))) (sort t2 (t2tb x))))
(declare-fun tb2t (uni) (_ BitVec 64))
;; BridgeL
(assert
(forall ((i (_ BitVec 64))) (! (= (tb2t (t2tb i)) i) :pattern ((t2tb i)) )))
;; BridgeR
(assert
(forall ((j uni))
(! (=> (sort t2 j) (= (t2tb (tb2t j)) j)) :pattern ((t2tb (tb2t j))) )))
;; contents_def
(assert
(forall ((u (_ BitVec 64))) (= (tb2t (contents t2 (t2tb7 (mk_ref2 u)))) u)))
;; 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-sort skein_512_context 0)
(declare-fun skein_512_context1 () ty)
(declare-sort us_split_fields6 0)
(declare-fun us_split_fields7 () ty)
(declare-sort context_header 0)
(declare-fun context_header1 () ty)
(declare-sort us_split_fields3 0)
(declare-fun us_split_fields4 () ty)
(declare-sort tweak_value 0)
(declare-fun tweak_value1 () ty)
(declare-sort us_split_fields 0)
(declare-fun us_split_fields1 () ty)
(declare-sort u6 0)
(declare-fun u61 () ty)
(declare-sort u7 0)
(declare-fun u71 () ty)
(declare-sort hash_bit_length 0)
(declare-fun hash_bit_length1 () ty)
(declare-sort us_t 0)
(declare-fun us_t1 () ty)
(declare-sort t 0)
(declare-fun t1 () ty)
(declare-sort u64 0)
(declare-fun u641 () ty)
(declare-sort u32 0)
(declare-fun u321 () ty)
(declare-sort u16 0)
(declare-fun u161 () ty)
(declare-sort byte 0)
(declare-fun byte1 () ty)
(declare-sort unsigned_64 0)
(declare-fun unsigned_641 () ty)
(declare-fun t3 () ty)
(declare-fun map1 (ty ty) ty)
(declare-fun ite1 (ty Bool uni uni) uni)
;; ite_sort
(assert
(forall ((a ty))
(forall ((x Bool) (x1 uni) (x2 uni)) (sort a (ite1 a x x1 x2)))))
(declare-fun bool_eq (Bool Bool) Bool)
;; bool_eq_def
(assert
(forall ((x Bool) (y Bool))
(! (ite (= x y) (= (bool_eq x y) true) (= (bool_eq x y) false)) :pattern (
(bool_eq x y)) )))
(declare-fun to_int1 (Bool) Int)
;; to_int_def
(assert
(forall ((b Bool))
(! (ite (= b true) (= (to_int1 b) 1) (= (to_int1 b) 0)) :pattern ((to_int1
b)) )))
(declare-fun of_int (Int) Bool)
;; of_int_def
(assert
(forall ((i Int))
(! (ite (= i 0) (= (of_int i) false) (= (of_int i) true)) :pattern (
(of_int i)) )))
(declare-fun in_range (Int) Bool)
;; in_range_def
(assert
(forall ((x Int))
(! (= (in_range x) (or (= x 0) (= x 1))) :pattern ((in_range x)) )))
(declare-fun attr__ATTRIBUTE_IMAGE (Bool) uni)
;; attr__ATTRIBUTE_IMAGE_sort
(assert (forall ((x Bool)) (sort us_image (attr__ATTRIBUTE_IMAGE x))))
(declare-fun attr__ATTRIBUTE_VALUE__pre_check (uni) Bool)
(declare-fun attr__ATTRIBUTE_VALUE (uni) Bool)
;; size_int_pos
(assert (< 0 8))
(declare-fun nth ((_ BitVec 8) Int) Bool)
(declare-fun lsr ((_ BitVec 8) Int) (_ BitVec 8))
(declare-fun asr ((_ BitVec 8) Int) (_ BitVec 8))
(declare-fun lsl ((_ BitVec 8) Int) (_ BitVec 8))
(declare-fun pow2 (Int) Int)
(declare-fun to_int2 ((_ BitVec 8)) Int)
(declare-fun of_int1 (Int) (_ BitVec 8))
;; to_int_extensionality
(assert
(forall ((v (_ BitVec 8)) (vqt (_ BitVec 8)))
(=> (= (to_int2 v) (to_int2 vqt)) (= v vqt))))
(declare-fun uint_in_range (Int) Bool)
;; uint_in_range_def
(assert
(forall ((i Int))
(! (= (uint_in_range i) (and (<= 0 i) (<= i 255))) :pattern ((uint_in_range
i)) )))
;; Of_int_zero
(assert (= #x00 ((_ int2bv 8) 0)))
;; Of_int_ones
(assert (= #xFF ((_ int2bv 8) 255)))
;; lsr_bv_is_lsr
(assert
(forall ((x (_ BitVec 8)) (n (_ BitVec 8)))
(= (bvlshr x n) (lsr x (bv2int n)))))
;; asr_bv_is_asr
(assert
(forall ((x (_ BitVec 8)) (n (_ BitVec 8)))
(= (bvashr x n) (asr x (bv2int n)))))
;; lsl_bv_is_lsl
(assert
(forall ((x (_ BitVec 8)) (n (_ BitVec 8)))
(= (bvshl x n) (lsl x (bv2int n)))))
;; two_power_size_val
(assert (= (+ 255 1) (pow2 8)))
(declare-fun bool_eq1 ((_ BitVec 8) (_ BitVec 8)) Bool)
;; bool_eq_def
(assert
(forall ((x (_ BitVec 8)) (y (_ BitVec 8)))
(! (ite (= x y) (= (bool_eq1 x y) true) (= (bool_eq1 x y) false)) :pattern (
(bool_eq1 x y)) )))
(declare-fun bool_ne ((_ BitVec 8) (_ BitVec 8)) Bool)
;; bool_ne_def
(assert
(forall ((x (_ BitVec 8)) (y (_ BitVec 8)))
(! (ite (not (= x y)) (= (bool_ne x y) true) (= (bool_ne x y) false)) :pattern (
(bool_ne x y)) )))
(declare-fun bool_lt ((_ BitVec 8) (_ BitVec 8)) Bool)
;; bool_lt_def
(assert
(forall ((x (_ BitVec 8)) (y (_ BitVec 8)))
(! (ite (bvult x y) (= (bool_lt x y) true) (= (bool_lt x y) false)) :pattern (
(bool_lt x y)) )))
(declare-fun bool_le ((_ BitVec 8) (_ BitVec 8)) Bool)
;; bool_le_def
(assert
(forall ((x (_ BitVec 8)) (y (_ BitVec 8)))
(! (ite (bvule x y) (= (bool_le x y) true) (= (bool_le x y) false)) :pattern (
(bool_le x y)) )))
(declare-fun bool_gt ((_ BitVec 8) (_ BitVec 8)) Bool)
;; bool_gt_def
(assert
(forall ((x (_ BitVec 8)) (y (_ BitVec 8)))
(! (ite (bvugt x y) (= (bool_gt x y) true) (= (bool_gt x y) false)) :pattern (
(bool_gt x y)) )))
(declare-fun bool_ge ((_ BitVec 8) (_ BitVec 8)) Bool)
;; bool_ge_def
(assert
(forall ((x (_ BitVec 8)) (y (_ BitVec 8)))
(! (ite (bvuge x y) (= (bool_ge x y) true) (= (bool_ge x y) false)) :pattern (
(bool_ge x y)) )))
(declare-fun power ((_ BitVec 8) Int) (_ BitVec 8))
;; Power_0
(assert (forall ((x (_ BitVec 8))) (= (power x 0) ((_ int2bv 8) 1))))
;; Power_1
(assert (forall ((x (_ BitVec 8))) (= (power x 1) x)))
;; Power_s
(assert
(forall ((x (_ BitVec 8)) (n Int))
(=> (<= 0 n) (= (power x (+ n 1)) (bvmul x (power x n))))))
;; Power_s_alt
(assert
(forall ((x (_ BitVec 8)) (n Int))
(=> (< 0 n) (= (power x n) (bvmul x (power x (- n 1)))))))
;; Power_sum
(assert
(forall ((x (_ BitVec 8)) (n Int) (m Int))
(=> (<= 0 n)
(=> (<= 0 m) (= (power x (+ n m)) (bvmul (power x n) (power x m)))))))
;; Power_mult
(assert
(forall ((x (_ BitVec 8)) (n Int) (m Int))
(=> (<= 0 n) (=> (<= 0 m) (= (power x (* n m)) (power (power x n) m))))))
;; Power_mult2
(assert
(forall ((x (_ BitVec 8)) (y (_ BitVec 8)) (n Int))
(=> (<= 0 n) (= (power (bvmul x y) n) (bvmul (power x n) (power y n))))))
(declare-fun bv_min ((_ BitVec 8) (_ BitVec 8)) (_ BitVec 8))
;; bv_min_def
(assert
(forall ((x (_ BitVec 8)) (y (_ BitVec 8)))
(! (ite (bvule x y) (= (bv_min x y) x) (= (bv_min x y) y)) :pattern (
(bv_min x y)) )))
(declare-fun bv_max ((_ BitVec 8) (_ BitVec 8)) (_ BitVec 8))
;; bv_max_def
(assert
(forall ((x (_ BitVec 8)) (y (_ BitVec 8)))
(! (ite (bvule x y) (= (bv_max x y) y) (= (bv_max x y) x)) :pattern (
(bv_max x y)) )))
;; bv_min_to_uint
(assert
(forall ((x (_ BitVec 8)) (y (_ BitVec 8)))
(= (bv2int (bv_min x y)) (ite (< (bv2int x) (bv2int y)) (bv2int x) (bv2int y)))))
;; bv_max_to_uint
(assert
(forall ((x (_ BitVec 8)) (y (_ BitVec 8)))
(= (bv2int (bv_max x y)) (ite (< (bv2int x) (bv2int y)) (bv2int y) (bv2int x)))))
;; size_int_pos
(assert (< 0 64))
(declare-fun nth1 ((_ BitVec 64) Int) Bool)
(declare-fun lsr1 ((_ BitVec 64) Int) (_ BitVec 64))
(declare-fun asr1 ((_ BitVec 64) Int) (_ BitVec 64))
(declare-fun lsl1 ((_ BitVec 64) Int) (_ BitVec 64))
(declare-fun to_int3 ((_ BitVec 64)) Int)
(declare-fun of_int2 (Int) (_ BitVec 64))
;; to_int_extensionality
(assert
(forall ((v (_ BitVec 64)) (vqt (_ BitVec 64)))
(=> (= (to_int3 v) (to_int3 vqt)) (= v vqt))))
(declare-fun uint_in_range1 (Int) Bool)
;; uint_in_range_def
(assert
(forall ((i Int))
(! (= (uint_in_range1 i) (and (<= 0 i) (<= i 18446744073709551615))) :pattern ((uint_in_range1
i)) )))
;; Of_int_zero
(assert (= #x0000000000000000 ((_ int2bv 64) 0)))
;; Of_int_ones
(assert (= #xFFFFFFFFFFFFFFFF ((_ int2bv 64) 18446744073709551615)))
;; lsr_bv_is_lsr
(assert
(forall ((x (_ BitVec 64)) (n (_ BitVec 64)))
(= (bvlshr x n) (lsr1 x (bv2int n)))))
;; asr_bv_is_asr
(assert
(forall ((x (_ BitVec 64)) (n (_ BitVec 64)))
(= (bvashr x n) (asr1 x (bv2int n)))))
;; lsl_bv_is_lsl
(assert
(forall ((x (_ BitVec 64)) (n (_ BitVec 64)))
(= (bvshl x n) (lsl1 x (bv2int n)))))
;; two_power_size_val
(assert (= (+ 18446744073709551615 1) (pow2 64)))
(declare-fun bool_eq2 ((_ BitVec 64) (_ BitVec 64)) Bool)
;; bool_eq_def
(assert
(forall ((x (_ BitVec 64)) (y (_ BitVec 64)))
(! (ite (= x y) (= (bool_eq2 x y) true) (= (bool_eq2 x y) false)) :pattern (
(bool_eq2 x y)) )))
(declare-fun bool_ne1 ((_ BitVec 64) (_ BitVec 64)) Bool)
;; bool_ne_def
(assert
(forall ((x (_ BitVec 64)) (y (_ BitVec 64)))
(! (ite (not (= x y)) (= (bool_ne1 x y) true) (= (bool_ne1 x y) false)) :pattern (
(bool_ne1 x y)) )))
(declare-fun bool_lt1 ((_ BitVec 64) (_ BitVec 64)) Bool)
;; bool_lt_def
(assert
(forall ((x (_ BitVec 64)) (y (_ BitVec 64)))
(! (ite (bvult x y) (= (bool_lt1 x y) true) (= (bool_lt1 x y) false)) :pattern (
(bool_lt1 x y)) )))
(declare-fun bool_le1 ((_ BitVec 64) (_ BitVec 64)) Bool)
;; bool_le_def
(assert
(forall ((x (_ BitVec 64)) (y (_ BitVec 64)))
(! (ite (bvule x y) (= (bool_le1 x y) true) (= (bool_le1 x y) false)) :pattern (
(bool_le1 x y)) )))
(declare-fun bool_gt1 ((_ BitVec 64) (_ BitVec 64)) Bool)
;; bool_gt_def
(assert
(forall ((x (_ BitVec 64)) (y (_ BitVec 64)))
(! (ite (bvugt x y) (= (bool_gt1 x y) true) (= (bool_gt1 x y) false)) :pattern (
(bool_gt1 x y)) )))
(declare-fun bool_ge1 ((_ BitVec 64) (_ BitVec 64)) Bool)
;; bool_ge_def
(assert
(forall ((x (_ BitVec 64)) (y (_ BitVec 64)))
(! (ite (bvuge x y) (= (bool_ge1 x y) true) (= (bool_ge1 x y) false)) :pattern (
(bool_ge1 x y)) )))
(declare-fun power1 ((_ BitVec 64) Int) (_ BitVec 64))
;; Power_0
(assert (forall ((x (_ BitVec 64))) (= (power1 x 0) ((_ int2bv 64) 1))))
;; Power_1
(assert (forall ((x (_ BitVec 64))) (= (power1 x 1) x)))
;; Power_s
(assert
(forall ((x (_ BitVec 64)) (n Int))
(=> (<= 0 n) (= (power1 x (+ n 1)) (bvmul x (power1 x n))))))
;; Power_s_alt
(assert
(forall ((x (_ BitVec 64)) (n Int))
(=> (< 0 n) (= (power1 x n) (bvmul x (power1 x (- n 1)))))))
;; Power_sum
(assert
(forall ((x (_ BitVec 64)) (n Int) (m Int))
(=> (<= 0 n)
(=> (<= 0 m) (= (power1 x (+ n m)) (bvmul (power1 x n) (power1 x m)))))))
;; Power_mult
(assert
(forall ((x (_ BitVec 64)) (n Int) (m Int))
(=> (<= 0 n) (=> (<= 0 m) (= (power1 x (* n m)) (power1 (power1 x n) m))))))
;; Power_mult2
(assert
(forall ((x (_ BitVec 64)) (y (_ BitVec 64)) (n Int))
(=> (<= 0 n) (= (power1 (bvmul x y) n) (bvmul (power1 x n) (power1 y n))))))
(declare-fun bv_min1 ((_ BitVec 64) (_ BitVec 64)) (_ BitVec 64))
;; bv_min_def
(assert
(forall ((x (_ BitVec 64)) (y (_ BitVec 64)))
(! (ite (bvule x y) (= (bv_min1 x y) x) (= (bv_min1 x y) y)) :pattern (
(bv_min1 x y)) )))
(declare-fun bv_max1 ((_ BitVec 64) (_ BitVec 64)) (_ BitVec 64))
;; bv_max_def
(assert
(forall ((x (_ BitVec 64)) (y (_ BitVec 64)))
(! (ite (bvule x y) (= (bv_max1 x y) y) (= (bv_max1 x y) x)) :pattern (
(bv_max1 x y)) )))
;; bv_min_to_uint
(assert
(forall ((x (_ BitVec 64)) (y (_ BitVec 64)))
(= (bv2int (bv_min1 x y)) (ite (< (bv2int x) (bv2int y)) (bv2int x) (bv2int y)))))
;; bv_max_to_uint
(assert
(forall ((x (_ BitVec 64)) (y (_ BitVec 64)))
(= (bv2int (bv_max1 x y)) (ite (< (bv2int x) (bv2int y)) (bv2int y) (bv2int x)))))
(declare-fun in_range1 ((_ BitVec 8)) Bool)
;; in_range_def
(assert
(forall ((x (_ BitVec 8)))
(! (= (in_range1 x)
(and (bvule ((_ int2bv 8) 0) x) (bvule x ((_ int2bv 8) 255)))) :pattern ((in_range1
x)) )))
(declare-fun in_range_int (Int) Bool)
;; in_range_int_def
(assert
(forall ((x Int))
(! (= (in_range_int x) (and (<= 0 x) (<= x 255))) :pattern ((in_range_int
x)) )))
(declare-fun bool_eq3 (Int Int) Bool)
(declare-fun bool_ne2 (Int Int) Bool)
(declare-fun bool_lt2 (Int Int) Bool)
(declare-fun bool_le2 (Int Int) Bool)
(declare-fun bool_gt2 (Int Int) Bool)
(declare-fun bool_ge2 (Int Int) Bool)
;; bool_eq_axiom
(assert
(forall ((x Int)) (forall ((y Int)) (= (= (bool_eq3 x y) true) (= x y)))))
;; bool_ne_axiom
(assert
(forall ((x Int))
(forall ((y Int)) (= (= (bool_ne2 x y) true) (not (= x y))))))
;; bool_lt_axiom
(assert
(forall ((x Int)) (forall ((y Int)) (= (= (bool_lt2 x y) true) (< x y)))))
;; bool_int__le_axiom
(assert
(forall ((x Int)) (forall ((y Int)) (= (= (bool_le2 x y) true) (<= x y)))))
;; bool_gt_axiom
(assert
(forall ((x Int)) (forall ((y Int)) (= (= (bool_gt2 x y) true) (< y x)))))
;; bool_ge_axiom
(assert
(forall ((x Int)) (forall ((y Int)) (= (= (bool_ge2 x y) true) (<= y x)))))
(declare-fun bool_eq4 ((_ BitVec 8) (_ BitVec 8)) Bool)
;; bool_eq_def
(assert
(forall ((x (_ BitVec 8)) (y (_ BitVec 8)))
(! (ite (= x y) (= (bool_eq4 x y) true) (= (bool_eq4 x y) false)) :pattern (
(bool_eq4 x y)) )))
(declare-fun attr__ATTRIBUTE_IMAGE1 ((_ BitVec 8)) uni)
;; attr__ATTRIBUTE_IMAGE_sort
(assert
(forall ((x (_ BitVec 8))) (sort us_image (attr__ATTRIBUTE_IMAGE1 x))))
(declare-fun attr__ATTRIBUTE_VALUE__pre_check1 (uni) Bool)
(declare-fun attr__ATTRIBUTE_VALUE1 (uni) (_ BitVec 8))
(declare-fun to_rep (byte) (_ BitVec 8))
(declare-fun of_rep ((_ BitVec 8)) byte)
(declare-fun user_eq (byte byte) Bool)
(declare-fun dummy () byte)
;; inversion_axiom
(assert
(forall ((x byte)) (! (= (of_rep (to_rep x)) x) :pattern ((to_rep x)) )))
;; range_axiom
(assert
(forall ((x byte)) (! (in_range1 (to_rep x)) :pattern ((to_rep x)) )))
(declare-fun to_int4 (byte) Int)
;; to_int_def
(assert
(forall ((x byte))
(! (= (to_int4 x) (bv2int (to_rep x))) :pattern ((to_int4 x)) )))
;; range_int_axiom
(assert
(forall ((x byte)) (! (in_range_int (to_int4 x)) :pattern ((to_int4 x)) )))
;; coerce_axiom
(assert
(forall ((x (_ BitVec 8)))
(! (= (to_rep (of_rep x)) x) :pattern ((to_rep (of_rep x))) )))
(declare-fun in_range2 ((_ BitVec 64)) Bool)
;; in_range_def
(assert
(forall ((x (_ BitVec 64)))
(! (= (in_range2 x)
(and (bvule ((_ int2bv 64) 0) x)
(bvule x ((_ int2bv 64) 18446744073709551615)))) :pattern ((in_range2
x)) )))
(declare-fun in_range_int1 (Int) Bool)
;; in_range_int_def
(assert
(forall ((x Int))
(! (= (in_range_int1 x) (and (<= 0 x) (<= x 18446744073709551615))) :pattern ((in_range_int1
x)) )))
(declare-fun bool_eq5 ((_ BitVec 64) (_ BitVec 64)) Bool)
;; bool_eq_def
(assert
(forall ((x (_ BitVec 64)) (y (_ BitVec 64)))
(! (ite (= x y) (= (bool_eq5 x y) true) (= (bool_eq5 x y) false)) :pattern (
(bool_eq5 x y)) )))
(declare-fun attr__ATTRIBUTE_IMAGE2 ((_ BitVec 64)) uni)
;; attr__ATTRIBUTE_IMAGE_sort
(assert
(forall ((x (_ BitVec 64))) (sort us_image (attr__ATTRIBUTE_IMAGE2 x))))
(declare-fun attr__ATTRIBUTE_VALUE__pre_check2 (uni) Bool)
(declare-fun attr__ATTRIBUTE_VALUE2 (uni) (_ BitVec 64))
(declare-fun to_rep1 (u64) (_ BitVec 64))
(declare-fun of_rep1 ((_ BitVec 64)) u64)
(declare-fun user_eq1 (u64 u64) Bool)
(declare-fun dummy1 () u64)
;; inversion_axiom
(assert
(forall ((x u64)) (! (= (of_rep1 (to_rep1 x)) x) :pattern ((to_rep1 x)) )))
;; range_axiom
(assert
(forall ((x u64)) (! (in_range2 (to_rep1 x)) :pattern ((to_rep1 x)) )))
(declare-fun to_int5 (u64) Int)
;; to_int_def
(assert
(forall ((x u64))
(! (= (to_int5 x) (bv2int (to_rep1 x))) :pattern ((to_int5 x)) )))
;; range_int_axiom
(assert
(forall ((x u64)) (! (in_range_int1 (to_int5 x)) :pattern ((to_int5 x)) )))
;; coerce_axiom
(assert
(forall ((x (_ BitVec 64)))
(! (= (to_rep1 (of_rep1 x)) x) :pattern ((to_rep1 (of_rep1 x))) )))
(declare-fun get (ty ty uni uni) uni)
;; get_sort
(assert
(forall ((a ty) (b ty))
(forall ((x uni) (x1 uni)) (sort b (get b a x x1)))))
(declare-fun set (ty ty uni uni uni) uni)
;; set_sort
(assert
(forall ((a ty) (b ty))
(forall ((x uni) (x1 uni) (x2 uni)) (sort (map1 a b) (set b a x x1 x2)))))
(declare-fun const1 (ty ty uni) uni)
;; const_sort
(assert
(forall ((a ty) (b ty))
(forall ((x uni)) (sort (map1 a b) (const1 b a x)))))
(declare-fun const2 (byte) (Array (_ BitVec 64) byte))
(declare-fun const3 (u64) (Array (_ BitVec 64) u64))
;; Const
(assert (forall ((b u64) (a (_ BitVec 64))) (= (select (const3 b) a) b)))
;; Const
(assert (forall ((b byte) (a (_ BitVec 64))) (= (select (const2 b) a) b)))
;; Const
(assert
(forall ((a ty) (b ty))
(forall ((b1 uni) (a1 uni))
(=> (sort b b1) (= (get b a (const1 b a b1) a1) b1)))))
(declare-fun bool_eq9 (ty uni (_ BitVec 64) (_ BitVec 64) uni (_ BitVec 64)
(_ BitVec 64)) Bool)
(declare-fun bool_eq33 ((Array (_ BitVec 64) byte) (_ BitVec 64)
(_ BitVec 64) (Array (_ BitVec 64) byte) (_ BitVec 64) (_ BitVec 64)) Bool)
(declare-fun bool_eq34 ((Array (_ BitVec 64) u64) (_ BitVec 64) (_ BitVec 64)
(Array (_ BitVec 64) u64) (_ BitVec 64) (_ BitVec 64)) Bool)
;; T__ada_array___equal_def
(assert
(forall ((a (Array (_ BitVec 64) u64)))
(forall ((af (_ BitVec 64)))
(forall ((al (_ BitVec 64)))
(forall ((b (Array (_ BitVec 64) u64)))
(forall ((bf (_ BitVec 64)))
(forall ((bl (_ BitVec 64)))
(! (=
(and
(ite (bvule af al)
(= (bvadd (bvsub al af) ((_ int2bv 64) 1)) (bvadd (bvsub bl bf) ((_ int2bv 64) 1)))
(bvugt bf bl))
(forall ((i (_ BitVec 64)))
(! (=> (and (bvule af i) (bvule i al))
(= (select a i) (select b (bvadd (bvsub bf af) i)))) :pattern ((select a i)) )))
(= (bool_eq34 a af al b bf bl) true)) :pattern ((bool_eq34 a af al b bf
bl)) ))))))))
;; T__ada_array___equal_def
(assert
(forall ((a (Array (_ BitVec 64) byte)))
(forall ((af (_ BitVec 64)))
(forall ((al (_ BitVec 64)))
(forall ((b (Array (_ BitVec 64) byte)))
(forall ((bf (_ BitVec 64)))
(forall ((bl (_ BitVec 64)))
(! (=
(and
(ite (bvule af al)
(= (bvadd (bvsub al af) ((_ int2bv 64) 1)) (bvadd (bvsub bl bf) ((_ int2bv 64) 1)))
(bvugt bf bl))
(forall ((i (_ BitVec 64)))
(! (=> (and (bvule af i) (bvule i al))
(= (select a i) (select b (bvadd (bvsub bf af) i)))) :pattern ((select a i)) )))
(= (bool_eq33 a af al b bf bl) true)) :pattern ((bool_eq33 a af al b bf
bl)) ))))))))
;; T__ada_array___equal_def
(assert
(forall ((a ty))
(forall ((a1 uni))
(forall ((af (_ BitVec 64)))
(forall ((al (_ BitVec 64)))
(forall ((b uni))
(forall ((bf (_ BitVec 64)))
(forall ((bl (_ BitVec 64)))
(! (=
(and
(ite (bvule af al)
(= (bvadd (bvsub al af) ((_ int2bv 64) 1)) (bvadd (bvsub bl bf) ((_ int2bv 64) 1)))
(bvugt bf bl))
(forall ((i (_ BitVec 64)))
(! (=> (and (bvule af i) (bvule i al))
(= (get a t2 a1 (t2tb i)) (get a t2 b (t2tb (bvadd (bvsub bf af) i))))) :pattern (
(get a t2 a1 (t2tb i))) ))) (= (bool_eq9 a a1 af al b bf bl) true)) :pattern (
(bool_eq9 a a1 af al b bf bl)) )))))))))
(declare-fun slide (ty uni (_ BitVec 64) (_ BitVec 64)) uni)
;; slide_sort
(assert
(forall ((a ty))
(forall ((x uni) (x1 (_ BitVec 64)) (x2 (_ BitVec 64))) (sort (map1 t2 a)
(slide a x x1 x2)))))
(declare-fun slide1 ((Array (_ BitVec 64) byte) (_ BitVec 64)
(_ BitVec 64)) (Array (_ BitVec 64) byte))
(declare-fun slide2 ((Array (_ BitVec 64) u64) (_ BitVec 64)
(_ BitVec 64)) (Array (_ BitVec 64) u64))
;; slide_eq
(assert
(forall ((a (Array (_ BitVec 64) u64)))
(forall ((first10 (_ BitVec 64)))
(! (= (slide2 a first10 first10) a) :pattern ((slide2 a first10 first10)) ))))
;; slide_eq
(assert
(forall ((a (Array (_ BitVec 64) byte)))
(forall ((first10 (_ BitVec 64)))
(! (= (slide1 a first10 first10) a) :pattern ((slide1 a first10 first10)) ))))
;; slide_eq
(assert
(forall ((a ty))
(forall ((a1 uni))
(=> (sort (map1 t2 a) a1)
(forall ((first10 (_ BitVec 64)))
(! (= (slide a a1 first10 first10) a1) :pattern ((slide a a1 first10
first10)) ))))))
;; slide_def
(assert
(forall ((a (Array (_ BitVec 64) u64)))
(forall ((old_first (_ BitVec 64)))
(forall ((new_first (_ BitVec 64)))
(forall ((i (_ BitVec 64)))
(! (= (select (slide2 a old_first new_first) i) (select a (bvsub i (bvsub new_first old_first)))) :pattern ((select
(slide2 a old_first new_first) i)) ))))))
;; slide_def
(assert
(forall ((a (Array (_ BitVec 64) byte)))
(forall ((old_first (_ BitVec 64)))
(forall ((new_first (_ BitVec 64)))
(forall ((i (_ BitVec 64)))
(! (= (select (slide1 a old_first new_first) i) (select a (bvsub i (bvsub new_first old_first)))) :pattern ((select
(slide1 a old_first new_first) i)) ))))))
;; slide_def
(assert
(forall ((a ty))
(forall ((a1 uni))
(forall ((old_first (_ BitVec 64)))
(forall ((new_first (_ BitVec 64)))
(forall ((i (_ BitVec 64)))
(! (= (get a t2 (slide a a1 old_first new_first) (t2tb i)) (get a t2 a1
(t2tb
(bvsub i (bvsub new_first old_first))))) :pattern (
(get a t2 (slide a a1 old_first new_first) (t2tb i))) )))))))
(declare-fun concat1 (ty uni (_ BitVec 64) (_ BitVec 64) uni (_ BitVec 64)
(_ BitVec 64)) uni)
;; concat_sort
(assert
(forall ((a ty))
(forall ((x uni) (x1 (_ BitVec 64)) (x2 (_ BitVec 64)) (x3 uni)
(x4 (_ BitVec 64)) (x5 (_ BitVec 64))) (sort (map1 t2 a)
(concat1 a x x1 x2 x3 x4 x5)))))
(declare-fun concat2 ((Array (_ BitVec 64) byte) (_ BitVec 64) (_ BitVec 64)
(Array (_ BitVec 64) byte) (_ BitVec 64)
(_ BitVec 64)) (Array (_ BitVec 64) byte))
(declare-fun concat3 ((Array (_ BitVec 64) u64) (_ BitVec 64) (_ BitVec 64)
(Array (_ BitVec 64) u64) (_ BitVec 64)
(_ BitVec 64)) (Array (_ BitVec 64) u64))
;; concat_def
(assert
(forall ((a (Array (_ BitVec 64) u64)) (b (Array (_ BitVec 64) u64)))
(forall ((a_first (_ BitVec 64)) (a_last (_ BitVec 64))
(b_first (_ BitVec 64)) (b_last (_ BitVec 64)))
(forall ((i (_ BitVec 64)))
(! (and
(=> (and (bvule a_first i) (bvule i a_last))
(= (select (concat3 a a_first a_last b b_first b_last) i) (select a i)))
(=> (bvugt i a_last)
(= (select (concat3 a a_first a_last b b_first b_last) i) (select b (bvadd (bvsub i a_last) (bvsub b_first ((_ int2bv 64) 1))))))) :pattern ((select
(concat3 a a_first a_last b b_first b_last) i)) )))))
;; concat_def
(assert
(forall ((a (Array (_ BitVec 64) byte)) (b (Array (_ BitVec 64) byte)))
(forall ((a_first (_ BitVec 64)) (a_last (_ BitVec 64))
(b_first (_ BitVec 64)) (b_last (_ BitVec 64)))
(forall ((i (_ BitVec 64)))
(! (and
(=> (and (bvule a_first i) (bvule i a_last))
(= (select (concat2 a a_first a_last b b_first b_last) i) (select a i)))
(=> (bvugt i a_last)
(= (select (concat2 a a_first a_last b b_first b_last) i) (select b (bvadd (bvsub i a_last) (bvsub b_first ((_ int2bv 64) 1))))))) :pattern ((select
(concat2 a a_first a_last b b_first b_last) i)) )))))
;; concat_def
(assert
(forall ((a ty))
(forall ((a1 uni) (b uni))
(forall ((a_first (_ BitVec 64)) (a_last (_ BitVec 64))
(b_first (_ BitVec 64)) (b_last (_ BitVec 64)))
(forall ((i (_ BitVec 64)))
(! (and
(=> (and (bvule a_first i) (bvule i a_last))
(= (get a t2 (concat1 a a1 a_first a_last b b_first b_last) (t2tb i))
(get a t2 a1 (t2tb i))))
(=> (bvugt i a_last)
(= (get a t2 (concat1 a a1 a_first a_last b b_first b_last) (t2tb i))
(get a t2 b
(t2tb (bvadd (bvsub i a_last) (bvsub b_first ((_ int2bv 64) 1)))))))) :pattern (
(get a t2 (concat1 a a1 a_first a_last b b_first b_last) (t2tb i))) ))))))
(declare-fun compare (ty uni (_ BitVec 64) (_ BitVec 64) uni (_ BitVec 64)
(_ BitVec 64)) Int)
(declare-fun compare1 ((Array (_ BitVec 64) byte) (_ BitVec 64) (_ BitVec 64)
(Array (_ BitVec 64) byte) (_ BitVec 64) (_ BitVec 64)) Int)
(declare-fun compare2 ((Array (_ BitVec 64) u64) (_ BitVec 64) (_ BitVec 64)
(Array (_ BitVec 64) u64) (_ BitVec 64) (_ BitVec 64)) Int)
(declare-fun xorb (ty uni (_ BitVec 64) (_ BitVec 64) uni (_ BitVec 64)
(_ BitVec 64)) uni)
;; xorb_sort
(assert
(forall ((a ty))
(forall ((x uni) (x1 (_ BitVec 64)) (x2 (_ BitVec 64)) (x3 uni)
(x4 (_ BitVec 64)) (x5 (_ BitVec 64))) (sort (map1 t2 a)
(xorb a x x1 x2 x3 x4 x5)))))
(declare-fun xorb1 ((Array (_ BitVec 64) byte) (_ BitVec 64) (_ BitVec 64)
(Array (_ BitVec 64) byte) (_ BitVec 64)
(_ BitVec 64)) (Array (_ BitVec 64) byte))
(declare-fun xorb2 ((Array (_ BitVec 64) u64) (_ BitVec 64) (_ BitVec 64)
(Array (_ BitVec 64) u64) (_ BitVec 64)
(_ BitVec 64)) (Array (_ BitVec 64) u64))
(declare-fun andb (ty uni (_ BitVec 64) (_ BitVec 64) uni (_ BitVec 64)
(_ BitVec 64)) uni)
;; andb_sort
(assert
(forall ((a ty))
(forall ((x uni) (x1 (_ BitVec 64)) (x2 (_ BitVec 64)) (x3 uni)
(x4 (_ BitVec 64)) (x5 (_ BitVec 64))) (sort (map1 t2 a)
(andb a x x1 x2 x3 x4 x5)))))
(declare-fun andb1 ((Array (_ BitVec 64) byte) (_ BitVec 64) (_ BitVec 64)
(Array (_ BitVec 64) byte) (_ BitVec 64)
(_ BitVec 64)) (Array (_ BitVec 64) byte))
(declare-fun andb2 ((Array (_ BitVec 64) u64) (_ BitVec 64) (_ BitVec 64)
(Array (_ BitVec 64) u64) (_ BitVec 64)
(_ BitVec 64)) (Array (_ BitVec 64) u64))
(declare-fun orb (ty uni (_ BitVec 64) (_ BitVec 64) uni (_ BitVec 64)
(_ BitVec 64)) uni)
;; orb_sort
(assert
(forall ((a ty))
(forall ((x uni) (x1 (_ BitVec 64)) (x2 (_ BitVec 64)) (x3 uni)
(x4 (_ BitVec 64)) (x5 (_ BitVec 64))) (sort (map1 t2 a)
(orb a x x1 x2 x3 x4 x5)))))
(declare-fun orb1 ((Array (_ BitVec 64) byte) (_ BitVec 64) (_ BitVec 64)
(Array (_ BitVec 64) byte) (_ BitVec 64)
(_ BitVec 64)) (Array (_ BitVec 64) byte))
(declare-fun orb2 ((Array (_ BitVec 64) u64) (_ BitVec 64) (_ BitVec 64)
(Array (_ BitVec 64) u64) (_ BitVec 64)
(_ BitVec 64)) (Array (_ BitVec 64) u64))
(declare-fun notb (ty uni (_ BitVec 64) (_ BitVec 64)) uni)
;; notb_sort
(assert
(forall ((a ty))
(forall ((x uni) (x1 (_ BitVec 64)) (x2 (_ BitVec 64))) (sort (map1 t2 a)
(notb a x x1 x2)))))
(declare-fun notb1 ((Array (_ BitVec 64) byte) (_ BitVec 64)
(_ BitVec 64)) (Array (_ BitVec 64) byte))
(declare-fun notb2 ((Array (_ BitVec 64) u64) (_ BitVec 64)
(_ BitVec 64)) (Array (_ BitVec 64) u64))
(declare-fun singleton (ty uni (_ BitVec 64)) uni)
;; singleton_sort
(assert
(forall ((a ty))
(forall ((x uni) (x1 (_ BitVec 64))) (sort (map1 t2 a) (singleton a x x1)))))
(declare-fun singleton1 (byte (_ BitVec 64)) (Array (_ BitVec 64) byte))
(declare-fun singleton2 (u64 (_ BitVec 64)) (Array (_ BitVec 64) u64))
;; singleton_def
(assert
(forall ((v u64))
(forall ((i (_ BitVec 64)))
(! (= (select (singleton2 v i) i) v) :pattern ((select (singleton2 v i) i)) ))))
;; singleton_def
(assert
(forall ((v byte))
(forall ((i (_ BitVec 64)))
(! (= (select (singleton1 v i) i) v) :pattern ((select (singleton1 v i) i)) ))))
;; singleton_def
(assert
(forall ((a ty))
(forall ((v uni))
(=> (sort a v)
(forall ((i (_ BitVec 64)))
(! (= (get a t2 (singleton a v i) (t2tb i)) v) :pattern ((get a t2
(singleton a v i)
(t2tb i))) ))))))
(declare-fun in_range6 ((_ BitVec 64)) Bool)
;; in_range_def
(assert
(forall ((x (_ BitVec 64)))
(! (= (in_range6 x)
(and (bvule ((_ int2bv 64) 0) x)
(bvule x ((_ int2bv 64) 18446744073709551615)))) :pattern ((in_range6
x)) )))
(declare-fun in_range_int5 (Int) Bool)
;; in_range_int_def
(assert
(forall ((x Int))
(! (= (in_range_int5 x) (and (<= 0 x) (<= x 18446744073709551615))) :pattern ((in_range_int5
x)) )))
(declare-fun bool_eq10 ((_ BitVec 64) (_ BitVec 64)) Bool)
;; bool_eq_def
(assert
(forall ((x (_ BitVec 64)) (y (_ BitVec 64)))
(! (ite (= x y) (= (bool_eq10 x y) true) (= (bool_eq10 x y) false)) :pattern (
(bool_eq10 x y)) )))
(declare-fun attr__ATTRIBUTE_IMAGE6 ((_ BitVec 64)) uni)
;; attr__ATTRIBUTE_IMAGE_sort
(assert
(forall ((x (_ BitVec 64))) (sort us_image (attr__ATTRIBUTE_IMAGE6 x))))
(declare-fun attr__ATTRIBUTE_VALUE__pre_check6 (uni) Bool)
(declare-fun attr__ATTRIBUTE_VALUE6 (uni) (_ BitVec 64))
(declare-fun to_rep5 (unsigned_64) (_ BitVec 64))
(declare-fun of_rep5 ((_ BitVec 64)) unsigned_64)
(declare-fun user_eq5 (unsigned_64 unsigned_64) Bool)
(declare-fun dummy5 () unsigned_64)
;; inversion_axiom
(assert
(forall ((x unsigned_64))
(! (= (of_rep5 (to_rep5 x)) x) :pattern ((to_rep5 x)) )))
;; range_axiom
(assert
(forall ((x unsigned_64)) (! (in_range6
(to_rep5 x)) :pattern ((to_rep5 x)) )))
(declare-fun to_int9 (unsigned_64) Int)
;; to_int_def
(assert
(forall ((x unsigned_64))
(! (= (to_int9 x) (bv2int (to_rep5 x))) :pattern ((to_int9 x)) )))
;; range_int_axiom
(assert
(forall ((x unsigned_64)) (! (in_range_int5
(to_int9 x)) :pattern ((to_int9 x)) )))
;; coerce_axiom
(assert
(forall ((x (_ BitVec 64)))
(! (= (to_rep5 (of_rep5 x)) x) :pattern ((to_rep5 (of_rep5 x))) )))
(declare-fun first (t) unsigned_64)
(declare-fun last (t) unsigned_64)
(declare-fun mk ((_ BitVec 64) (_ BitVec 64)) t)
;; mk_def
(assert
(forall ((f (_ BitVec 64)) (l (_ BitVec 64)))
(! (=> (in_range6 f)
(=> (in_range6 l)
(and (= (to_rep5 (first (mk f l))) f) (= (to_rep5 (last (mk f l))) l)))) :pattern (
(mk f l)) )))
(declare-fun dynamic_property ((_ BitVec 64) (_ BitVec 64) (_ BitVec 64)
(_ BitVec 64)) Bool)
;; dynamic_property_def
(assert
(forall ((range_first (_ BitVec 64)) (range_last (_ BitVec 64))
(low (_ BitVec 64)) (high (_ BitVec 64)))
(! (= (dynamic_property range_first range_last low high)
(and (in_range6 low)
(and (in_range6 high)
(=> (bvule low high) (and (in_range2 low) (in_range2 high)))))) :pattern ((dynamic_property
range_first range_last low high)) )))
(declare-fun mk___t ((Array (_ BitVec 64) byte) t) us_t)
(declare-fun elts (us_t) (Array (_ BitVec 64) byte))
;; elts_def
(assert
(forall ((u (Array (_ BitVec 64) byte)) (u1 t)) (= (elts (mk___t u u1)) u)))
(declare-fun rt (us_t) t)
;; rt_def
(assert
(forall ((u (Array (_ BitVec 64) byte)) (u1 t)) (= (rt (mk___t u u1)) u1)))
(declare-fun of_array ((Array (_ BitVec 64) byte) (_ BitVec 64)
(_ BitVec 64)) us_t)
;; of_array_def
(assert
(forall ((a (Array (_ BitVec 64) byte)) (f (_ BitVec 64))
(l (_ BitVec 64)))
(! (= (of_array a f l) (mk___t a (mk f l))) :pattern ((of_array a f l)) )))
(declare-fun first1 (us_t) (_ BitVec 64))
;; first_def
(assert
(forall ((a us_t))
(! (= (first1 a) (to_rep5 (first (rt a)))) :pattern ((first1 a)) )))
(declare-fun last1 (us_t) (_ BitVec 64))
;; last_def
(assert
(forall ((a us_t))
(! (= (last1 a) (to_rep5 (last (rt a)))) :pattern ((last1 a)) )))
(declare-fun length (us_t) Int)
;; length_def
(assert
(forall ((a us_t))
(! (ite (bvule (first1 a) (last1 a))
(= (length a) (+ (- (bv2int (last1 a)) (bv2int (first1 a))) 1))
(= (length a) 0)) :pattern ((length a)) )))
(declare-fun value__size () Int)
(declare-fun object__size ((Array (_ BitVec 64) byte)) Int)
;; value__size_axiom
(assert (<= 0 value__size))
;; object__size_axiom
(assert (forall ((a (Array (_ BitVec 64) byte))) (<= 0 (object__size a))))
(declare-fun bool_eq11 (us_t us_t) Bool)
;; bool_eq_def
(assert
(forall ((x us_t) (y us_t))
(! (= (bool_eq11 x y) (bool_eq33 (elts x) (to_rep5 (first (rt x)))
(to_rep5 (last (rt x))) (elts y)
(to_rep5 (first (rt y))) (to_rep5 (last (rt y))))) :pattern (
(bool_eq11 x y)) )))
(declare-fun user_eq6 (us_t us_t) Bool)
(declare-fun dummy6 () us_t)
;; compare_def
(assert
(forall ((a (Array (_ BitVec 64) byte)) (b (Array (_ BitVec 64) byte)))
(forall ((a_first (_ BitVec 64)) (a_last (_ BitVec 64))
(b_first (_ BitVec 64)) (b_last (_ BitVec 64)))
(! (and
(= (= (compare1 a a_first a_last b b_first b_last) 0)
(= (bool_eq33 a a_first a_last b b_first b_last) true))
(and
(= (< (compare1 a a_first a_last b b_first b_last) 0)
(exists ((i (_ BitVec 64)) (j (_ BitVec 64)))
(and (bvule i a_last)
(and (bvult j b_last)
(and (= (bool_eq33 a a_first i b b_first j) true)
(or (= i a_last)
(and (bvult i a_last)
(bvult (to_rep (select a (bvadd i ((_ int2bv 64) 1)))) (to_rep
(select b (bvadd j ((_ int2bv 64) 1))))))))))))
(= (< 0 (compare1 a a_first a_last b b_first b_last))
(exists ((i (_ BitVec 64)) (j (_ BitVec 64)))
(and (bvule i b_last)
(and (bvult j a_last)
(and (= (bool_eq33 a a_first j b b_first i) true)
(or (= i b_last)
(and (bvult i b_last)
(bvugt (to_rep (select a (bvadd j ((_ int2bv 64) 1)))) (to_rep
(select b (bvadd i ((_ int2bv 64) 1)))))))))))))) :pattern (
(compare1 a a_first a_last b b_first b_last)) ))))
(declare-fun in_range8 ((_ BitVec 64)) Bool)
;; in_range_def
(assert
(forall ((x (_ BitVec 64)))
(! (= (in_range8 x)
(and (bvule ((_ int2bv 64) 0) x)
(bvule x ((_ int2bv 64) 18446744073709551608)))) :pattern ((in_range8
x)) )))
(declare-fun in_range_int7 (Int) Bool)
;; in_range_int_def
(assert
(forall ((x Int))
(! (= (in_range_int7 x) (and (<= 0 x) (<= x 18446744073709551608))) :pattern ((in_range_int7
x)) )))
(declare-fun bool_eq14 ((_ BitVec 64) (_ BitVec 64)) Bool)
;; bool_eq_def
(assert
(forall ((x (_ BitVec 64)) (y (_ BitVec 64)))
(! (ite (= x y) (= (bool_eq14 x y) true) (= (bool_eq14 x y) false)) :pattern (
(bool_eq14 x y)) )))
(declare-fun attr__ATTRIBUTE_IMAGE8 ((_ BitVec 64)) uni)
;; attr__ATTRIBUTE_IMAGE_sort
(assert
(forall ((x (_ BitVec 64))) (sort us_image (attr__ATTRIBUTE_IMAGE8 x))))
(declare-fun attr__ATTRIBUTE_VALUE__pre_check8 (uni) Bool)
(declare-fun attr__ATTRIBUTE_VALUE8 (uni) (_ BitVec 64))
(declare-fun to_rep7 (hash_bit_length) (_ BitVec 64))
(declare-fun of_rep7 ((_ BitVec 64)) hash_bit_length)
(declare-fun user_eq12 (hash_bit_length hash_bit_length) Bool)
(declare-fun dummy12 () hash_bit_length)
;; inversion_axiom
(assert
(forall ((x hash_bit_length))
(! (= (of_rep7 (to_rep7 x)) x) :pattern ((to_rep7 x)) )))
;; range_axiom
(assert
(forall ((x hash_bit_length)) (! (in_range8
(to_rep7 x)) :pattern ((to_rep7 x)) )))
(declare-fun to_int11 (hash_bit_length) Int)
;; to_int_def
(assert
(forall ((x hash_bit_length))
(! (= (to_int11 x) (bv2int (to_rep7 x))) :pattern ((to_int11 x)) )))
;; range_int_axiom
(assert
(forall ((x hash_bit_length)) (! (in_range_int7
(to_int11 x)) :pattern ((to_int11 x)) )))
;; coerce_axiom
(assert
(forall ((x (_ BitVec 64)))
(! (= (to_rep7 (of_rep7 x)) x) :pattern ((to_rep7 (of_rep7 x))) )))
(declare-sort initialized_hash_bit_length 0)
(declare-fun initialized_hash_bit_length1 () ty)
(declare-fun in_range9 ((_ BitVec 64)) Bool)
;; in_range_def
(assert
(forall ((x (_ BitVec 64)))
(! (= (in_range9 x)
(and (bvule ((_ int2bv 64) 1) x)
(bvule x ((_ int2bv 64) 18446744073709551608)))) :pattern ((in_range9
x)) )))
(declare-fun in_range_int8 (Int) Bool)
;; in_range_int_def
(assert
(forall ((x Int))
(! (= (in_range_int8 x) (and (<= 1 x) (<= x 18446744073709551608))) :pattern ((in_range_int8
x)) )))
(declare-fun bool_eq15 ((_ BitVec 64) (_ BitVec 64)) Bool)
;; bool_eq_def
(assert
(forall ((x (_ BitVec 64)) (y (_ BitVec 64)))
(! (ite (= x y) (= (bool_eq15 x y) true) (= (bool_eq15 x y) false)) :pattern (
(bool_eq15 x y)) )))
(declare-fun attr__ATTRIBUTE_IMAGE9 ((_ BitVec 64)) uni)
;; attr__ATTRIBUTE_IMAGE_sort
(assert
(forall ((x (_ BitVec 64))) (sort us_image (attr__ATTRIBUTE_IMAGE9 x))))
(declare-fun attr__ATTRIBUTE_VALUE__pre_check9 (uni) Bool)
(declare-fun attr__ATTRIBUTE_VALUE9 (uni) (_ BitVec 64))
(declare-fun to_rep8 (initialized_hash_bit_length) (_ BitVec 64))
(declare-fun of_rep8 ((_ BitVec 64)) initialized_hash_bit_length)
(declare-fun user_eq13 (initialized_hash_bit_length
initialized_hash_bit_length) Bool)
(declare-fun dummy13 () initialized_hash_bit_length)
;; inversion_axiom
(assert
(forall ((x initialized_hash_bit_length))
(! (= (of_rep8 (to_rep8 x)) x) :pattern ((to_rep8 x)) )))
;; range_axiom
(assert
(forall ((x initialized_hash_bit_length)) (! (in_range9
(to_rep8 x)) :pattern ((to_rep8 x)) )))
(declare-fun to_int12 (initialized_hash_bit_length) Int)
;; to_int_def
(assert
(forall ((x initialized_hash_bit_length))
(! (= (to_int12 x) (bv2int (to_rep8 x))) :pattern ((to_int12 x)) )))
;; range_int_axiom
(assert
(forall ((x initialized_hash_bit_length)) (! (in_range_int8
(to_int12 x)) :pattern ((to_int12 x)) )))
;; coerce_axiom
(assert
(forall ((x (_ BitVec 64)))
(! (= (to_rep8 (of_rep8 x)) x) :pattern ((to_rep8 (of_rep8 x))) )))
(declare-sort skein_512_block_bytes_count 0)
(declare-fun skein_512_block_bytes_count1 () ty)
(declare-fun in_range11 ((_ BitVec 64)) Bool)
;; in_range_def
(assert
(forall ((x (_ BitVec 64)))
(! (= (in_range11 x)
(and (bvule ((_ int2bv 64) 0) x) (bvule x ((_ int2bv 64) 64)))) :pattern ((in_range11
x)) )))
(declare-fun in_range_int10 (Int) Bool)
;; in_range_int_def
(assert
(forall ((x Int))
(! (= (in_range_int10 x) (and (<= 0 x) (<= x 64))) :pattern ((in_range_int10
x)) )))
(declare-fun bool_eq17 ((_ BitVec 64) (_ BitVec 64)) Bool)
;; bool_eq_def
(assert
(forall ((x (_ BitVec 64)) (y (_ BitVec 64)))
(! (ite (= x y) (= (bool_eq17 x y) true) (= (bool_eq17 x y) false)) :pattern (
(bool_eq17 x y)) )))
(declare-fun attr__ATTRIBUTE_IMAGE11 ((_ BitVec 64)) uni)
;; attr__ATTRIBUTE_IMAGE_sort
(assert
(forall ((x (_ BitVec 64))) (sort us_image (attr__ATTRIBUTE_IMAGE11 x))))
(declare-fun attr__ATTRIBUTE_VALUE__pre_check11 (uni) Bool)
(declare-fun attr__ATTRIBUTE_VALUE11 (uni) (_ BitVec 64))
(declare-fun to_rep10 (skein_512_block_bytes_count) (_ BitVec 64))
(declare-fun of_rep10 ((_ BitVec 64)) skein_512_block_bytes_count)
(declare-fun user_eq16 (skein_512_block_bytes_count
skein_512_block_bytes_count) Bool)
(declare-fun dummy16 () skein_512_block_bytes_count)
;; inversion_axiom
(assert
(forall ((x skein_512_block_bytes_count))
(! (= (of_rep10 (to_rep10 x)) x) :pattern ((to_rep10 x)) )))
;; range_axiom
(assert
(forall ((x skein_512_block_bytes_count)) (! (in_range11
(to_rep10 x)) :pattern ((to_rep10 x)) )))
(declare-fun to_int14 (skein_512_block_bytes_count) Int)
;; to_int_def
(assert
(forall ((x skein_512_block_bytes_count))
(! (= (to_int14 x) (bv2int (to_rep10 x))) :pattern ((to_int14 x)) )))
;; range_int_axiom
(assert
(forall ((x skein_512_block_bytes_count)) (! (in_range_int10
(to_int14 x)) :pattern ((to_int14 x)) )))
;; coerce_axiom
(assert
(forall ((x (_ BitVec 64)))
(! (= (to_rep10 (of_rep10 x)) x) :pattern ((to_rep10 (of_rep10 x))) )))
(declare-sort skein_512_block_bytes_index 0)
(declare-fun skein_512_block_bytes_index1 () ty)
(declare-fun in_range25 ((_ BitVec 64)) Bool)
;; in_range_def
(assert
(forall ((x (_ BitVec 64)))
(! (= (in_range25 x)
(and (bvule ((_ int2bv 64) 0) x) (bvule x ((_ int2bv 64) 63)))) :pattern ((in_range25
x)) )))
(declare-fun in_range_int23 (Int) Bool)
;; in_range_int_def
(assert
(forall ((x Int))
(! (= (in_range_int23 x) (and (<= 0 x) (<= x 63))) :pattern ((in_range_int23
x)) )))
(declare-fun bool_eq39 ((_ BitVec 64) (_ BitVec 64)) Bool)
;; bool_eq_def
(assert
(forall ((x (_ BitVec 64)) (y (_ BitVec 64)))
(! (ite (= x y) (= (bool_eq39 x y) true) (= (bool_eq39 x y) false)) :pattern (
(bool_eq39 x y)) )))
(declare-fun attr__ATTRIBUTE_IMAGE26 ((_ BitVec 64)) uni)
;; attr__ATTRIBUTE_IMAGE_sort
(assert
(forall ((x (_ BitVec 64))) (sort us_image (attr__ATTRIBUTE_IMAGE26 x))))
(declare-fun attr__ATTRIBUTE_VALUE__pre_check26 (uni) Bool)
(declare-fun attr__ATTRIBUTE_VALUE26 (uni) (_ BitVec 64))
(declare-fun to_rep24 (skein_512_block_bytes_index) (_ BitVec 64))
(declare-fun of_rep24 ((_ BitVec 64)) skein_512_block_bytes_index)
(declare-fun user_eq45 (skein_512_block_bytes_index
skein_512_block_bytes_index) Bool)
(declare-fun dummy45 () skein_512_block_bytes_index)
;; inversion_axiom
(assert
(forall ((x skein_512_block_bytes_index))
(! (= (of_rep24 (to_rep24 x)) x) :pattern ((to_rep24 x)) )))
;; range_axiom
(assert
(forall ((x skein_512_block_bytes_index)) (! (in_range25
(to_rep24 x)) :pattern ((to_rep24 x)) )))
(declare-fun to_int29 (skein_512_block_bytes_index) Int)
;; to_int_def
(assert
(forall ((x skein_512_block_bytes_index))
(! (= (to_int29 x) (bv2int (to_rep24 x))) :pattern ((to_int29 x)) )))
;; range_int_axiom
(assert
(forall ((x skein_512_block_bytes_index)) (! (in_range_int23
(to_int29 x)) :pattern ((to_int29 x)) )))
;; coerce_axiom
(assert
(forall ((x (_ BitVec 64)))
(! (= (to_rep24 (of_rep24 x)) x) :pattern ((to_rep24 (of_rep24 x))) )))
(declare-fun dummy24 () (Array (_ BitVec 64) byte))
(declare-fun value__size8 () Int)
(declare-fun object__size8 ((Array (_ BitVec 64) byte)) Int)
;; value__size_axiom
(assert (<= 0 value__size8))
;; object__size_axiom
(assert (forall ((a (Array (_ BitVec 64) byte))) (<= 0 (object__size8 a))))
(declare-fun user_eq24 ((Array (_ BitVec 64) byte)
(Array (_ BitVec 64) byte)) Bool)
;; compare_def
(assert
(forall ((a (Array (_ BitVec 64) byte)) (b (Array (_ BitVec 64) byte)))
(forall ((a_first (_ BitVec 64)) (a_last (_ BitVec 64))
(b_first (_ BitVec 64)) (b_last (_ BitVec 64)))
(! (and
(= (= (compare1 a a_first a_last b b_first b_last) 0)
(= (bool_eq33 a a_first a_last b b_first b_last) true))
(and
(= (< (compare1 a a_first a_last b b_first b_last) 0)
(exists ((i (_ BitVec 64)) (j (_ BitVec 64)))
(and (bvule i a_last)
(and (bvult j b_last)
(and (= (bool_eq33 a a_first i b b_first j) true)
(or (= i a_last)
(and (bvult i a_last)
(bvult (to_rep (select a (bvadd i ((_ int2bv 64) 1)))) (to_rep
(select b (bvadd j ((_ int2bv 64) 1))))))))))))
(= (< 0 (compare1 a a_first a_last b b_first b_last))
(exists ((i (_ BitVec 64)) (j (_ BitVec 64)))
(and (bvule i b_last)
(and (bvult j a_last)
(and (= (bool_eq33 a a_first j b b_first i) true)
(or (= i b_last)
(and (bvult i b_last)
(bvugt (to_rep (select a (bvadd j ((_ int2bv 64) 1)))) (to_rep
(select b (bvadd i ((_ int2bv 64) 1)))))))))))))) :pattern (
(compare1 a a_first a_last b b_first b_last)) ))))
(declare-sort positive_block_512_count_t 0)
(declare-fun positive_block_512_count_t1 () ty)
(declare-fun in_range12 ((_ BitVec 64)) Bool)
;; in_range_def
(assert
(forall ((x (_ BitVec 64)))
(! (= (in_range12 x)
(and (bvule ((_ int2bv 64) 1) x)
(bvule x ((_ int2bv 64) 288230376151711743)))) :pattern ((in_range12
x)) )))
(declare-fun in_range_int11 (Int) Bool)
;; in_range_int_def
(assert
(forall ((x Int))
(! (= (in_range_int11 x) (and (<= 1 x) (<= x 288230376151711743))) :pattern ((in_range_int11
x)) )))
(declare-fun bool_eq18 ((_ BitVec 64) (_ BitVec 64)) Bool)
;; bool_eq_def
(assert
(forall ((x (_ BitVec 64)) (y (_ BitVec 64)))
(! (ite (= x y) (= (bool_eq18 x y) true) (= (bool_eq18 x y) false)) :pattern (
(bool_eq18 x y)) )))
(declare-fun attr__ATTRIBUTE_IMAGE12 ((_ BitVec 64)) uni)
;; attr__ATTRIBUTE_IMAGE_sort
(assert
(forall ((x (_ BitVec 64))) (sort us_image (attr__ATTRIBUTE_IMAGE12 x))))
(declare-fun attr__ATTRIBUTE_VALUE__pre_check12 (uni) Bool)
(declare-fun attr__ATTRIBUTE_VALUE12 (uni) (_ BitVec 64))
(declare-fun to_rep11 (positive_block_512_count_t) (_ BitVec 64))
(declare-fun of_rep11 ((_ BitVec 64)) positive_block_512_count_t)
(declare-fun user_eq17 (positive_block_512_count_t
positive_block_512_count_t) Bool)
(declare-fun dummy17 () positive_block_512_count_t)
;; inversion_axiom
(assert
(forall ((x positive_block_512_count_t))
(! (= (of_rep11 (to_rep11 x)) x) :pattern ((to_rep11 x)) )))
;; range_axiom
(assert
(forall ((x positive_block_512_count_t)) (! (in_range12
(to_rep11 x)) :pattern ((to_rep11 x)) )))
(declare-fun to_int15 (positive_block_512_count_t) Int)
;; to_int_def
(assert
(forall ((x positive_block_512_count_t))
(! (= (to_int15 x) (bv2int (to_rep11 x))) :pattern ((to_int15 x)) )))
;; range_int_axiom
(assert
(forall ((x positive_block_512_count_t)) (! (in_range_int11
(to_int15 x)) :pattern ((to_int15 x)) )))
;; coerce_axiom
(assert
(forall ((x (_ BitVec 64)))
(! (= (to_rep11 (of_rep11 x)) x) :pattern ((to_rep11 (of_rep11 x))) )))
;; size_int_pos
(assert (< 0 16))
(declare-fun t6 () ty)
(declare-fun nth2 ((_ BitVec 16) Int) Bool)
(declare-fun lsr2 ((_ BitVec 16) Int) (_ BitVec 16))
(declare-fun asr2 ((_ BitVec 16) Int) (_ BitVec 16))
(declare-fun lsl2 ((_ BitVec 16) Int) (_ BitVec 16))
(declare-fun to_int16 ((_ BitVec 16)) Int)
(declare-fun of_int3 (Int) (_ BitVec 16))
;; to_int_extensionality
(assert
(forall ((v (_ BitVec 16)) (vqt (_ BitVec 16)))
(=> (= (to_int16 v) (to_int16 vqt)) (= v vqt))))
(declare-fun uint_in_range2 (Int) Bool)
;; uint_in_range_def
(assert
(forall ((i Int))
(! (= (uint_in_range2 i) (and (<= 0 i) (<= i 65535))) :pattern ((uint_in_range2
i)) )))
;; Of_int_zero
(assert (= #x0000 ((_ int2bv 16) 0)))
;; Of_int_ones
(assert (= #xFFFF ((_ int2bv 16) 65535)))
;; lsr_bv_is_lsr
(assert
(forall ((x (_ BitVec 16)) (n (_ BitVec 16)))
(= (bvlshr x n) (lsr2 x (bv2int n)))))
;; asr_bv_is_asr
(assert
(forall ((x (_ BitVec 16)) (n (_ BitVec 16)))
(= (bvashr x n) (asr2 x (bv2int n)))))
;; lsl_bv_is_lsl
(assert
(forall ((x (_ BitVec 16)) (n (_ BitVec 16)))
(= (bvshl x n) (lsl2 x (bv2int n)))))
;; two_power_size_val
(assert (= (+ 65535 1) (pow2 16)))
(declare-fun bool_eq19 ((_ BitVec 16) (_ BitVec 16)) Bool)
;; bool_eq_def
(assert
(forall ((x (_ BitVec 16)) (y (_ BitVec 16)))
(! (ite (= x y) (= (bool_eq19 x y) true) (= (bool_eq19 x y) false)) :pattern (
(bool_eq19 x y)) )))
(declare-fun bool_ne3 ((_ BitVec 16) (_ BitVec 16)) Bool)
;; bool_ne_def
(assert
(forall ((x (_ BitVec 16)) (y (_ BitVec 16)))
(! (ite (not (= x y)) (= (bool_ne3 x y) true) (= (bool_ne3 x y) false)) :pattern (
(bool_ne3 x y)) )))
(declare-fun bool_lt3 ((_ BitVec 16) (_ BitVec 16)) Bool)
;; bool_lt_def
(assert
(forall ((x (_ BitVec 16)) (y (_ BitVec 16)))
(! (ite (bvult x y) (= (bool_lt3 x y) true) (= (bool_lt3 x y) false)) :pattern (
(bool_lt3 x y)) )))
(declare-fun bool_le3 ((_ BitVec 16) (_ BitVec 16)) Bool)
;; bool_le_def
(assert
(forall ((x (_ BitVec 16)) (y (_ BitVec 16)))
(! (ite (bvule x y) (= (bool_le3 x y) true) (= (bool_le3 x y) false)) :pattern (
(bool_le3 x y)) )))
(declare-fun bool_gt3 ((_ BitVec 16) (_ BitVec 16)) Bool)
;; bool_gt_def
(assert
(forall ((x (_ BitVec 16)) (y (_ BitVec 16)))
(! (ite (bvugt x y) (= (bool_gt3 x y) true) (= (bool_gt3 x y) false)) :pattern (
(bool_gt3 x y)) )))
(declare-fun bool_ge3 ((_ BitVec 16) (_ BitVec 16)) Bool)
;; bool_ge_def
(assert
(forall ((x (_ BitVec 16)) (y (_ BitVec 16)))
(! (ite (bvuge x y) (= (bool_ge3 x y) true) (= (bool_ge3 x y) false)) :pattern (
(bool_ge3 x y)) )))
(declare-fun power2 ((_ BitVec 16) Int) (_ BitVec 16))
;; Power_0
(assert (forall ((x (_ BitVec 16))) (= (power2 x 0) ((_ int2bv 16) 1))))
;; Power_1
(assert (forall ((x (_ BitVec 16))) (= (power2 x 1) x)))
;; Power_s
(assert
(forall ((x (_ BitVec 16)) (n Int))
(=> (<= 0 n) (= (power2 x (+ n 1)) (bvmul x (power2 x n))))))
;; Power_s_alt
(assert
(forall ((x (_ BitVec 16)) (n Int))
(=> (< 0 n) (= (power2 x n) (bvmul x (power2 x (- n 1)))))))
;; Power_sum
(assert
(forall ((x (_ BitVec 16)) (n Int) (m Int))
(=> (<= 0 n)
(=> (<= 0 m) (= (power2 x (+ n m)) (bvmul (power2 x n) (power2 x m)))))))
;; Power_mult
(assert
(forall ((x (_ BitVec 16)) (n Int) (m Int))
(=> (<= 0 n) (=> (<= 0 m) (= (power2 x (* n m)) (power2 (power2 x n) m))))))
;; Power_mult2
(assert
(forall ((x (_ BitVec 16)) (y (_ BitVec 16)) (n Int))
(=> (<= 0 n) (= (power2 (bvmul x y) n) (bvmul (power2 x n) (power2 y n))))))
(declare-fun bv_min2 ((_ BitVec 16) (_ BitVec 16)) (_ BitVec 16))
;; bv_min_def
(assert
(forall ((x (_ BitVec 16)) (y (_ BitVec 16)))
(! (ite (bvule x y) (= (bv_min2 x y) x) (= (bv_min2 x y) y)) :pattern (
(bv_min2 x y)) )))
(declare-fun bv_max2 ((_ BitVec 16) (_ BitVec 16)) (_ BitVec 16))
;; bv_max_def
(assert
(forall ((x (_ BitVec 16)) (y (_ BitVec 16)))
(! (ite (bvule x y) (= (bv_max2 x y) y) (= (bv_max2 x y) x)) :pattern (
(bv_max2 x y)) )))
;; bv_min_to_uint
(assert
(forall ((x (_ BitVec 16)) (y (_ BitVec 16)))
(= (bv2int (bv_min2 x y)) (ite (< (bv2int x) (bv2int y)) (bv2int x) (bv2int y)))))
;; bv_max_to_uint
(assert
(forall ((x (_ BitVec 16)) (y (_ BitVec 16)))
(= (bv2int (bv_max2 x y)) (ite (< (bv2int x) (bv2int y)) (bv2int y) (bv2int x)))))
;; size_int_pos
(assert (< 0 32))
(declare-fun t7 () ty)
(declare-fun nth3 ((_ BitVec 32) Int) Bool)
(declare-fun lsr3 ((_ BitVec 32) Int) (_ BitVec 32))
(declare-fun asr3 ((_ BitVec 32) Int) (_ BitVec 32))
(declare-fun lsl3 ((_ BitVec 32) Int) (_ BitVec 32))
(declare-fun to_int17 ((_ BitVec 32)) Int)
(declare-fun of_int4 (Int) (_ BitVec 32))
;; to_int_extensionality
(assert
(forall ((v (_ BitVec 32)) (vqt (_ BitVec 32)))
(=> (= (to_int17 v) (to_int17 vqt)) (= v vqt))))
(declare-fun uint_in_range3 (Int) Bool)
;; uint_in_range_def
(assert
(forall ((i Int))
(! (= (uint_in_range3 i) (and (<= 0 i) (<= i 4294967295))) :pattern ((uint_in_range3
i)) )))
;; Of_int_zero
(assert (= #x00000000 ((_ int2bv 32) 0)))
;; Of_int_ones
(assert (= #xFFFFFFFF ((_ int2bv 32) 4294967295)))
;; lsr_bv_is_lsr
(assert
(forall ((x (_ BitVec 32)) (n (_ BitVec 32)))
(= (bvlshr x n) (lsr3 x (bv2int n)))))
;; asr_bv_is_asr
(assert
(forall ((x (_ BitVec 32)) (n (_ BitVec 32)))
(= (bvashr x n) (asr3 x (bv2int n)))))
;; lsl_bv_is_lsl
(assert
(forall ((x (_ BitVec 32)) (n (_ BitVec 32)))
(= (bvshl x n) (lsl3 x (bv2int n)))))
;; two_power_size_val
(assert (= (+ 4294967295 1) (pow2 32)))
(declare-fun bool_eq20 ((_ BitVec 32) (_ BitVec 32)) Bool)
;; bool_eq_def
(assert
(forall ((x (_ BitVec 32)) (y (_ BitVec 32)))
(! (ite (= x y) (= (bool_eq20 x y) true) (= (bool_eq20 x y) false)) :pattern (
(bool_eq20 x y)) )))
(declare-fun bool_ne4 ((_ BitVec 32) (_ BitVec 32)) Bool)
;; bool_ne_def
(assert
(forall ((x (_ BitVec 32)) (y (_ BitVec 32)))
(! (ite (not (= x y)) (= (bool_ne4 x y) true) (= (bool_ne4 x y) false)) :pattern (
(bool_ne4 x y)) )))
(declare-fun bool_lt4 ((_ BitVec 32) (_ BitVec 32)) Bool)
;; bool_lt_def
(assert
(forall ((x (_ BitVec 32)) (y (_ BitVec 32)))
(! (ite (bvult x y) (= (bool_lt4 x y) true) (= (bool_lt4 x y) false)) :pattern (
(bool_lt4 x y)) )))
(declare-fun bool_le4 ((_ BitVec 32) (_ BitVec 32)) Bool)
;; bool_le_def
(assert
(forall ((x (_ BitVec 32)) (y (_ BitVec 32)))
(! (ite (bvule x y) (= (bool_le4 x y) true) (= (bool_le4 x y) false)) :pattern (
(bool_le4 x y)) )))
(declare-fun bool_gt4 ((_ BitVec 32) (_ BitVec 32)) Bool)
;; bool_gt_def
(assert
(forall ((x (_ BitVec 32)) (y (_ BitVec 32)))
(! (ite (bvugt x y) (= (bool_gt4 x y) true) (= (bool_gt4 x y) false)) :pattern (
(bool_gt4 x y)) )))
(declare-fun bool_ge4 ((_ BitVec 32) (_ BitVec 32)) Bool)
;; bool_ge_def
(assert
(forall ((x (_ BitVec 32)) (y (_ BitVec 32)))
(! (ite (bvuge x y) (= (bool_ge4 x y) true) (= (bool_ge4 x y) false)) :pattern (
(bool_ge4 x y)) )))
(declare-fun power3 ((_ BitVec 32) Int) (_ BitVec 32))
;; Power_0
(assert (forall ((x (_ BitVec 32))) (= (power3 x 0) ((_ int2bv 32) 1))))
;; Power_1
(assert (forall ((x (_ BitVec 32))) (= (power3 x 1) x)))
;; Power_s
(assert
(forall ((x (_ BitVec 32)) (n Int))
(=> (<= 0 n) (= (power3 x (+ n 1)) (bvmul x (power3 x n))))))
;; Power_s_alt
(assert
(forall ((x (_ BitVec 32)) (n Int))
(=> (< 0 n) (= (power3 x n) (bvmul x (power3 x (- n 1)))))))
;; Power_sum
(assert
(forall ((x (_ BitVec 32)) (n Int) (m Int))
(=> (<= 0 n)
(=> (<= 0 m) (= (power3 x (+ n m)) (bvmul (power3 x n) (power3 x m)))))))
;; Power_mult
(assert
(forall ((x (_ BitVec 32)) (n Int) (m Int))
(=> (<= 0 n) (=> (<= 0 m) (= (power3 x (* n m)) (power3 (power3 x n) m))))))
;; Power_mult2
(assert
(forall ((x (_ BitVec 32)) (y (_ BitVec 32)) (n Int))
(=> (<= 0 n) (= (power3 (bvmul x y) n) (bvmul (power3 x n) (power3 y n))))))
(declare-fun bv_min3 ((_ BitVec 32) (_ BitVec 32)) (_ BitVec 32))
;; bv_min_def
(assert
(forall ((x (_ BitVec 32)) (y (_ BitVec 32)))
(! (ite (bvule x y) (= (bv_min3 x y) x) (= (bv_min3 x y) y)) :pattern (
(bv_min3 x y)) )))
(declare-fun bv_max3 ((_ BitVec 32) (_ BitVec 32)) (_ BitVec 32))
;; bv_max_def
(assert
(forall ((x (_ BitVec 32)) (y (_ BitVec 32)))
(! (ite (bvule x y) (= (bv_max3 x y) y) (= (bv_max3 x y) x)) :pattern (
(bv_max3 x y)) )))
;; bv_min_to_uint
(assert
(forall ((x (_ BitVec 32)) (y (_ BitVec 32)))
(= (bv2int (bv_min3 x y)) (ite (< (bv2int x) (bv2int y)) (bv2int x) (bv2int y)))))
;; bv_max_to_uint
(assert
(forall ((x (_ BitVec 32)) (y (_ BitVec 32)))
(= (bv2int (bv_max3 x y)) (ite (< (bv2int x) (bv2int y)) (bv2int y) (bv2int x)))))
(declare-fun in_range13 ((_ BitVec 16)) Bool)
;; in_range_def
(assert
(forall ((x (_ BitVec 16)))
(! (= (in_range13 x)
(and (bvule ((_ int2bv 16) 0) x) (bvule x ((_ int2bv 16) 65535)))) :pattern ((in_range13
x)) )))
(declare-fun in_range_int12 (Int) Bool)
;; in_range_int_def
(assert
(forall ((x Int))
(! (= (in_range_int12 x) (and (<= 0 x) (<= x 65535))) :pattern ((in_range_int12
x)) )))
(declare-fun bool_eq21 ((_ BitVec 16) (_ BitVec 16)) Bool)
;; bool_eq_def
(assert
(forall ((x (_ BitVec 16)) (y (_ BitVec 16)))
(! (ite (= x y) (= (bool_eq21 x y) true) (= (bool_eq21 x y) false)) :pattern (
(bool_eq21 x y)) )))
(declare-fun attr__ATTRIBUTE_IMAGE13 ((_ BitVec 16)) uni)
;; attr__ATTRIBUTE_IMAGE_sort
(assert
(forall ((x (_ BitVec 16))) (sort us_image (attr__ATTRIBUTE_IMAGE13 x))))
(declare-fun attr__ATTRIBUTE_VALUE__pre_check13 (uni) Bool)
(declare-fun attr__ATTRIBUTE_VALUE13 (uni) (_ BitVec 16))
(declare-fun to_rep12 (u16) (_ BitVec 16))
(declare-fun of_rep12 ((_ BitVec 16)) u16)
(declare-fun user_eq18 (u16 u16) Bool)
(declare-fun dummy18 () u16)
;; inversion_axiom
(assert
(forall ((x u16))
(! (= (of_rep12 (to_rep12 x)) x) :pattern ((to_rep12 x)) )))
;; range_axiom
(assert
(forall ((x u16)) (! (in_range13 (to_rep12 x)) :pattern ((to_rep12 x)) )))
(declare-fun to_int18 (u16) Int)
;; to_int_def
(assert
(forall ((x u16))
(! (= (to_int18 x) (bv2int (to_rep12 x))) :pattern ((to_int18 x)) )))
;; range_int_axiom
(assert
(forall ((x u16)) (! (in_range_int12
(to_int18 x)) :pattern ((to_int18 x)) )))
;; coerce_axiom
(assert
(forall ((x (_ BitVec 16)))
(! (= (to_rep12 (of_rep12 x)) x) :pattern ((to_rep12 (of_rep12 x))) )))
(declare-fun in_range14 ((_ BitVec 32)) Bool)
;; in_range_def
(assert
(forall ((x (_ BitVec 32)))
(! (= (in_range14 x)
(and (bvule ((_ int2bv 32) 0) x) (bvule x ((_ int2bv 32) 4294967295)))) :pattern ((in_range14
x)) )))
(declare-fun in_range_int13 (Int) Bool)
;; in_range_int_def
(assert
(forall ((x Int))
(! (= (in_range_int13 x) (and (<= 0 x) (<= x 4294967295))) :pattern ((in_range_int13
x)) )))
(declare-fun bool_eq22 ((_ BitVec 32) (_ BitVec 32)) Bool)
;; bool_eq_def
(assert
(forall ((x (_ BitVec 32)) (y (_ BitVec 32)))
(! (ite (= x y) (= (bool_eq22 x y) true) (= (bool_eq22 x y) false)) :pattern (
(bool_eq22 x y)) )))
(declare-fun attr__ATTRIBUTE_IMAGE14 ((_ BitVec 32)) uni)
;; attr__ATTRIBUTE_IMAGE_sort
(assert
(forall ((x (_ BitVec 32))) (sort us_image (attr__ATTRIBUTE_IMAGE14 x))))
(declare-fun attr__ATTRIBUTE_VALUE__pre_check14 (uni) Bool)
(declare-fun attr__ATTRIBUTE_VALUE14 (uni) (_ BitVec 32))
(declare-fun to_rep13 (u32) (_ BitVec 32))
(declare-fun of_rep13 ((_ BitVec 32)) u32)
(declare-fun user_eq19 (u32 u32) Bool)
(declare-fun dummy19 () u32)
;; inversion_axiom
(assert
(forall ((x u32))
(! (= (of_rep13 (to_rep13 x)) x) :pattern ((to_rep13 x)) )))
;; range_axiom
(assert
(forall ((x u32)) (! (in_range14 (to_rep13 x)) :pattern ((to_rep13 x)) )))
(declare-fun to_int19 (u32) Int)
;; to_int_def
(assert
(forall ((x u32))
(! (= (to_int19 x) (bv2int (to_rep13 x))) :pattern ((to_int19 x)) )))
;; range_int_axiom
(assert
(forall ((x u32)) (! (in_range_int13
(to_int19 x)) :pattern ((to_int19 x)) )))
;; coerce_axiom
(assert
(forall ((x (_ BitVec 32)))
(! (= (to_rep13 (of_rep13 x)) x) :pattern ((to_rep13 (of_rep13 x))) )))
(declare-fun in_range15 ((_ BitVec 8)) Bool)
;; in_range_def
(assert
(forall ((x (_ BitVec 8)))
(! (= (in_range15 x)
(and (bvule ((_ int2bv 8) 0) x) (bvule x ((_ int2bv 8) 127)))) :pattern ((in_range15
x)) )))
(declare-fun in_range_int14 (Int) Bool)
;; in_range_int_def
(assert
(forall ((x Int))
(! (= (in_range_int14 x) (and (<= 0 x) (<= x 127))) :pattern ((in_range_int14
x)) )))
(declare-fun bool_eq23 ((_ BitVec 8) (_ BitVec 8)) Bool)
;; bool_eq_def
(assert
(forall ((x (_ BitVec 8)) (y (_ BitVec 8)))
(! (ite (= x y) (= (bool_eq23 x y) true) (= (bool_eq23 x y) false)) :pattern (
(bool_eq23 x y)) )))
(declare-fun attr__ATTRIBUTE_IMAGE15 ((_ BitVec 8)) uni)
;; attr__ATTRIBUTE_IMAGE_sort
(assert
(forall ((x (_ BitVec 8))) (sort us_image (attr__ATTRIBUTE_IMAGE15 x))))
(declare-fun attr__ATTRIBUTE_VALUE__pre_check15 (uni) Bool)
(declare-fun attr__ATTRIBUTE_VALUE15 (uni) (_ BitVec 8))
(declare-fun to_rep14 (u7) (_ BitVec 8))
(declare-fun of_rep14 ((_ BitVec 8)) u7)
(declare-fun user_eq20 (u7 u7) Bool)
(declare-fun dummy20 () u7)
;; inversion_axiom
(assert
(forall ((x u7))
(! (= (of_rep14 (to_rep14 x)) x) :pattern ((to_rep14 x)) )))
;; range_axiom
(assert
(forall ((x u7)) (! (in_range15 (to_rep14 x)) :pattern ((to_rep14 x)) )))
(declare-fun to_int20 (u7) Int)
;; to_int_def
(assert
(forall ((x u7))
(! (= (to_int20 x) (bv2int (to_rep14 x))) :pattern ((to_int20 x)) )))
;; range_int_axiom
(assert
(forall ((x u7)) (! (in_range_int14
(to_int20 x)) :pattern ((to_int20 x)) )))
;; coerce_axiom
(assert
(forall ((x (_ BitVec 8)))
(! (let ((y (bvurem x ((_ int2bv 8) 128))))
(=> (in_range15 y) (= (to_rep14 (of_rep14 x)) y))) :pattern ((to_rep14
(of_rep14
x))) )))
(declare-fun in_range16 ((_ BitVec 8)) Bool)
;; in_range_def
(assert
(forall ((x (_ BitVec 8)))
(! (= (in_range16 x)
(and (bvule ((_ int2bv 8) 0) x) (bvule x ((_ int2bv 8) 63)))) :pattern ((in_range16
x)) )))
(declare-fun in_range_int15 (Int) Bool)
;; in_range_int_def
(assert
(forall ((x Int))
(! (= (in_range_int15 x) (and (<= 0 x) (<= x 63))) :pattern ((in_range_int15
x)) )))
(declare-fun bool_eq24 ((_ BitVec 8) (_ BitVec 8)) Bool)
;; bool_eq_def
(assert
(forall ((x (_ BitVec 8)) (y (_ BitVec 8)))
(! (ite (= x y) (= (bool_eq24 x y) true) (= (bool_eq24 x y) false)) :pattern (
(bool_eq24 x y)) )))
(declare-fun attr__ATTRIBUTE_IMAGE16 ((_ BitVec 8)) uni)
;; attr__ATTRIBUTE_IMAGE_sort
(assert
(forall ((x (_ BitVec 8))) (sort us_image (attr__ATTRIBUTE_IMAGE16 x))))
(declare-fun attr__ATTRIBUTE_VALUE__pre_check16 (uni) Bool)
(declare-fun attr__ATTRIBUTE_VALUE16 (uni) (_ BitVec 8))
(declare-fun to_rep15 (u6) (_ BitVec 8))
(declare-fun of_rep15 ((_ BitVec 8)) u6)
(declare-fun user_eq21 (u6 u6) Bool)
(declare-fun dummy21 () u6)
;; inversion_axiom
(assert
(forall ((x u6))
(! (= (of_rep15 (to_rep15 x)) x) :pattern ((to_rep15 x)) )))
;; range_axiom
(assert
(forall ((x u6)) (! (in_range16 (to_rep15 x)) :pattern ((to_rep15 x)) )))
(declare-fun to_int21 (u6) Int)
;; to_int_def
(assert
(forall ((x u6))
(! (= (to_int21 x) (bv2int (to_rep15 x))) :pattern ((to_int21 x)) )))
;; range_int_axiom
(assert
(forall ((x u6)) (! (in_range_int15
(to_int21 x)) :pattern ((to_int21 x)) )))
;; coerce_axiom
(assert
(forall ((x (_ BitVec 8)))
(! (let ((y (bvurem x ((_ int2bv 8) 64))))
(=> (in_range16 y) (= (to_rep15 (of_rep15 x)) y))) :pattern ((to_rep15
(of_rep15
x))) )))
(declare-fun mk___split_fields (u64 u32 u16 u7 Bool u6 Bool
Bool) us_split_fields)
(declare-fun rec__byte_count_lsb (us_split_fields) u64)
;; rec__byte_count_lsb_def
(assert
(forall ((u u64) (u1 u32) (u2 u16) (u3 u7) (u4 Bool) (u5 u6) (u8 Bool)
(u9 Bool))
(= (rec__byte_count_lsb (mk___split_fields u u1 u2 u3 u4 u5 u8 u9)) u)))
(declare-fun rec__byte_count_msb (us_split_fields) u32)
;; rec__byte_count_msb_def
(assert
(forall ((u u64) (u1 u32) (u2 u16) (u3 u7) (u4 Bool) (u5 u6) (u8 Bool)
(u9 Bool))
(= (rec__byte_count_msb (mk___split_fields u u1 u2 u3 u4 u5 u8 u9)) u1)))
(declare-fun rec__reserved (us_split_fields) u16)
;; rec__reserved_def
(assert
(forall ((u u64) (u1 u32) (u2 u16) (u3 u7) (u4 Bool) (u5 u6) (u8 Bool)
(u9 Bool))
(= (rec__reserved (mk___split_fields u u1 u2 u3 u4 u5 u8 u9)) u2)))
(declare-fun rec__tree_level (us_split_fields) u7)
;; rec__tree_level_def
(assert
(forall ((u u64) (u1 u32) (u2 u16) (u3 u7) (u4 Bool) (u5 u6) (u8 Bool)
(u9 Bool))
(= (rec__tree_level (mk___split_fields u u1 u2 u3 u4 u5 u8 u9)) u3)))
(declare-fun rec__bit_pad (us_split_fields) Bool)
;; rec__bit_pad_def
(assert
(forall ((u u64) (u1 u32) (u2 u16) (u3 u7) (u4 Bool) (u5 u6) (u8 Bool)
(u9 Bool))
(= (rec__bit_pad (mk___split_fields u u1 u2 u3 u4 u5 u8 u9)) u4)))
(declare-fun rec__field_type (us_split_fields) u6)
;; rec__field_type_def
(assert
(forall ((u u64) (u1 u32) (u2 u16) (u3 u7) (u4 Bool) (u5 u6) (u8 Bool)
(u9 Bool))
(= (rec__field_type (mk___split_fields u u1 u2 u3 u4 u5 u8 u9)) u5)))
(declare-fun rec__first_block (us_split_fields) Bool)
;; rec__first_block_def
(assert
(forall ((u u64) (u1 u32) (u2 u16) (u3 u7) (u4 Bool) (u5 u6) (u8 Bool)
(u9 Bool))
(= (rec__first_block (mk___split_fields u u1 u2 u3 u4 u5 u8 u9)) u8)))
(declare-fun rec__final_block (us_split_fields) Bool)
;; rec__final_block_def
(assert
(forall ((u u64) (u1 u32) (u2 u16) (u3 u7) (u4 Bool) (u5 u6) (u8 Bool)
(u9 Bool))
(= (rec__final_block (mk___split_fields u u1 u2 u3 u4 u5 u8 u9)) u9)))
(declare-fun mk_tweak_value (us_split_fields) tweak_value)
(declare-fun us_split_fields2 (tweak_value) us_split_fields)
;; __split_fields_def
(assert
(forall ((u us_split_fields)) (= (us_split_fields2 (mk_tweak_value u)) u)))
(declare-fun bool_eq25 (tweak_value tweak_value) Bool)
;; bool_eq_def
(assert
(forall ((a tweak_value) (b tweak_value))
(! (ite (and
(and
(and
(and
(and
(and
(and
(= (to_rep1 (rec__byte_count_lsb (us_split_fields2 a))) (to_rep1
(rec__byte_count_lsb
(us_split_fields2
b))))
(= (to_rep13 (rec__byte_count_msb (us_split_fields2 a))) (to_rep13
(rec__byte_count_msb
(us_split_fields2
b)))))
(= (to_rep12 (rec__reserved (us_split_fields2 a))) (to_rep12
(rec__reserved
(us_split_fields2
b)))))
(= (to_rep14 (rec__tree_level (us_split_fields2 a))) (to_rep14
(rec__tree_level
(us_split_fields2
b)))))
(= (rec__bit_pad (us_split_fields2 a)) (rec__bit_pad
(us_split_fields2 b))))
(= (to_rep15 (rec__field_type (us_split_fields2 a))) (to_rep15
(rec__field_type
(us_split_fields2
b)))))
(= (rec__first_block (us_split_fields2 a)) (rec__first_block
(us_split_fields2 b))))
(= (rec__final_block (us_split_fields2 a)) (rec__final_block
(us_split_fields2 b))))
(= (bool_eq25 a b) true) (= (bool_eq25 a b) false)) :pattern ((bool_eq25
a b)) )))
(declare-fun user_eq22 (tweak_value tweak_value) Bool)
(declare-fun value__size6 () Int)
(declare-fun object__size6 (tweak_value) Int)
;; value__size_axiom
(assert (<= 0 value__size6))
;; object__size_axiom
(assert (forall ((a tweak_value)) (<= 0 (object__size6 a))))
(declare-fun dummy22 () tweak_value)
(declare-fun mk___split_fields1 (tweak_value hash_bit_length
u64) us_split_fields3)
(declare-fun rec__tweak_words (us_split_fields3) tweak_value)
;; rec__tweak_words_def
(assert
(forall ((u tweak_value) (u1 hash_bit_length) (u2 u64))
(= (rec__tweak_words (mk___split_fields1 u u1 u2)) u)))
(declare-fun rec__hash_bit_len (us_split_fields3) hash_bit_length)
;; rec__hash_bit_len_def
(assert
(forall ((u tweak_value) (u1 hash_bit_length) (u2 u64))
(= (rec__hash_bit_len (mk___split_fields1 u u1 u2)) u1)))
(declare-fun rec__byte_count (us_split_fields3) u64)
;; rec__byte_count_def
(assert
(forall ((u tweak_value) (u1 hash_bit_length) (u2 u64))
(= (rec__byte_count (mk___split_fields1 u u1 u2)) u2)))
(declare-fun mk_context_header (us_split_fields3) context_header)
(declare-fun us_split_fields5 (context_header) us_split_fields3)
;; __split_fields_def
(assert
(forall ((u us_split_fields3))
(= (us_split_fields5 (mk_context_header u)) u)))
(declare-fun bool_eq26 (context_header context_header) Bool)
;; bool_eq_def
(assert
(forall ((a context_header) (b context_header))
(! (ite (and
(and
(= (bool_eq25 (rec__tweak_words (us_split_fields5 a))
(rec__tweak_words (us_split_fields5 b))) true)
(= (to_rep7 (rec__hash_bit_len (us_split_fields5 a))) (to_rep7
(rec__hash_bit_len
(us_split_fields5
b)))))
(= (to_rep1 (rec__byte_count (us_split_fields5 a))) (to_rep1
(rec__byte_count
(us_split_fields5
b)))))
(= (bool_eq26 a b) true) (= (bool_eq26 a b) false)) :pattern ((bool_eq26
a b)) )))
(declare-fun user_eq23 (context_header context_header) Bool)
(declare-fun value__size7 () Int)
(declare-fun object__size7 (context_header) Int)
;; value__size_axiom
(assert (<= 0 value__size7))
;; object__size_axiom
(assert (forall ((a context_header)) (<= 0 (object__size7 a))))
(declare-fun dummy23 () context_header)
(declare-fun dummy15 () (Array (_ BitVec 64) u64))
(declare-fun value__size5 () Int)
(declare-fun object__size5 ((Array (_ BitVec 64) u64)) Int)
;; value__size_axiom
(assert (<= 0 value__size5))
;; object__size_axiom
(assert (forall ((a (Array (_ BitVec 64) u64))) (<= 0 (object__size5 a))))
(declare-fun user_eq15 ((Array (_ BitVec 64) u64)
(Array (_ BitVec 64) u64)) Bool)
;; compare_def
(assert
(forall ((a (Array (_ BitVec 64) u64)) (b (Array (_ BitVec 64) u64)))
(forall ((a_first (_ BitVec 64)) (a_last (_ BitVec 64))
(b_first (_ BitVec 64)) (b_last (_ BitVec 64)))
(! (and
(= (= (compare2 a a_first a_last b b_first b_last) 0)
(= (bool_eq34 a a_first a_last b b_first b_last) true))
(and
(= (< (compare2 a a_first a_last b b_first b_last) 0)
(exists ((i (_ BitVec 64)) (j (_ BitVec 64)))
(and (bvule i a_last)
(and (bvult j b_last)
(and (= (bool_eq34 a a_first i b b_first j) true)
(or (= i a_last)
(and (bvult i a_last)
(bvult (to_rep1 (select a (bvadd i ((_ int2bv 64) 1)))) (to_rep1
(select b (bvadd j ((_ int2bv 64) 1))))))))))))
(= (< 0 (compare2 a a_first a_last b b_first b_last))
(exists ((i (_ BitVec 64)) (j (_ BitVec 64)))
(and (bvule i b_last)
(and (bvult j a_last)
(and (= (bool_eq34 a a_first j b b_first i) true)
(or (= i b_last)
(and (bvult i b_last)
(bvugt (to_rep1 (select a (bvadd j ((_ int2bv 64) 1)))) (to_rep1
(select b (bvadd i ((_ int2bv 64) 1)))))))))))))) :pattern (
(compare2 a a_first a_last b b_first b_last)) ))))
(declare-fun mk___split_fields2 (context_header (Array (_ BitVec 64) u64)
(Array (_ BitVec 64) byte)) us_split_fields6)
(declare-fun rec__h (us_split_fields6) context_header)
;; rec__h_def
(assert
(forall ((u context_header) (u1 (Array (_ BitVec 64) u64))
(u2 (Array (_ BitVec 64) byte)))
(= (rec__h (mk___split_fields2 u u1 u2)) u)))
(declare-fun rec__x (us_split_fields6) (Array (_ BitVec 64) u64))
;; rec__x_def
(assert
(forall ((u context_header) (u1 (Array (_ BitVec 64) u64))
(u2 (Array (_ BitVec 64) byte)))
(= (rec__x (mk___split_fields2 u u1 u2)) u1)))
(declare-fun rec__b (us_split_fields6) (Array (_ BitVec 64) byte))
;; rec__b_def
(assert
(forall ((u context_header) (u1 (Array (_ BitVec 64) u64))
(u2 (Array (_ BitVec 64) byte)))
(= (rec__b (mk___split_fields2 u u1 u2)) u2)))
(declare-fun mk_skein_512_context (us_split_fields6) skein_512_context)
(declare-fun us_split_fields8 (skein_512_context) us_split_fields6)
;; __split_fields_def
(assert
(forall ((u us_split_fields6))
(= (us_split_fields8 (mk_skein_512_context u)) u)))
(declare-fun bool_eq27 (skein_512_context skein_512_context) Bool)
;; bool_eq_def
(assert
(forall ((a skein_512_context) (b skein_512_context))
(! (ite (and
(and
(= (bool_eq26 (rec__h (us_split_fields8 a))
(rec__h (us_split_fields8 b))) true)
(= (bool_eq34 (rec__x (us_split_fields8 a)) ((_ int2bv 64) 0)
((_ int2bv 64) 7) (rec__x (us_split_fields8 b))
((_ int2bv 64) 0) ((_ int2bv 64) 7)) true))
(= (bool_eq33 (rec__b (us_split_fields8 a)) ((_ int2bv 64) 0)
((_ int2bv 64) 63) (rec__b (us_split_fields8 b))
((_ int2bv 64) 0) ((_ int2bv 64) 63)) true))
(= (bool_eq27 a b) true) (= (bool_eq27 a b) false)) :pattern ((bool_eq27
a b)) )))
(declare-fun user_eq25 (skein_512_context skein_512_context) Bool)
(declare-fun value__size9 () Int)
(declare-fun object__size9 (skein_512_context) Int)
;; value__size_axiom
(assert (<= 0 value__size9))
;; object__size_axiom
(assert (forall ((a skein_512_context)) (<= 0 (object__size9 a))))
(declare-fun dummy25 () skein_512_context)
(declare-fun add_in_range ((_ BitVec 64) (_ BitVec 64)) Bool)
;; add_in_range__def_axiom
(assert
(forall ((x (_ BitVec 64)) (y (_ BitVec 64)))
(! (= (= (add_in_range x y) true)
(bvule y (bvsub ((_ int2bv 64) 18446744073709551615) x))) :pattern (
(add_in_range x y)) )))
(declare-fun hash_bit_len_of (skein_512_context) (_ BitVec 64))
;; hash_bit_len_of__post_axiom
(assert
(forall ((ctx1 skein_512_context)) (! (in_range8
(hash_bit_len_of ctx1)) :pattern ((hash_bit_len_of ctx1)) )))
;; hash_bit_len_of__def_axiom
(assert
(forall ((ctx1 skein_512_context))
(! (= (hash_bit_len_of ctx1) (to_rep7
(rec__hash_bit_len
(us_split_fields5
(rec__h (us_split_fields8 ctx1)))))) :pattern (
(hash_bit_len_of ctx1)) )))
(declare-fun byte_count_of (skein_512_context) (_ BitVec 64))
;; byte_count_of__post_axiom
(assert
(forall ((ctx1 skein_512_context)) (! (in_range2
(byte_count_of ctx1)) :pattern ((byte_count_of ctx1)) )))
;; byte_count_of__def_axiom
(assert
(forall ((ctx1 skein_512_context))
(! (= (byte_count_of ctx1) (to_rep1
(rec__byte_count
(us_split_fields5
(rec__h (us_split_fields8 ctx1)))))) :pattern (
(byte_count_of ctx1)) )))
(declare-fun attr__ATTRIBUTE_ADDRESS23 () Int)
(declare-fun msg () us_t)
(declare-fun attr__ATTRIBUTE_ADDRESS24 () Int)
(declare-fun attr__ATTRIBUTE_ADDRESS25 () Int)
(declare-fun attr__ATTRIBUTE_ADDRESS26 () Int)
(declare-fun attr__ATTRIBUTE_ADDRESS27 () Int)
(declare-fun attr__ATTRIBUTE_ADDRESS28 () Int)
(declare-fun attr__ATTRIBUTE_ADDRESS29 () Int)
(declare-fun c232b () (_ BitVec 64))
(declare-fun attr__ATTRIBUTE_ADDRESS30 () Int)
(declare-fun attr__ATTRIBUTE_ADDRESS31 () Int)
(declare-fun attr__ATTRIBUTE_ADDRESS32 () Int)
(declare-fun attr__ATTRIBUTE_ADDRESS33 () Int)
(declare-fun c234b () (_ BitVec 64))
(declare-fun attr__ATTRIBUTE_ADDRESS34 () Int)
(declare-fun attr__ATTRIBUTE_ADDRESS35 () Int)
(declare-fun attr__ATTRIBUTE_ADDRESS36 () Int)
(declare-fun attr__ATTRIBUTE_ADDRESS37 () Int)
(assert
;; WP_parameter_def3
;; File "/home/kanig/dev/spark2014/testsuite/gnatprove/temp/tmp-test-sparkskein-22763/src/gnatprove/skein/../skein.mlw", line 29657, characters 5-8
(not
(forall ((ctx__split_fields u64) (ctx__split_fields1 u32)
(ctx__split_fields2 u16) (ctx__split_fields3 u7) (ctx__split_fields4 Bool)
(ctx__split_fields5 u6) (ctx__split_fields6 Bool) (ctx__split_fields7 Bool)
(ctx__split_fields8 hash_bit_length) (ctx__split_fields9 u64)
(ctx__split_fields10 (Array (_ BitVec 64) u64))
(ctx__split_fields11 (Array (_ BitVec 64) byte))
(msg_byte_count (_ BitVec 64)) (n (_ BitVec 64))
(block_count1 (_ BitVec 64)) (current_msg_offset (_ BitVec 64))
(bytes_hashed (_ BitVec 64)) (tmp_b (Array (_ BitVec 64) byte))
(src (_ BitVec 64)) (dst (_ BitVec 64)) (final_dst (_ BitVec 64))
(final_src (_ BitVec 64)) (src1 (_ BitVec 64)) (dst1 (_ BitVec 64))
(final_dst1 (_ BitVec 64)) (final_src1 (_ BitVec 64)) (o (_ BitVec 64))
(o1 (_ BitVec 64)) (o2 (_ BitVec 64))
(temp___standard__skein_126 (_ BitVec 64))
(temp___standard__skein_127 (_ BitVec 64)) (o3 (_ BitVec 64)) (o4 byte)
(o5 (_ BitVec 8)) (o6 byte) (o7 (Array (_ BitVec 64) byte)) (o8 u64)
(o9 u32) (o10 u16) (o11 u7) (o12 Bool) (o13 u6) (o14 Bool) (o15 Bool)
(o16 hash_bit_length) (o17 u64) (o18 (Array (_ BitVec 64) u64))
(o19 (Array (_ BitVec 64) byte)) (temp___standard__skein_123 u64)
(temp___standard__skein_1231 u32) (temp___standard__skein_1232 u16)
(temp___standard__skein_1233 u7) (temp___standard__skein_1234 Bool)
(temp___standard__skein_1235 u6) (temp___standard__skein_1236 Bool)
(temp___standard__skein_1237 Bool)
(temp___standard__skein_1238 hash_bit_length)
(temp___standard__skein_1239 u64)
(temp___standard__skein_12310 (Array (_ BitVec 64) u64))
(temp___standard__skein_12311 (Array (_ BitVec 64) byte)) (o20 u64)
(o21 u64) (o22 u32) (o23 u16) (o24 u7) (o25 Bool) (o26 u6) (o27 Bool)
(o28 Bool) (o29 hash_bit_length) (o30 u64) (o31 u64) (o32 u32) (o33 u16)
(o34 u7) (o35 Bool) (o36 u6) (o37 Bool) (o38 Bool) (o39 hash_bit_length)
(o40 u64) (o41 u64) (o42 u32) (o43 u16) (o44 u7) (o45 Bool) (o46 u6)
(o47 Bool) (o48 Bool) (o49 hash_bit_length) (o50 u64)
(o51 (Array (_ BitVec 64) u64)) (o52 (Array (_ BitVec 64) byte))
(temp___standard__skein_130 u64) (temp___standard__skein_1301 u32)
(temp___standard__skein_1302 u16) (temp___standard__skein_1303 u7)
(temp___standard__skein_1304 Bool) (temp___standard__skein_1305 u6)
(temp___standard__skein_1306 Bool) (temp___standard__skein_1307 Bool)
(temp___standard__skein_1308 hash_bit_length)
(temp___standard__skein_1309 u64)
(temp___standard__skein_13010 (Array (_ BitVec 64) u64))
(temp___standard__skein_13011 (Array (_ BitVec 64) byte)) (o53 u64)
(o54 u64) (o55 u32) (o56 u16) (o57 u7) (o58 Bool) (o59 u6) (o60 Bool)
(o61 Bool) (o62 hash_bit_length) (o63 u64) (o64 u64) (o65 u32) (o66 u16)
(o67 u7) (o68 Bool) (o69 u6) (o70 Bool) (o71 Bool) (o72 hash_bit_length)
(o73 u64) (o74 u64) (o75 u32) (o76 u16) (o77 u7) (o78 Bool) (o79 u6)
(o80 Bool) (o81 Bool) (o82 hash_bit_length) (o83 u64)
(o84 (Array (_ BitVec 64) u64)) (o85 (Array (_ BitVec 64) byte))
(temp___standard__skein_133 u64) (temp___standard__skein_1331 u32)
(temp___standard__skein_1332 u16) (temp___standard__skein_1333 u7)
(temp___standard__skein_1334 Bool) (temp___standard__skein_1335 u6)
(temp___standard__skein_1336 Bool) (temp___standard__skein_1337 Bool)
(temp___standard__skein_1338 hash_bit_length)
(temp___standard__skein_1339 u64)
(temp___standard__skein_13310 (Array (_ BitVec 64) u64))
(temp___standard__skein_13311 (Array (_ BitVec 64) byte))
(o86 (_ BitVec 64)) (o87 (_ BitVec 64)) (o88 (_ BitVec 64))
(temp___standard__skein_139 (_ BitVec 64))
(temp___standard__skein_140 (_ BitVec 64)) (o89 (_ BitVec 64)) (o90 byte)
(o91 (_ BitVec 8)) (o92 byte) (o93 (Array (_ BitVec 64) byte)) (o94 u64)
(o95 u32) (o96 u16) (o97 u7) (o98 Bool) (o99 u6) (o100 Bool) (o101 Bool)
(o102 hash_bit_length) (o103 u64) (o104 (Array (_ BitVec 64) u64))
(o105 (Array (_ BitVec 64) byte)) (temp___standard__skein_136 u64)
(temp___standard__skein_1361 u32) (temp___standard__skein_1362 u16)
(temp___standard__skein_1363 u7) (temp___standard__skein_1364 Bool)
(temp___standard__skein_1365 u6) (temp___standard__skein_1366 Bool)
(temp___standard__skein_1367 Bool)
(temp___standard__skein_1368 hash_bit_length)
(temp___standard__skein_1369 u64)
(temp___standard__skein_13610 (Array (_ BitVec 64) u64))
(temp___standard__skein_13611 (Array (_ BitVec 64) byte)) (o106 u64)
(o107 u64) (o108 u32) (o109 u16) (o110 u7) (o111 Bool) (o112 u6)
(o113 Bool) (o114 Bool) (o115 hash_bit_length) (o116 u64) (o117 u64)
(o118 u32) (o119 u16) (o120 u7) (o121 Bool) (o122 u6) (o123 Bool)
(o124 Bool) (o125 hash_bit_length) (o126 u64) (o127 u64) (o128 u32)
(o129 u16) (o130 u7) (o131 Bool) (o132 u6) (o133 Bool) (o134 Bool)
(o135 hash_bit_length) (o136 u64) (o137 (Array (_ BitVec 64) u64))
(o138 (Array (_ BitVec 64) byte)) (temp___standard__skein_143 u64)
(temp___standard__skein_1431 u32) (temp___standard__skein_1432 u16)
(temp___standard__skein_1433 u7) (temp___standard__skein_1434 Bool)
(temp___standard__skein_1435 u6) (temp___standard__skein_1436 Bool)
(temp___standard__skein_1437 Bool)
(temp___standard__skein_1438 hash_bit_length)
(temp___standard__skein_1439 u64)
(temp___standard__skein_14310 (Array (_ BitVec 64) u64))
(temp___standard__skein_14311 (Array (_ BitVec 64) byte))
(ctx__split_fields12 u64) (ctx__split_fields13 u32)
(ctx__split_fields14 u16) (ctx__split_fields15 u7)
(ctx__split_fields16 Bool) (ctx__split_fields17 u6)
(ctx__split_fields18 Bool) (ctx__split_fields19 Bool)
(ctx__split_fields20 hash_bit_length) (ctx__split_fields21 u64)
(ctx__split_fields22 (Array (_ BitVec 64) u64))
(ctx__split_fields23 (Array (_ BitVec 64) byte)) (n1 (_ BitVec 64))
(block_count2 (_ BitVec 64)) (bytes_hashed1 (_ BitVec 64))
(tmp_b1 (Array (_ BitVec 64) byte)) (src2 (_ BitVec 64))
(dst2 (_ BitVec 64)) (final_dst2 (_ BitVec 64)) (final_src2 (_ BitVec 64))
(src3 (_ BitVec 64)) (dst3 (_ BitVec 64)) (final_dst3 (_ BitVec 64))
(final_src3 (_ BitVec 64)) (msg_byte_count1 (_ BitVec 64))
(current_msg_offset1 (_ BitVec 64)) (n2 (_ BitVec 64)) (src4 (_ BitVec 64))
(dst4 (_ BitVec 64)) (final_dst4 (_ BitVec 64)) (final_src4 (_ BitVec 64))
(ctx__split_fields24 u64) (ctx__split_fields25 u32)
(ctx__split_fields26 u16) (ctx__split_fields27 u7)
(ctx__split_fields28 Bool) (ctx__split_fields29 u6)
(ctx__split_fields30 Bool) (ctx__split_fields31 Bool)
(ctx__split_fields32 hash_bit_length) (ctx__split_fields33 u64)
(ctx__split_fields34 (Array (_ BitVec 64) u64))
(ctx__split_fields35 (Array (_ BitVec 64) byte)) (ctx__split_fields36 u64)
(ctx__split_fields37 u32) (ctx__split_fields38 u16)
(ctx__split_fields39 u7) (ctx__split_fields40 Bool)
(ctx__split_fields41 u6) (ctx__split_fields42 Bool)
(ctx__split_fields43 Bool) (ctx__split_fields44 hash_bit_length)
(ctx__split_fields45 u64) (ctx__split_fields46 (Array (_ BitVec 64) u64))
(ctx__split_fields47 (Array (_ BitVec 64) byte)) (src5 (_ BitVec 64))
(dst5 (_ BitVec 64)) (src6 (_ BitVec 64)) (dst6 (_ BitVec 64))
(src7 (_ BitVec 64)) (dst7 (_ BitVec 64)) (ctx__split_fields48 u64)
(ctx__split_fields49 u32) (ctx__split_fields50 u16)
(ctx__split_fields51 u7) (ctx__split_fields52 Bool)
(ctx__split_fields53 u6) (ctx__split_fields54 Bool)
(ctx__split_fields55 Bool) (ctx__split_fields56 hash_bit_length)
(ctx__split_fields57 u64) (ctx__split_fields58 (Array (_ BitVec 64) u64))
(ctx__split_fields59 (Array (_ BitVec 64) byte)) (src8 (_ BitVec 64))
(dst8 (_ BitVec 64)) (ctx__split_fields60 u64) (ctx__split_fields61 u32)
(ctx__split_fields62 u16) (ctx__split_fields63 u7)
(ctx__split_fields64 Bool) (ctx__split_fields65 u6)
(ctx__split_fields66 Bool) (ctx__split_fields67 Bool)
(ctx__split_fields68 hash_bit_length) (ctx__split_fields69 u64)
(ctx__split_fields70 (Array (_ BitVec 64) u64))
(ctx__split_fields71 (Array (_ BitVec 64) byte)) (src9 (_ BitVec 64))
(dst9 (_ BitVec 64)) (ctx__split_fields72 u64) (ctx__split_fields73 u32)
(ctx__split_fields74 u16) (ctx__split_fields75 u7)
(ctx__split_fields76 Bool) (ctx__split_fields77 u6)
(ctx__split_fields78 Bool) (ctx__split_fields79 Bool)
(ctx__split_fields80 hash_bit_length) (ctx__split_fields81 u64)
(ctx__split_fields82 (Array (_ BitVec 64) u64))
(ctx__split_fields83 (Array (_ BitVec 64) byte))
(msg_byte_count2 (_ BitVec 64)) (current_msg_offset2 (_ BitVec 64))
(tmp_b2 (Array (_ BitVec 64) byte)) (ctx__split_fields84 u64)
(ctx__split_fields85 u32) (ctx__split_fields86 u16)
(ctx__split_fields87 u7) (ctx__split_fields88 Bool)
(ctx__split_fields89 u6) (ctx__split_fields90 Bool)
(ctx__split_fields91 Bool) (ctx__split_fields92 hash_bit_length)
(ctx__split_fields93 u64) (ctx__split_fields94 (Array (_ BitVec 64) u64))
(ctx__split_fields95 (Array (_ BitVec 64) byte)) (ctx__split_fields96 u64)
(ctx__split_fields97 u32) (ctx__split_fields98 u16)
(ctx__split_fields99 u7) (ctx__split_fields100 Bool)
(ctx__split_fields101 u6) (ctx__split_fields102 Bool)
(ctx__split_fields103 Bool) (ctx__split_fields104 hash_bit_length)
(ctx__split_fields105 u64) (ctx__split_fields106 (Array (_ BitVec 64) u64))
(ctx__split_fields107 (Array (_ BitVec 64) byte))
(block_count3 (_ BitVec 64)) (ctx__split_fields108 u64)
(ctx__split_fields109 u32) (ctx__split_fields110 u16)
(ctx__split_fields111 u7) (ctx__split_fields112 Bool)
(ctx__split_fields113 u6) (ctx__split_fields114 Bool)
(ctx__split_fields115 Bool) (ctx__split_fields116 hash_bit_length)
(ctx__split_fields117 u64) (ctx__split_fields118 (Array (_ BitVec 64) u64))
(ctx__split_fields119 (Array (_ BitVec 64) byte))
(bytes_hashed2 (_ BitVec 64)) (msg_byte_count3 (_ BitVec 64))
(current_msg_offset3 (_ BitVec 64)) (src10 (_ BitVec 64))
(dst10 (_ BitVec 64)) (final_dst5 (_ BitVec 64)) (final_src5 (_ BitVec 64))
(ctx__split_fields120 u64) (ctx__split_fields121 u32)
(ctx__split_fields122 u16) (ctx__split_fields123 u7)
(ctx__split_fields124 Bool) (ctx__split_fields125 u6)
(ctx__split_fields126 Bool) (ctx__split_fields127 Bool)
(ctx__split_fields128 hash_bit_length) (ctx__split_fields129 u64)
(ctx__split_fields130 (Array (_ BitVec 64) u64))
(ctx__split_fields131 (Array (_ BitVec 64) byte))
(ctx__split_fields132 u64) (ctx__split_fields133 u32)
(ctx__split_fields134 u16) (ctx__split_fields135 u7)
(ctx__split_fields136 Bool) (ctx__split_fields137 u6)
(ctx__split_fields138 Bool) (ctx__split_fields139 Bool)
(ctx__split_fields140 hash_bit_length) (ctx__split_fields141 u64)
(ctx__split_fields142 (Array (_ BitVec 64) u64))
(ctx__split_fields143 (Array (_ BitVec 64) byte)) (src11 (_ BitVec 64))
(dst11 (_ BitVec 64)) (src12 (_ BitVec 64)) (dst12 (_ BitVec 64))
(src13 (_ BitVec 64)) (dst13 (_ BitVec 64)) (ctx__split_fields144 u64)
(ctx__split_fields145 u32) (ctx__split_fields146 u16)
(ctx__split_fields147 u7) (ctx__split_fields148 Bool)
(ctx__split_fields149 u6) (ctx__split_fields150 Bool)
(ctx__split_fields151 Bool) (ctx__split_fields152 hash_bit_length)
(ctx__split_fields153 u64) (ctx__split_fields154 (Array (_ BitVec 64) u64))
(ctx__split_fields155 (Array (_ BitVec 64) byte)) (src14 (_ BitVec 64))
(dst14 (_ BitVec 64)) (ctx__split_fields156 u64) (ctx__split_fields157 u32)
(ctx__split_fields158 u16) (ctx__split_fields159 u7)
(ctx__split_fields160 Bool) (ctx__split_fields161 u6)
(ctx__split_fields162 Bool) (ctx__split_fields163 Bool)
(ctx__split_fields164 hash_bit_length) (ctx__split_fields165 u64)
(ctx__split_fields166 (Array (_ BitVec 64) u64))
(ctx__split_fields167 (Array (_ BitVec 64) byte)) (src15 (_ BitVec 64))
(dst15 (_ BitVec 64)) (ctx__split_fields168 u64) (ctx__split_fields169 u32)
(ctx__split_fields170 u16) (ctx__split_fields171 u7)
(ctx__split_fields172 Bool) (ctx__split_fields173 u6)
(ctx__split_fields174 Bool) (ctx__split_fields175 Bool)
(ctx__split_fields176 hash_bit_length) (ctx__split_fields177 u64)
(ctx__split_fields178 (Array (_ BitVec 64) u64))
(ctx__split_fields179 (Array (_ BitVec 64) byte))
(ctx__split_fields180 u64) (ctx__split_fields181 u32)
(ctx__split_fields182 u16) (ctx__split_fields183 u7)
(ctx__split_fields184 Bool) (ctx__split_fields185 u6)
(ctx__split_fields186 Bool) (ctx__split_fields187 Bool)
(ctx__split_fields188 hash_bit_length) (ctx__split_fields189 u64)
(ctx__split_fields190 (Array (_ BitVec 64) u64))
(ctx__split_fields191 (Array (_ BitVec 64) byte))
(msg_byte_count4 (_ BitVec 64)) (n3 (_ BitVec 64))
(block_count4 (_ BitVec 64)) (current_msg_offset4 (_ BitVec 64))
(bytes_hashed3 (_ BitVec 64)) (tmp_b3 (Array (_ BitVec 64) byte))
(src16 (_ BitVec 64)) (dst16 (_ BitVec 64)) (final_dst6 (_ BitVec 64))
(final_src6 (_ BitVec 64)) (src17 (_ BitVec 64)) (dst17 (_ BitVec 64))
(final_dst7 (_ BitVec 64)) (final_src7 (_ BitVec 64))
(ctx__split_fields192 u64) (ctx__split_fields193 u32)
(ctx__split_fields194 u16) (ctx__split_fields195 u7)
(ctx__split_fields196 Bool) (ctx__split_fields197 u6)
(ctx__split_fields198 Bool) (ctx__split_fields199 Bool)
(ctx__split_fields200 hash_bit_length) (ctx__split_fields201 u64)
(ctx__split_fields202 (Array (_ BitVec 64) u64))
(ctx__split_fields203 (Array (_ BitVec 64) byte))
(msg_byte_count5 (_ BitVec 64)) (n4 (_ BitVec 64))
(block_count5 (_ BitVec 64)) (current_msg_offset5 (_ BitVec 64))
(bytes_hashed4 (_ BitVec 64)) (tmp_b4 (Array (_ BitVec 64) byte))
(src18 (_ BitVec 64)) (dst18 (_ BitVec 64)) (final_dst8 (_ BitVec 64))
(final_src8 (_ BitVec 64)) (src19 (_ BitVec 64)) (dst19 (_ BitVec 64))
(final_dst9 (_ BitVec 64)) (final_src9 (_ BitVec 64)))
(let ((ctx__split_fields204 (mk___split_fields2
(mk_context_header
(mk___split_fields1
(mk_tweak_value
(mk___split_fields ctx__split_fields168
ctx__split_fields169 ctx__split_fields170
ctx__split_fields171 ctx__split_fields172
ctx__split_fields173 ctx__split_fields174
ctx__split_fields175)) ctx__split_fields176
ctx__split_fields177)) ctx__split_fields178
ctx__split_fields179)))
(let ((ctx__split_fields205 (mk___split_fields2
(mk_context_header
(mk___split_fields1
(mk_tweak_value
(mk___split_fields ctx__split_fields156
ctx__split_fields157 ctx__split_fields158
ctx__split_fields159 ctx__split_fields160
ctx__split_fields161 ctx__split_fields162
ctx__split_fields163)) ctx__split_fields164
ctx__split_fields165)) ctx__split_fields166
ctx__split_fields167)))
(let ((dst20 (mk_ref2 dst14)))
(let ((src20 (mk_ref2 src14)))
(let ((ctx__split_fields206 (mk___split_fields2
(mk_context_header
(mk___split_fields1
(mk_tweak_value
(mk___split_fields ctx__split_fields132
ctx__split_fields133 ctx__split_fields134
ctx__split_fields135 ctx__split_fields136
ctx__split_fields137 ctx__split_fields138
ctx__split_fields139)) ctx__split_fields140
ctx__split_fields141)) ctx__split_fields142
ctx__split_fields143)))
(let ((ctx__split_fields207 (mk___split_fields2
(mk_context_header
(mk___split_fields1
(mk_tweak_value
(mk___split_fields ctx__split_fields108
ctx__split_fields109 ctx__split_fields110
ctx__split_fields111 ctx__split_fields112
ctx__split_fields113 ctx__split_fields114
ctx__split_fields115)) ctx__split_fields116
ctx__split_fields117)) ctx__split_fields118
ctx__split_fields119)))
(let ((ctx__split_fields208 (mk___split_fields2
(mk_context_header
(mk___split_fields1
(mk_tweak_value
(mk___split_fields ctx__split_fields96
ctx__split_fields97 ctx__split_fields98
ctx__split_fields99 ctx__split_fields100
ctx__split_fields101 ctx__split_fields102
ctx__split_fields103)) ctx__split_fields104
ctx__split_fields105)) ctx__split_fields106
ctx__split_fields107)))
(let ((ctx__split_fields209 (mk___split_fields2
(mk_context_header
(mk___split_fields1
(mk_tweak_value
(mk___split_fields ctx__split_fields60
ctx__split_fields61 ctx__split_fields62
ctx__split_fields63 ctx__split_fields64
ctx__split_fields65 ctx__split_fields66
ctx__split_fields67)) ctx__split_fields68
ctx__split_fields69)) ctx__split_fields70
ctx__split_fields71)))
(let ((dst21 (mk_ref2 dst8)))
(let ((src21 (mk_ref2 src8)))
(let ((ctx__split_fields210 (mk___split_fields2
(mk_context_header
(mk___split_fields1
(mk_tweak_value
(mk___split_fields ctx__split_fields36
ctx__split_fields37 ctx__split_fields38
ctx__split_fields39 ctx__split_fields40
ctx__split_fields41 ctx__split_fields42
ctx__split_fields43)) ctx__split_fields44
ctx__split_fields45)) ctx__split_fields46
ctx__split_fields47)))
(let ((ctx__split_fields211 (mk___split_fields2
(mk_context_header
(mk___split_fields1
(mk_tweak_value
(mk___split_fields ctx__split_fields12
ctx__split_fields13 ctx__split_fields14
ctx__split_fields15 ctx__split_fields16
ctx__split_fields17 ctx__split_fields18
ctx__split_fields19)) ctx__split_fields20
ctx__split_fields21)) ctx__split_fields22
ctx__split_fields23)))
(let ((dst22 (mk_ref2 dst)))
(let ((src22 (mk_ref2 src)))
(=>
(and (dynamic_property ((_ int2bv 64) 0)
((_ int2bv 64) 18446744073709551615) (to_rep5 (first (rt msg)))
(to_rep5 (last (rt msg))))
(and
(and
(and
(and
(and
(and (in_range9
(hash_bit_len_of
(mk_skein_512_context
(mk___split_fields2
(mk_context_header
(mk___split_fields1
(mk_tweak_value
(mk___split_fields ctx__split_fields ctx__split_fields1 ctx__split_fields2
ctx__split_fields3 ctx__split_fields4 ctx__split_fields5 ctx__split_fields6
ctx__split_fields7)) ctx__split_fields8 ctx__split_fields9))
ctx__split_fields10 ctx__split_fields11)))) (in_range11
(byte_count_of
(mk_skein_512_context
(mk___split_fields2
(mk_context_header
(mk___split_fields1
(mk_tweak_value
(mk___split_fields ctx__split_fields ctx__split_fields1 ctx__split_fields2
ctx__split_fields3 ctx__split_fields4 ctx__split_fields5 ctx__split_fields6
ctx__split_fields7)) ctx__split_fields8 ctx__split_fields9))
ctx__split_fields10 ctx__split_fields11)))))
(= (to_rep5 (first (rt msg))) ((_ int2bv 64) 0)))
(bvult (to_rep5 (last (rt msg))) ((_ int2bv 64) 18446744073709551615)))
(= (add_in_range (to_rep5 (last (rt msg))) ((_ int2bv 64) 64)) true))
(bvult (bvadd (to_rep5 (last (rt msg))) ((_ int2bv 64) 64)) ((_ int2bv 64) 18446744073709551615)))
(and
(and
(and
(and
(and
(and
(=> (bvule ((_ int2bv 64) 0) ((_ int2bv 64) 18446744073709551615))
(in_range2 msg_byte_count))
(=> (bvule ((_ int2bv 64) 0) ((_ int2bv 64) 63)) (in_range25 n)))
(=> (bvule ((_ int2bv 64) 1) ((_ int2bv 64) 288230376151711743))
(in_range12 block_count1)))
(=> (bvule ((_ int2bv 64) 0) ((_ int2bv 64) 18446744073709551615))
(in_range2 current_msg_offset)))
(=> (bvule ((_ int2bv 64) 0) ((_ int2bv 64) 18446744073709551615))
(in_range2 bytes_hashed)))
(and
(= msg_byte_count1 (bvadd (to_rep5 (last (rt msg))) ((_ int2bv 64) 1)))
(and (= current_msg_offset1 ((_ int2bv 64) 0))
(and
(ite (bvugt (bvadd msg_byte_count1 (to_rep1 ctx__split_fields9)) ((_ int2bv 64) 64))
(and
(ite (bvugt (to_rep1 ctx__split_fields9) ((_ int2bv 64) 0))
(and
(and
(and (= o (bvsub ((_ int2bv 64) 64) (to_rep1 ctx__split_fields9)))
(in_range25 (bvsub ((_ int2bv 64) 64) (to_rep1 ctx__split_fields9))))
(= n2 o))
(and
(and (= n2 c232b)
(=> (bvule ((_ int2bv 64) 0) ((_ int2bv 64) 18446744073709551615))
(in_range2 c232b)))
(and
(and
(=> (bvule ((_ int2bv 64) 0) ((_ int2bv 64) 18446744073709551615))
(in_range2 src))
(and (=> (bvule ((_ int2bv 64) 0) ((_ int2bv 64) 63)) (in_range25 dst))
(and
(=> (bvule ((_ int2bv 64) 0) ((_ int2bv 64) 63)) (in_range25 final_dst))
(and
(=> (bvule ((_ int2bv 64) 0) ((_ int2bv 64) 18446744073709551615))
(in_range2 final_src))
(ite (bvugt c232b ((_ int2bv 64) 0))
(and (= src4 current_msg_offset1)
(and
(and
(and (= o1 (to_rep1 ctx__split_fields9)) (in_range25
(to_rep1 ctx__split_fields9))) (= dst4 o1))
(and
(and
(and (= o2 (bvadd dst4 (bvsub c232b ((_ int2bv 64) 1)))) (in_range25
(bvadd dst4 (bvsub c232b ((_ int2bv 64) 1))))) (= final_dst4 o2))
(and (= final_src4 (bvadd src4 (bvsub c232b ((_ int2bv 64) 1))))
(and
(or
(and
(and
(and
(and
(and
(and
(and
(and
(and
(and (bvule (to_rep5 (first (rt msg))) src4)
(bvule src4 (to_rep5 (last (rt msg))))) (= o3 src4))
(= o4 (select (elts msg) o3))) (= o5 (to_rep o4))) (= (to_rep o6) o5))
(= o7 (store ctx__split_fields11 dst4 o6)))
(and
(and
(and (= ctx__split_fields o8)
(and (= ctx__split_fields1 o9)
(and (= ctx__split_fields2 o10)
(and (= ctx__split_fields3 o11)
(and (= ctx__split_fields4 o12)
(and (= ctx__split_fields5 o13)
(and (= ctx__split_fields6 o14) (= ctx__split_fields7 o15))))))))
(and (= ctx__split_fields8 o16) (= ctx__split_fields9 o17)))
(and (= ctx__split_fields10 o18) (= o7 o19))))
(and
(and
(and (= temp___standard__skein_123 o8)
(and (= temp___standard__skein_1231 o9)
(and (= temp___standard__skein_1232 o10)
(and (= temp___standard__skein_1233 o11)
(and (= temp___standard__skein_1234 o12)
(and (= temp___standard__skein_1235 o13)
(and (= temp___standard__skein_1236 o14)
(= temp___standard__skein_1237 o15))))))))
(and (= temp___standard__skein_1238 o16)
(= temp___standard__skein_1239 o17)))
(and (= temp___standard__skein_12310 o18)
(= temp___standard__skein_12311 o19))))
(and
(and
(and (= temp___standard__skein_123 ctx__split_fields24)
(and (= temp___standard__skein_1231 ctx__split_fields25)
(and (= temp___standard__skein_1232 ctx__split_fields26)
(and (= temp___standard__skein_1233 ctx__split_fields27)
(and (= temp___standard__skein_1234 ctx__split_fields28)
(and (= temp___standard__skein_1235 ctx__split_fields29)
(and (= temp___standard__skein_1236 ctx__split_fields30)
(= temp___standard__skein_1237 ctx__split_fields31))))))))
(and (= temp___standard__skein_1238 ctx__split_fields32)
(= temp___standard__skein_1239 ctx__split_fields33)))
(and (= temp___standard__skein_12310 ctx__split_fields34)
(= temp___standard__skein_12311 ctx__split_fields35))))
(and
(and
(and (= (to_rep7 ctx__split_fields44) (to_rep7 ctx__split_fields8))
(= (to_rep1 ctx__split_fields45) (to_rep1 ctx__split_fields9))) false)
(and
(and (= dst5 dst8)
(and (= src5 src8)
(and
(and
(and (= ctx__split_fields48 ctx__split_fields36)
(and (= ctx__split_fields49 ctx__split_fields37)
(and (= ctx__split_fields50 ctx__split_fields38)
(and (= ctx__split_fields51 ctx__split_fields39)
(and (= ctx__split_fields52 ctx__split_fields40)
(and (= ctx__split_fields53 ctx__split_fields41)
(and (= ctx__split_fields54 ctx__split_fields42)
(= ctx__split_fields55 ctx__split_fields43))))))))
(and (= ctx__split_fields56 ctx__split_fields44)
(= ctx__split_fields57 ctx__split_fields45)))
(and (= ctx__split_fields58 ctx__split_fields46)
(= ctx__split_fields59 ctx__split_fields47)))))
(and (= dst9 dst5)
(and (= src9 src5) (= ctx__split_fields209 ctx__split_fields210))))))
(and
(and (= temp___standard__skein_126 (to_rep7 ctx__split_fields8))
(and (= temp___standard__skein_127 (to_rep1 ctx__split_fields9))
(and
(and
(and
(and
(and
(and
(and
(and
(and
(and (bvule (to_rep5 (first (rt msg))) src4)
(bvule src4 (to_rep5 (last (rt msg))))) (= o3 src4))
(= o4 (select (elts msg) o3))) (= o5 (to_rep o4))) (= (to_rep o6) o5))
(= o7 (store ctx__split_fields11 dst4 o6)))
(and
(and
(and (= ctx__split_fields o8)
(and (= ctx__split_fields1 o9)
(and (= ctx__split_fields2 o10)
(and (= ctx__split_fields3 o11)
(and (= ctx__split_fields4 o12)
(and (= ctx__split_fields5 o13)
(and (= ctx__split_fields6 o14) (= ctx__split_fields7 o15))))))))
(and (= ctx__split_fields8 o16) (= ctx__split_fields9 o17)))
(and (= ctx__split_fields10 o18) (= o7 o19))))
(and
(and
(and (= temp___standard__skein_123 o8)
(and (= temp___standard__skein_1231 o9)
(and (= temp___standard__skein_1232 o10)
(and (= temp___standard__skein_1233 o11)
(and (= temp___standard__skein_1234 o12)
(and (= temp___standard__skein_1235 o13)
(and (= temp___standard__skein_1236 o14)
(= temp___standard__skein_1237 o15))))))))
(and (= temp___standard__skein_1238 o16)
(= temp___standard__skein_1239 o17)))
(and (= temp___standard__skein_12310 o18)
(= temp___standard__skein_12311 o19))))
(and
(and
(and (= temp___standard__skein_123 ctx__split_fields24)
(and (= temp___standard__skein_1231 ctx__split_fields25)
(and (= temp___standard__skein_1232 ctx__split_fields26)
(and (= temp___standard__skein_1233 ctx__split_fields27)
(and (= temp___standard__skein_1234 ctx__split_fields28)
(and (= temp___standard__skein_1235 ctx__split_fields29)
(and (= temp___standard__skein_1236 ctx__split_fields30)
(= temp___standard__skein_1237 ctx__split_fields31))))))))
(and (= temp___standard__skein_1238 ctx__split_fields32)
(= temp___standard__skein_1239 ctx__split_fields33)))
(and (= temp___standard__skein_12310 ctx__split_fields34)
(= temp___standard__skein_12311 ctx__split_fields35))))
(and
(and (= (to_rep7 ctx__split_fields44) temp___standard__skein_126)
(= (to_rep1 ctx__split_fields45) temp___standard__skein_127))
(and
(and
(=> (bvule ((_ int2bv 64) 0) ((_ int2bv 64) 18446744073709551615))
(in_range2 src5))
(=> (bvule ((_ int2bv 64) 0) ((_ int2bv 64) 63)) (in_range25 dst5)))
(and
(and (and (= dst5 dst6) (= src5 src6)) (and (= dst7 dst5) (= src7 src5)))
(=> (not (bvuge dst5 final_dst4)) (bvuge src5 final_src4))))))))
(and
(and (= dst21 (mk_ref2 dst6))
(and (= src21 (mk_ref2 src6))
(and
(and
(and (= ctx__split_fields48 ctx__split_fields36)
(and (= ctx__split_fields49 ctx__split_fields37)
(and (= ctx__split_fields50 ctx__split_fields38)
(and (= ctx__split_fields51 ctx__split_fields39)
(and (= ctx__split_fields52 ctx__split_fields40)
(and (= ctx__split_fields53 ctx__split_fields41)
(and (= ctx__split_fields54 ctx__split_fields42)
(= ctx__split_fields55 ctx__split_fields43))))))))
(and (= ctx__split_fields56 ctx__split_fields44)
(= ctx__split_fields57 ctx__split_fields45)))
(and (= ctx__split_fields58 ctx__split_fields46)
(= ctx__split_fields59 ctx__split_fields47)))))
(and (= dst9 dst7)
(and (= src9 src7) (= ctx__split_fields209 ctx__split_fields210))))))
(and
(and
(and
(and
(and (= (to_rep1 o20) (bvadd (to_rep1 ctx__split_fields57) c232b))
(and
(and (= ctx__split_fields48 o21)
(and (= ctx__split_fields49 o22)
(and (= ctx__split_fields50 o23)
(and (= ctx__split_fields51 o24)
(and (= ctx__split_fields52 o25)
(and (= ctx__split_fields53 o26)
(and (= ctx__split_fields54 o27) (= ctx__split_fields55 o28))))))))
(and (= ctx__split_fields56 o29) (= o20 o30))))
(and
(and (= o31 o21)
(and (= o32 o22)
(and (= o33 o23)
(and (= o34 o24)
(and (= o35 o25) (and (= o36 o26) (and (= o37 o27) (= o38 o28))))))))
(and (= o39 o29) (= o40 o30))))
(and
(and
(and (= o41 o31)
(and (= o42 o32)
(and (= o43 o33)
(and (= o44 o34)
(and (= o45 o35) (and (= o46 o36) (and (= o47 o37) (= o48 o38))))))))
(and (= o49 o39) (= o50 o40)))
(and (= ctx__split_fields58 o51) (= ctx__split_fields59 o52))))
(and
(and
(and (= temp___standard__skein_130 o41)
(and (= temp___standard__skein_1301 o42)
(and (= temp___standard__skein_1302 o43)
(and (= temp___standard__skein_1303 o44)
(and (= temp___standard__skein_1304 o45)
(and (= temp___standard__skein_1305 o46)
(and (= temp___standard__skein_1306 o47)
(= temp___standard__skein_1307 o48))))))))
(and (= temp___standard__skein_1308 o49)
(= temp___standard__skein_1309 o50)))
(and (= temp___standard__skein_13010 o51)
(= temp___standard__skein_13011 o52))))
(and
(and
(and (= temp___standard__skein_130 ctx__split_fields72)
(and (= temp___standard__skein_1301 ctx__split_fields73)
(and (= temp___standard__skein_1302 ctx__split_fields74)
(and (= temp___standard__skein_1303 ctx__split_fields75)
(and (= temp___standard__skein_1304 ctx__split_fields76)
(and (= temp___standard__skein_1305 ctx__split_fields77)
(and (= temp___standard__skein_1306 ctx__split_fields78)
(= temp___standard__skein_1307 ctx__split_fields79))))))))
(and (= temp___standard__skein_1308 ctx__split_fields80)
(= temp___standard__skein_1309 ctx__split_fields81)))
(and (= temp___standard__skein_13010 ctx__split_fields82)
(= temp___standard__skein_13011 ctx__split_fields83)))))))))
(and
(and (= final_src4 final_src)
(and (= final_dst4 final_dst)
(and (= dst21 dst22)
(and (= src21 src22)
(and
(and
(and (= ctx__split_fields ctx__split_fields72)
(and (= ctx__split_fields1 ctx__split_fields73)
(and (= ctx__split_fields2 ctx__split_fields74)
(and (= ctx__split_fields3 ctx__split_fields75)
(and (= ctx__split_fields4 ctx__split_fields76)
(and (= ctx__split_fields5 ctx__split_fields77)
(and (= ctx__split_fields6 ctx__split_fields78)
(= ctx__split_fields7 ctx__split_fields79))))))))
(and (= ctx__split_fields8 ctx__split_fields80)
(= ctx__split_fields9 ctx__split_fields81)))
(and (= ctx__split_fields10 ctx__split_fields82)
(= ctx__split_fields11 ctx__split_fields83)))))))
(and (= final_src4 final_src2)
(and (= final_dst4 final_dst2)
(and (= dst9 dst2)
(and (= src9 src2)
(= (mk___split_fields2
(mk_context_header
(mk___split_fields1
(mk_tweak_value
(mk___split_fields ctx__split_fields72 ctx__split_fields73
ctx__split_fields74 ctx__split_fields75 ctx__split_fields76
ctx__split_fields77 ctx__split_fields78 ctx__split_fields79))
ctx__split_fields80 ctx__split_fields81)) ctx__split_fields82
ctx__split_fields83) ctx__split_fields211)))))))))))
(and (= msg_byte_count2 (bvsub msg_byte_count1 n2))
(and (= current_msg_offset2 (bvadd current_msg_offset1 n2))
(and (= tmp_b2 ctx__split_fields83)
(and
(and
(and
(and (in_range9 (to_rep7 ctx__split_fields92))
(= (to_rep7 ctx__split_fields92) (to_rep7 ctx__split_fields80)))
(in_range11 (to_rep1 ctx__split_fields93)))
(= (to_rep1 ctx__split_fields93) (to_rep1 ctx__split_fields81)))
(and
(and
(and
(and
(and (= (to_rep1 o53) ((_ int2bv 64) 0))
(and
(and (= ctx__split_fields84 o54)
(and (= ctx__split_fields85 o55)
(and (= ctx__split_fields86 o56)
(and (= ctx__split_fields87 o57)
(and (= ctx__split_fields88 o58)
(and (= ctx__split_fields89 o59)
(and (= ctx__split_fields90 o60) (= ctx__split_fields91 o61))))))))
(and (= ctx__split_fields92 o62) (= o53 o63))))
(and
(and (= o64 o54)
(and (= o65 o55)
(and (= o66 o56)
(and (= o67 o57)
(and (= o68 o58) (and (= o69 o59) (and (= o70 o60) (= o71 o61))))))))
(and (= o72 o62) (= o73 o63))))
(and
(and
(and (= o74 o64)
(and (= o75 o65)
(and (= o76 o66)
(and (= o77 o67)
(and (= o78 o68) (and (= o79 o69) (and (= o80 o70) (= o81 o71))))))))
(and (= o82 o72) (= o83 o73)))
(and (= ctx__split_fields94 o84) (= ctx__split_fields95 o85))))
(and
(and
(and (= temp___standard__skein_133 o74)
(and (= temp___standard__skein_1331 o75)
(and (= temp___standard__skein_1332 o76)
(and (= temp___standard__skein_1333 o77)
(and (= temp___standard__skein_1334 o78)
(and (= temp___standard__skein_1335 o79)
(and (= temp___standard__skein_1336 o80)
(= temp___standard__skein_1337 o81))))))))
(and (= temp___standard__skein_1338 o82)
(= temp___standard__skein_1339 o83)))
(and (= temp___standard__skein_13310 o84)
(= temp___standard__skein_13311 o85))))
(and
(and
(and (= temp___standard__skein_133 ctx__split_fields96)
(and (= temp___standard__skein_1331 ctx__split_fields97)
(and (= temp___standard__skein_1332 ctx__split_fields98)
(and (= temp___standard__skein_1333 ctx__split_fields99)
(and (= temp___standard__skein_1334 ctx__split_fields100)
(and (= temp___standard__skein_1335 ctx__split_fields101)
(and (= temp___standard__skein_1336 ctx__split_fields102)
(= temp___standard__skein_1337 ctx__split_fields103))))))))
(and (= temp___standard__skein_1338 ctx__split_fields104)
(= temp___standard__skein_1339 ctx__split_fields105)))
(and (= temp___standard__skein_13310 ctx__split_fields106)
(= temp___standard__skein_13311 ctx__split_fields107)))))))))))
(and
(and (= final_src4 final_src)
(and (= final_dst4 final_dst)
(and (= dst21 dst22)
(and (= src21 src22)
(and (= tmp_b2 tmp_b)
(and (= current_msg_offset2 current_msg_offset1)
(and (= n2 n)
(and (= msg_byte_count2 msg_byte_count1)
(and
(and
(and (= ctx__split_fields ctx__split_fields96)
(and (= ctx__split_fields1 ctx__split_fields97)
(and (= ctx__split_fields2 ctx__split_fields98)
(and (= ctx__split_fields3 ctx__split_fields99)
(and (= ctx__split_fields4 ctx__split_fields100)
(and (= ctx__split_fields5 ctx__split_fields101)
(and (= ctx__split_fields6 ctx__split_fields102)
(= ctx__split_fields7 ctx__split_fields103))))))))
(and (= ctx__split_fields8 ctx__split_fields104)
(= ctx__split_fields9 ctx__split_fields105)))
(and (= ctx__split_fields10 ctx__split_fields106)
(= ctx__split_fields11 ctx__split_fields107)))))))))))
(and (= final_src4 final_src2)
(and (= final_dst4 final_dst2)
(and (= dst9 dst2)
(and (= src9 src2)
(and (= tmp_b2 tmp_b1)
(and (= current_msg_offset2 current_msg_offset1)
(and (= n2 n1)
(and (= msg_byte_count2 msg_byte_count1)
(= ctx__split_fields208 ctx__split_fields211)))))))))))
(ite (bvugt msg_byte_count2 ((_ int2bv 64) 64))
(and
(and
(and
(= o86 (bvudiv (bvsub msg_byte_count2 ((_ int2bv 64) 1)) ((_ int2bv 64) 64)))
(in_range12
(bvudiv (bvsub msg_byte_count2 ((_ int2bv 64) 1)) ((_ int2bv 64) 64))))
(= block_count3 o86))
(and
(and
(and
(and (in_range9 (to_rep7 ctx__split_fields116))
(= (to_rep7 ctx__split_fields116) (to_rep7 ctx__split_fields104)))
(in_range11 (to_rep1 ctx__split_fields117)))
(= (to_rep1 ctx__split_fields117) (to_rep1 ctx__split_fields105)))
(and (= bytes_hashed2 (bvmul block_count3 ((_ int2bv 64) 64)))
(and (= msg_byte_count3 (bvsub msg_byte_count2 bytes_hashed2))
(= current_msg_offset3 (bvadd current_msg_offset2 bytes_hashed2))))))
(and
(and (= bytes_hashed2 bytes_hashed)
(and (= current_msg_offset3 current_msg_offset2)
(and (= block_count3 block_count1)
(and (= msg_byte_count3 msg_byte_count2)
(= ctx__split_fields207 ctx__split_fields208)))))
(and (= bytes_hashed2 bytes_hashed1)
(and (= current_msg_offset3 current_msg_offset2)
(and (= block_count3 block_count2)
(and (= msg_byte_count3 msg_byte_count2)
(= ctx__split_fields207 ctx__split_fields208))))))))
(and
(and (= final_src4 final_src)
(and (= final_dst4 final_dst)
(and (= dst21 dst22)
(and (= src21 src22)
(and (= tmp_b2 tmp_b)
(and (= bytes_hashed2 bytes_hashed)
(and (= current_msg_offset3 current_msg_offset1)
(and (= block_count3 block_count1)
(and (= n2 n)
(and (= msg_byte_count3 msg_byte_count1)
(and
(and
(and (= ctx__split_fields ctx__split_fields108)
(and (= ctx__split_fields1 ctx__split_fields109)
(and (= ctx__split_fields2 ctx__split_fields110)
(and (= ctx__split_fields3 ctx__split_fields111)
(and (= ctx__split_fields4 ctx__split_fields112)
(and (= ctx__split_fields5 ctx__split_fields113)
(and (= ctx__split_fields6 ctx__split_fields114)
(= ctx__split_fields7 ctx__split_fields115))))))))
(and (= ctx__split_fields8 ctx__split_fields116)
(= ctx__split_fields9 ctx__split_fields117)))
(and (= ctx__split_fields10 ctx__split_fields118)
(= ctx__split_fields11 ctx__split_fields119)))))))))))))
(and (= final_src4 final_src2)
(and (= final_dst4 final_dst2)
(and (= dst9 dst2)
(and (= src9 src2)
(and (= tmp_b2 tmp_b1)
(and (= bytes_hashed2 bytes_hashed1)
(and (= current_msg_offset3 current_msg_offset1)
(and (= block_count3 block_count2)
(and (= n2 n1)
(and (= msg_byte_count3 msg_byte_count1)
(= ctx__split_fields207 ctx__split_fields211)))))))))))))
(and
(and (= msg_byte_count3 c234b)
(=> (bvule ((_ int2bv 64) 0) ((_ int2bv 64) 18446744073709551615))
(in_range2 c234b)))
(and
(=> (bvule ((_ int2bv 64) 0) ((_ int2bv 64) 18446744073709551615))
(in_range2 src1))
(and (=> (bvule ((_ int2bv 64) 0) ((_ int2bv 64) 63)) (in_range25 dst1))
(and
(=> (bvule ((_ int2bv 64) 0) ((_ int2bv 64) 63)) (in_range25 final_dst1))
(and
(=> (bvule ((_ int2bv 64) 0) ((_ int2bv 64) 18446744073709551615))
(in_range2 final_src1))
(ite (bvugt c234b ((_ int2bv 64) 0))
(and (= src10 current_msg_offset3)
(and
(and
(and (= o87 (to_rep1 ctx__split_fields117)) (in_range25
(to_rep1 ctx__split_fields117))) (= dst10 o87))
(and
(and
(and (= o88 (bvadd dst10 (bvsub c234b ((_ int2bv 64) 1)))) (in_range25
(bvadd dst10 (bvsub c234b ((_ int2bv 64) 1))))) (= final_dst5 o88))
(and (= final_src5 (bvadd src10 (bvsub c234b ((_ int2bv 64) 1))))
(and
(or
(and
(and
(and
(and
(and
(and
(and
(and
(and
(and (bvule (to_rep5 (first (rt msg))) src10)
(bvule src10 (to_rep5 (last (rt msg))))) (= o89 src10))
(= o90 (select (elts msg) o89))) (= o91 (to_rep o90)))
(= (to_rep o92) o91)) (= o93 (store ctx__split_fields119 dst10 o92)))
(and
(and
(and (= ctx__split_fields108 o94)
(and (= ctx__split_fields109 o95)
(and (= ctx__split_fields110 o96)
(and (= ctx__split_fields111 o97)
(and (= ctx__split_fields112 o98)
(and (= ctx__split_fields113 o99)
(and (= ctx__split_fields114 o100) (= ctx__split_fields115 o101))))))))
(and (= ctx__split_fields116 o102) (= ctx__split_fields117 o103)))
(and (= ctx__split_fields118 o104) (= o93 o105))))
(and
(and
(and (= temp___standard__skein_136 o94)
(and (= temp___standard__skein_1361 o95)
(and (= temp___standard__skein_1362 o96)
(and (= temp___standard__skein_1363 o97)
(and (= temp___standard__skein_1364 o98)
(and (= temp___standard__skein_1365 o99)
(and (= temp___standard__skein_1366 o100)
(= temp___standard__skein_1367 o101))))))))
(and (= temp___standard__skein_1368 o102)
(= temp___standard__skein_1369 o103)))
(and (= temp___standard__skein_13610 o104)
(= temp___standard__skein_13611 o105))))
(and
(and
(and (= temp___standard__skein_136 ctx__split_fields120)
(and (= temp___standard__skein_1361 ctx__split_fields121)
(and (= temp___standard__skein_1362 ctx__split_fields122)
(and (= temp___standard__skein_1363 ctx__split_fields123)
(and (= temp___standard__skein_1364 ctx__split_fields124)
(and (= temp___standard__skein_1365 ctx__split_fields125)
(and (= temp___standard__skein_1366 ctx__split_fields126)
(= temp___standard__skein_1367 ctx__split_fields127))))))))
(and (= temp___standard__skein_1368 ctx__split_fields128)
(= temp___standard__skein_1369 ctx__split_fields129)))
(and (= temp___standard__skein_13610 ctx__split_fields130)
(= temp___standard__skein_13611 ctx__split_fields131))))
(and
(and
(and (= (to_rep7 ctx__split_fields140) (to_rep7 ctx__split_fields116))
(= (to_rep1 ctx__split_fields141) (to_rep1 ctx__split_fields117))) false)
(and
(and (= dst11 dst14)
(and (= src11 src14)
(and
(and
(and (= ctx__split_fields144 ctx__split_fields132)
(and (= ctx__split_fields145 ctx__split_fields133)
(and (= ctx__split_fields146 ctx__split_fields134)
(and (= ctx__split_fields147 ctx__split_fields135)
(and (= ctx__split_fields148 ctx__split_fields136)
(and (= ctx__split_fields149 ctx__split_fields137)
(and (= ctx__split_fields150 ctx__split_fields138)
(= ctx__split_fields151 ctx__split_fields139))))))))
(and (= ctx__split_fields152 ctx__split_fields140)
(= ctx__split_fields153 ctx__split_fields141)))
(and (= ctx__split_fields154 ctx__split_fields142)
(= ctx__split_fields155 ctx__split_fields143)))))
(and (= dst15 dst11)
(and (= src15 src11) (= ctx__split_fields205 ctx__split_fields206))))))
(and
(and (= temp___standard__skein_139 (to_rep7 ctx__split_fields116))
(and (= temp___standard__skein_140 (to_rep1 ctx__split_fields117))
(and
(and
(and
(and
(and
(and
(and
(and
(and
(and (bvule (to_rep5 (first (rt msg))) src10)
(bvule src10 (to_rep5 (last (rt msg))))) (= o89 src10))
(= o90 (select (elts msg) o89))) (= o91 (to_rep o90)))
(= (to_rep o92) o91)) (= o93 (store ctx__split_fields119 dst10 o92)))
(and
(and
(and (= ctx__split_fields108 o94)
(and (= ctx__split_fields109 o95)
(and (= ctx__split_fields110 o96)
(and (= ctx__split_fields111 o97)
(and (= ctx__split_fields112 o98)
(and (= ctx__split_fields113 o99)
(and (= ctx__split_fields114 o100) (= ctx__split_fields115 o101))))))))
(and (= ctx__split_fields116 o102) (= ctx__split_fields117 o103)))
(and (= ctx__split_fields118 o104) (= o93 o105))))
(and
(and
(and (= temp___standard__skein_136 o94)
(and (= temp___standard__skein_1361 o95)
(and (= temp___standard__skein_1362 o96)
(and (= temp___standard__skein_1363 o97)
(and (= temp___standard__skein_1364 o98)
(and (= temp___standard__skein_1365 o99)
(and (= temp___standard__skein_1366 o100)
(= temp___standard__skein_1367 o101))))))))
(and (= temp___standard__skein_1368 o102)
(= temp___standard__skein_1369 o103)))
(and (= temp___standard__skein_13610 o104)
(= temp___standard__skein_13611 o105))))
(and
(and
(and (= temp___standard__skein_136 ctx__split_fields120)
(and (= temp___standard__skein_1361 ctx__split_fields121)
(and (= temp___standard__skein_1362 ctx__split_fields122)
(and (= temp___standard__skein_1363 ctx__split_fields123)
(and (= temp___standard__skein_1364 ctx__split_fields124)
(and (= temp___standard__skein_1365 ctx__split_fields125)
(and (= temp___standard__skein_1366 ctx__split_fields126)
(= temp___standard__skein_1367 ctx__split_fields127))))))))
(and (= temp___standard__skein_1368 ctx__split_fields128)
(= temp___standard__skein_1369 ctx__split_fields129)))
(and (= temp___standard__skein_13610 ctx__split_fields130)
(= temp___standard__skein_13611 ctx__split_fields131))))
(and
(and (= (to_rep7 ctx__split_fields140) temp___standard__skein_139)
(= (to_rep1 ctx__split_fields141) temp___standard__skein_140))
(and
(and
(=> (bvule ((_ int2bv 64) 0) ((_ int2bv 64) 18446744073709551615))
(in_range2 src11))
(=> (bvule ((_ int2bv 64) 0) ((_ int2bv 64) 63)) (in_range25 dst11)))
(and
(and (and (= dst11 dst12) (= src11 src12))
(and (= dst13 dst11) (= src13 src11)))
(=> (not (bvuge dst11 final_dst5)) (bvuge src11 final_src5))))))))
(and
(and (= dst20 (mk_ref2 dst12))
(and (= src20 (mk_ref2 src12))
(and
(and
(and (= ctx__split_fields144 ctx__split_fields132)
(and (= ctx__split_fields145 ctx__split_fields133)
(and (= ctx__split_fields146 ctx__split_fields134)
(and (= ctx__split_fields147 ctx__split_fields135)
(and (= ctx__split_fields148 ctx__split_fields136)
(and (= ctx__split_fields149 ctx__split_fields137)
(and (= ctx__split_fields150 ctx__split_fields138)
(= ctx__split_fields151 ctx__split_fields139))))))))
(and (= ctx__split_fields152 ctx__split_fields140)
(= ctx__split_fields153 ctx__split_fields141)))
(and (= ctx__split_fields154 ctx__split_fields142)
(= ctx__split_fields155 ctx__split_fields143)))))
(and (= dst15 dst13)
(and (= src15 src13) (= ctx__split_fields205 ctx__split_fields206))))))
(and
(and
(and
(and
(and (= (to_rep1 o106) (bvadd (to_rep1 ctx__split_fields153) c234b))
(and
(and (= ctx__split_fields144 o107)
(and (= ctx__split_fields145 o108)
(and (= ctx__split_fields146 o109)
(and (= ctx__split_fields147 o110)
(and (= ctx__split_fields148 o111)
(and (= ctx__split_fields149 o112)
(and (= ctx__split_fields150 o113) (= ctx__split_fields151 o114))))))))
(and (= ctx__split_fields152 o115) (= o106 o116))))
(and
(and (= o117 o107)
(and (= o118 o108)
(and (= o119 o109)
(and (= o120 o110)
(and (= o121 o111) (and (= o122 o112) (and (= o123 o113) (= o124 o114))))))))
(and (= o125 o115) (= o126 o116))))
(and
(and
(and (= o127 o117)
(and (= o128 o118)
(and (= o129 o119)
(and (= o130 o120)
(and (= o131 o121) (and (= o132 o122) (and (= o133 o123) (= o134 o124))))))))
(and (= o135 o125) (= o136 o126)))
(and (= ctx__split_fields154 o137) (= ctx__split_fields155 o138))))
(and
(and
(and (= temp___standard__skein_143 o127)
(and (= temp___standard__skein_1431 o128)
(and (= temp___standard__skein_1432 o129)
(and (= temp___standard__skein_1433 o130)
(and (= temp___standard__skein_1434 o131)
(and (= temp___standard__skein_1435 o132)
(and (= temp___standard__skein_1436 o133)
(= temp___standard__skein_1437 o134))))))))
(and (= temp___standard__skein_1438 o135)
(= temp___standard__skein_1439 o136)))
(and (= temp___standard__skein_14310 o137)
(= temp___standard__skein_14311 o138))))
(and
(and
(and (= temp___standard__skein_143 ctx__split_fields168)
(and (= temp___standard__skein_1431 ctx__split_fields169)
(and (= temp___standard__skein_1432 ctx__split_fields170)
(and (= temp___standard__skein_1433 ctx__split_fields171)
(and (= temp___standard__skein_1434 ctx__split_fields172)
(and (= temp___standard__skein_1435 ctx__split_fields173)
(and (= temp___standard__skein_1436 ctx__split_fields174)
(= temp___standard__skein_1437 ctx__split_fields175))))))))
(and (= temp___standard__skein_1438 ctx__split_fields176)
(= temp___standard__skein_1439 ctx__split_fields177)))
(and (= temp___standard__skein_14310 ctx__split_fields178)
(= temp___standard__skein_14311 ctx__split_fields179)))))))))
(and
(and (= final_src5 final_src1)
(and (= final_dst5 final_dst1)
(and (= dst20 (mk_ref2 dst1))
(and (= src20 (mk_ref2 src1))
(= ctx__split_fields204 ctx__split_fields207)))))
(and (= final_src5 final_src3)
(and (= final_dst5 final_dst3)
(and (= dst15 dst3)
(and (= src15 src3) (= ctx__split_fields204 ctx__split_fields207))))))))))))))))
(and
(and (= final_src7 final_src5)
(and (= final_dst7 final_dst5)
(and (= dst17 dst14)
(and (= src17 src14)
(and (= final_src6 final_src4)
(and (= final_dst6 final_dst4)
(and (= dst16 dst8)
(and (= src16 src8)
(and (= tmp_b3 tmp_b2)
(and (= bytes_hashed3 bytes_hashed2)
(and (= current_msg_offset4 current_msg_offset3)
(and (= block_count4 block_count3)
(and (= n3 n2)
(and (= msg_byte_count4 msg_byte_count3)
(and
(and
(and (= ctx__split_fields180 ctx__split_fields168)
(and (= ctx__split_fields181 ctx__split_fields169)
(and (= ctx__split_fields182 ctx__split_fields170)
(and (= ctx__split_fields183 ctx__split_fields171)
(and (= ctx__split_fields184 ctx__split_fields172)
(and (= ctx__split_fields185 ctx__split_fields173)
(and (= ctx__split_fields186 ctx__split_fields174)
(= ctx__split_fields187 ctx__split_fields175))))))))
(and (= ctx__split_fields188 ctx__split_fields176)
(= ctx__split_fields189 ctx__split_fields177)))
(and (= ctx__split_fields190 ctx__split_fields178)
(= ctx__split_fields191 ctx__split_fields179)))))))))))))))))
(and (= final_src9 final_src5)
(and (= final_dst9 final_dst5)
(and (= dst19 dst15)
(and (= src19 src15)
(and (= final_src8 final_src4)
(and (= final_dst8 final_dst4)
(and (= dst18 dst9)
(and (= src18 src9)
(and (= tmp_b4 tmp_b2)
(and (= bytes_hashed4 bytes_hashed2)
(and (= current_msg_offset5 current_msg_offset3)
(and (= block_count5 block_count3)
(and (= n4 n2)
(and (= msg_byte_count5 msg_byte_count3)
(and
(and
(and (= ctx__split_fields192 ctx__split_fields168)
(and (= ctx__split_fields193 ctx__split_fields169)
(and (= ctx__split_fields194 ctx__split_fields170)
(and (= ctx__split_fields195 ctx__split_fields171)
(and (= ctx__split_fields196 ctx__split_fields172)
(and (= ctx__split_fields197 ctx__split_fields173)
(and (= ctx__split_fields198 ctx__split_fields174)
(= ctx__split_fields199 ctx__split_fields175))))))))
(and (= ctx__split_fields200 ctx__split_fields176)
(= ctx__split_fields201 ctx__split_fields177)))
(and (= ctx__split_fields202 ctx__split_fields178)
(= ctx__split_fields203 ctx__split_fields179)))))))))))))))))))))
(and
(and (in_range9
(hash_bit_len_of
(mk_skein_512_context
(mk___split_fields2
(mk_context_header
(mk___split_fields1
(mk_tweak_value
(mk___split_fields ctx__split_fields180 ctx__split_fields181
ctx__split_fields182 ctx__split_fields183 ctx__split_fields184
ctx__split_fields185 ctx__split_fields186 ctx__split_fields187))
ctx__split_fields188 ctx__split_fields189)) ctx__split_fields190
ctx__split_fields191))))
(= (hash_bit_len_of
(mk_skein_512_context
(mk___split_fields2
(mk_context_header
(mk___split_fields1
(mk_tweak_value
(mk___split_fields ctx__split_fields180 ctx__split_fields181
ctx__split_fields182 ctx__split_fields183 ctx__split_fields184
ctx__split_fields185 ctx__split_fields186 ctx__split_fields187))
ctx__split_fields188 ctx__split_fields189)) ctx__split_fields190
ctx__split_fields191))) (hash_bit_len_of
(mk_skein_512_context
(mk___split_fields2
(mk_context_header
(mk___split_fields1
(mk_tweak_value
(mk___split_fields ctx__split_fields
ctx__split_fields1 ctx__split_fields2
ctx__split_fields3 ctx__split_fields4
ctx__split_fields5 ctx__split_fields6
ctx__split_fields7)) ctx__split_fields8
ctx__split_fields9)) ctx__split_fields10
ctx__split_fields11)))))
(in_range11
(byte_count_of
(mk_skein_512_context
(mk___split_fields2
(mk_context_header
(mk___split_fields1
(mk_tweak_value
(mk___split_fields ctx__split_fields180 ctx__split_fields181
ctx__split_fields182 ctx__split_fields183 ctx__split_fields184
ctx__split_fields185 ctx__split_fields186 ctx__split_fields187))
ctx__split_fields188 ctx__split_fields189)) ctx__split_fields190
ctx__split_fields191)))))))))))))))))))))))
(check-sat)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment