--- /dev/null
+;; produced by cvc4_14.drv ;;
+(set-logic AUFBVDTNIRA)
+(set-info :source |VC generated by SPARK 2014|)
+(set-info :smt-lib-version 2.0)
+(set-info :category industrial)
+(set-info :status unsat)
+;;; generated by SMT-LIB2 driver
+;;; SMT-LIB2 driver: bit-vectors, common part
+;;; SMT-LIB2: integer arithmetic
+(declare-datatypes () ((tuple0 (Tuple0))))
+(declare-sort us_private 0)
+
+(declare-fun us_null_ext__ () us_private)
+
+(declare-sort us_type_of_heap 0)
+
+(declare-datatypes ()
+((us_type_of_heap__ref
+ (mk___type_of_heap__ref (us_type_of_heap__content us_type_of_heap)))))
+(declare-sort us_image 0)
+
+(declare-datatypes () ((int__ref (mk_int__ref (int__content Int)))))
+(declare-datatypes () ((bool__ref (mk_bool__ref (bool__content Bool)))))
+(declare-datatypes () ((real__ref (mk_real__ref (real__content Real)))))
+(declare-datatypes ()
+((us_private__ref (mk___private__ref (us_private__content us_private)))))
+(define-fun int__ref___projection ((a int__ref)) Int (int__content a))
+
+(define-fun bool__ref___projection ((a bool__ref)) Bool (bool__content a))
+
+(define-fun real__ref___projection ((a real__ref)) Real (real__content a))
+
+(define-fun us_private__ref___projection ((a us_private__ref)) us_private
+ (us_private__content a))
+
+(declare-fun us_compatible_tags (Int Int) Bool)
+
+;; __compatible_tags_refl
+ (assert (forall ((tag Int)) (us_compatible_tags tag tag)))
+
+(define-fun to_int1 ((b Bool)) Int (ite (= b true) 1 0))
+
+(define-fun of_int ((i Int)) Bool (ite (= i 0) false true))
+
+(define-fun in_range ((x Int)) Bool (or (= x 0) (= x 1)))
+
+(declare-fun attr__ATTRIBUTE_IMAGE (Bool) us_image)
+
+(declare-fun attr__ATTRIBUTE_VALUE__pre_check (us_image) Bool)
+
+(declare-fun attr__ATTRIBUTE_VALUE (us_image) Bool)
+
+(declare-sort integer 0)
+
+(define-fun in_range1 ((x Int)) Bool (and (<= (- 2147483648) x)
+ (<= x 2147483647)))
+
+(define-fun bool_eq ((x Int) (y Int)) Bool (ite (= x y) true false))
+
+(declare-fun attr__ATTRIBUTE_IMAGE1 (Int) us_image)
+
+(declare-fun attr__ATTRIBUTE_VALUE__pre_check1 (us_image) Bool)
+
+(declare-fun attr__ATTRIBUTE_VALUE1 (us_image) Int)
+
+(declare-fun to_rep (integer) Int)
+
+(declare-fun of_rep (Int) integer)
+
+(declare-fun user_eq (integer integer) Bool)
+
+(declare-fun dummy () integer)
+
+;; inversion_axiom
+ (assert
+ (forall ((x integer)) (! (= (of_rep (to_rep x)) x) :pattern ((to_rep x))
+)))
+
+;; range_axiom
+ (assert
+ (forall ((x integer)) (! (in_range1 (to_rep x)) :pattern ((to_rep x))
+)))
+
+;; coerce_axiom
+ (assert
+ (forall ((x Int))
+ (! (=> (in_range1 x) (= (to_rep (of_rep x)) x)) :pattern ((to_rep
+ (of_rep x)))
+)))
+
+(declare-datatypes ()
+((integer__ref (mk_integer__ref (integer__content integer)))))
+(define-fun integer__ref___projection ((a integer__ref)) integer
+(integer__content
+ a))
+
+(declare-sort natural 0)
+
+(define-fun in_range2 ((x Int)) Bool (and (<= 0 x) (<= x 2147483647)))
+
+(define-fun bool_eq1 ((x Int) (y Int)) Bool (ite (= x y) true false))
+
+(declare-fun attr__ATTRIBUTE_IMAGE2 (Int) us_image)
+
+(declare-fun attr__ATTRIBUTE_VALUE__pre_check2 (us_image) Bool)
+
+(declare-fun attr__ATTRIBUTE_VALUE2 (us_image) Int)
+
+(declare-fun to_rep1 (natural) Int)
+
+(declare-fun of_rep1 (Int) natural)
+
+(declare-fun user_eq1 (natural natural) Bool)
+
+(declare-fun dummy1 () natural)
+
+;; inversion_axiom
+ (assert
+ (forall ((x natural))
+ (! (= (of_rep1 (to_rep1 x)) x) :pattern ((to_rep1 x)) )))
+
+;; range_axiom
+ (assert
+ (forall ((x natural)) (! (in_range2 (to_rep1 x)) :pattern ((to_rep1 x))
+)))
+
+;; coerce_axiom
+ (assert
+ (forall ((x Int))
+ (! (=> (in_range2 x) (= (to_rep1 (of_rep1 x)) x)) :pattern ((to_rep1
+ (of_rep1
+x))) )))
+
+(declare-datatypes ()
+((natural__ref (mk_natural__ref (natural__content natural)))))
+(define-fun natural__ref___projection ((a natural__ref)) natural
+(natural__content
+ a))
+
+(define-fun dynamic_invariant ((temp___expr_33 Int) (temp___is_init_30
+Bool)
+ (temp___do_constant_31 Bool)
+ (temp___do_toplevel_32 Bool)) Bool (=>
+ (or (= temp___is_init_30 true)
+ (<= 0 2147483647)) (in_range2
+ temp___expr_33)))
+
+(declare-sort index 0)
+
+(define-fun in_range3 ((x Int)) Bool (and (<= 1 x) (<= x 100)))
+
+(define-fun bool_eq2 ((x Int) (y Int)) Bool (ite (= x y) true false))
+
+(declare-fun attr__ATTRIBUTE_IMAGE3 (Int) us_image)
+
+(declare-fun attr__ATTRIBUTE_VALUE__pre_check3 (us_image) Bool)
+
+(declare-fun attr__ATTRIBUTE_VALUE3 (us_image) Int)
+
+(declare-fun to_rep2 (index) Int)
+
+(declare-fun of_rep2 (Int) index)
+
+(declare-fun user_eq2 (index index) Bool)
+
+(declare-fun dummy2 () index)
+
+;; inversion_axiom
+ (assert
+ (forall ((x index))
+ (! (= (of_rep2 (to_rep2 x)) x) :pattern ((to_rep2 x)) )))
+
+;; range_axiom
+ (assert
+ (forall ((x index)) (! (in_range3 (to_rep2 x)) :pattern ((to_rep2 x))
+)))
+
+;; coerce_axiom
+ (assert
+ (forall ((x Int))
+ (! (=> (in_range3 x) (= (to_rep2 (of_rep2 x)) x)) :pattern ((to_rep2
+ (of_rep2
+x))) )))
+
+(declare-datatypes () ((index__ref (mk_index__ref (index__content
+index)))))
+(define-fun index__ref___projection ((a index__ref)) index (index__content
+a))
+
+(define-fun dynamic_invariant1 ((temp___expr_144 Int)
+ (temp___is_init_141 Bool) (temp___do_constant_142 Bool)
+ (temp___do_toplevel_143 Bool)) Bool (=>
+ (or (= temp___is_init_141 true)
+ (<= 1 100)) (in_range3
+ temp___expr_144)))
+
+(declare-datatypes ()
+((map__ref (mk_map__ref (map__content (Array Int natural))))))
+(declare-fun bool_eq3 ((Array Int natural) Int Int (Array Int natural) Int
+ Int) Bool)
+
+;; T__ada_array___equal_def
+ (assert
+ (forall ((a (Array Int natural)))
+ (forall ((af Int))
+ (forall ((al Int))
+ (forall ((b (Array Int natural)))
+ (forall ((bf Int))
+ (forall ((bl Int))
+ (! (=
+ (and (ite (<= af al) (= (+ (- al af) 1) (+ (- bl bf) 1)) (< bl bf))
+ (forall ((i Int))
+ (! (=> (and (<= af i) (<= i al))
+ (= (select a i) (select b (+ (- bf af) i)))) :pattern ((select a
+i)) )))
+ (= (bool_eq3 a af al b bf bl) true)) :pattern ((bool_eq3 a af al b bf
+ bl)) ))))))))
+
+(declare-fun slide ((Array Int natural) Int Int) (Array Int natural))
+
+;; slide_eq
+ (assert
+ (forall ((a (Array Int natural)))
+ (forall ((first Int))
+ (! (= (slide a first first) a) :pattern ((slide a first first)) ))))
+
+;; slide_def
+ (assert
+ (forall ((a (Array Int natural)))
+ (forall ((old_first Int))
+ (forall ((new_first Int))
+ (forall ((i Int))
+ (! (= (select (slide a old_first new_first) i) (select a (- i (-
+new_first old_first)))) :pattern ((select
+ (slide a old_first new_first) i)) ))))))
+
+(declare-fun concat1 ((Array Int natural) Int Int (Array Int natural) Int
+ Int) (Array Int natural))
+
+;; concat_def
+ (assert
+ (forall ((a (Array Int natural)) (b (Array Int natural)))
+ (forall ((a_first Int) (a_last Int) (b_first Int) (b_last Int))
+ (forall ((i Int))
+ (! (and
+ (=> (and (<= a_first i) (<= i a_last))
+ (= (select (concat1 a a_first a_last b b_first b_last) i) (select a
+i)))
+ (=> (< a_last i)
+ (= (select (concat1 a a_first a_last b b_first b_last) i) (select b
+(+ (- i a_last) (- b_first 1)))))) :pattern ((select
+ (concat1 a a_first a_last b b_first b_last) i)) )))))
+
+(declare-fun singleton (natural Int) (Array Int natural))
+
+;; singleton_def
+ (assert
+ (forall ((v natural))
+ (forall ((i Int))
+ (! (= (select (singleton v i) i) v) :pattern ((select (singleton v i)
+i)) ))))
+
+(declare-fun compare ((Array Int natural) Int Int (Array Int natural) Int
+ Int) Int)
+
+;; compare_def
+ (assert
+ (forall ((a (Array Int natural)) (b (Array Int natural)))
+ (forall ((a_first Int) (a_last Int) (b_first Int) (b_last Int))
+ (! (and
+ (= (= (compare a a_first a_last b b_first b_last) 0)
+ (= (bool_eq3 a a_first a_last b b_first b_last) true))
+ (and
+ (= (< (compare a a_first a_last b b_first b_last) 0)
+ (exists ((i Int) (j Int))
+ (and (<= i a_last)
+ (and (< j b_last)
+ (and (= (bool_eq3 a a_first i b b_first j) true)
+ (or (= i a_last)
+ (and (< i a_last)
+ (< (to_rep1 (select a (+ i 1))) (to_rep1 (select b (+ j 1)))))))))))
+ (= (< 0 (compare a a_first a_last b b_first b_last))
+ (exists ((i Int) (j Int))
+ (and (<= i b_last)
+ (and (< j a_last)
+ (and (= (bool_eq3 a a_first j b b_first i) true)
+ (or (= i b_last)
+ (and (< i b_last)
+ (< (to_rep1 (select b (+ i 1))) (to_rep1 (select a (+ j
+1))))))))))))) :pattern (
+ (compare a a_first a_last b b_first b_last)) ))))
+
+(declare-sort t 0)
+
+(declare-fun first (t) integer)
+
+(declare-fun last (t) integer)
+
+(declare-fun mk (Int Int) t)
+
+;; mk_def
+ (assert
+ (forall ((f Int) (l Int))
+ (! (=> (in_range1 f)
+ (=> (in_range1 l)
+ (and (= (to_rep (first (mk f l))) f) (= (to_rep (last (mk f l)))
+l)))) :pattern (
+ (mk f l)) )))
+
+(define-fun dynamic_property ((range_first Int) (range_last Int) (low Int)
+ (high Int)) Bool (and (in_range1 low)
+ (and (in_range1 high)
+ (=> (<= low high) (and (in_range3 low) (in_range3
+high))))))
+
+(declare-datatypes () ((us_t (mk___t (elts (Array Int natural))(rt t)))))
+(define-fun to_array ((a us_t)) (Array Int natural) (elts a))
+
+(define-fun of_array ((a (Array Int natural)) (f Int)
+ (l Int)) us_t (mk___t a (mk f l)))
+
+(define-fun first1 ((a us_t)) Int (to_rep (first (rt a))))
+
+(define-fun last1 ((a us_t)) Int (to_rep (last (rt a))))
+
+(define-fun length ((a us_t)) Int (ite (<= (first1 a) (last1 a))
+ (+ (- (last1 a) (first1 a)) 1) 0))
+
+(declare-fun value__size () Int)
+
+(declare-fun object__size ((Array Int natural)) Int)
+
+(declare-fun value__component__size () Int)
+
+(declare-fun object__component__size ((Array Int natural)) Int)
+
+(declare-fun value__alignment () Int)
+
+(declare-fun object__alignment ((Array Int natural)) Int)
+
+;; value__size_axiom
+ (assert (<= 0 value__size))
+
+;; object__size_axiom
+ (assert (forall ((a (Array Int natural))) (<= 0 (object__size a))))
+
+;; value__component__size_axiom
+ (assert (<= 0 value__component__size))
+
+;; object__component__size_axiom
+ (assert
+ (forall ((a (Array Int natural))) (<= 0 (object__component__size a))))
+
+;; value__alignment_axiom
+ (assert (<= 0 value__alignment))
+
+;; object__alignment_axiom
+ (assert (forall ((a (Array Int natural))) (<= 0 (object__alignment a))))
+
+(define-fun bool_eq4 ((x us_t)
+ (y us_t)) Bool (bool_eq3 (elts x) (to_rep (first (rt x)))
+ (to_rep (last (rt x))) (elts y) (to_rep (first (rt y)))
+ (to_rep (last (rt y)))))
+
+(declare-fun user_eq3 (us_t us_t) Bool)
+
+(declare-fun dummy3 () us_t)
+
+(declare-datatypes ()
+((nat_array__ref (mk_nat_array__ref (nat_array__content us_t)))))
+(define-fun nat_array__ref___projection ((a nat_array__ref)) us_t
+(nat_array__content
+ a))
+
+(define-fun dynamic_invariant2 ((temp___expr_150 us_t)
+ (temp___is_init_147 Bool) (temp___do_constant_148 Bool)
+ (temp___do_toplevel_149 Bool)) Bool (=>
+ (not (= temp___do_constant_148
+true))
+ (dynamic_property 1 100
+ (first1 temp___expr_150)
+ (last1 temp___expr_150))))
+
+(declare-fun remove_last (us_t) us_t)
+
+(declare-fun first2 () Int)
+
+(declare-fun last2 () Int)
+
+(define-fun dynamic_property1 ((first_int Int) (last_int Int)
+ (x Int)) Bool (and (<= first_int x) (<= x last_int)))
+
+(define-fun bool_eq5 ((x Int) (y Int)) Bool (ite (= x y) true false))
+
+(declare-fun attr__ATTRIBUTE_IMAGE4 (Int) us_image)
+
+(declare-fun attr__ATTRIBUTE_VALUE__pre_check4 (us_image) Bool)
+
+(declare-fun attr__ATTRIBUTE_VALUE4 (us_image) Int)
+
+(declare-fun user_eq4 (integer integer) Bool)
+
+(declare-fun dummy4 () integer)
+
+(declare-datatypes () ((t15s__ref (mk_t15s__ref (t15s__content
+integer)))))
+(define-fun t15s__ref___projection ((a t15s__ref)) integer (t15s__content
+a))
+
+(declare-sort t1 0)
+
+(declare-fun first3 (t1) integer)
+
+(declare-fun last3 (t1) integer)
+
+(declare-fun mk1 (Int Int) t1)
+
+;; mk_def
+ (assert
+ (forall ((f Int) (l Int))
+ (! (=> (in_range1 f)
+ (=> (in_range1 l)
+ (and (= (to_rep (first3 (mk1 f l))) f) (= (to_rep (last3 (mk1 f l)))
+l)))) :pattern (
+ (mk1 f l)) )))
+
+(define-fun dynamic_property2 ((range_first Int) (range_last Int) (low
+Int)
+ (high Int)) Bool (and (in_range1 low)
+ (and (in_range1 high)
+ (=> (<= low high)
+ (and (dynamic_property1 range_first range_last low)
+ (dynamic_property1 range_first range_last high))))))
+
+(declare-datatypes ()
+((us_t1 (mk___t1 (elts1 (Array Int natural))(rt1 t1)))))
+(define-fun to_array1 ((a us_t1)) (Array Int natural) (elts1 a))
+
+(define-fun of_array1 ((a (Array Int natural)) (f Int)
+ (l Int)) us_t1 (mk___t1 a (mk1 f l)))
+
+(define-fun first4 ((a us_t1)) Int (to_rep (first3 (rt1 a))))
+
+(define-fun last4 ((a us_t1)) Int (to_rep (last3 (rt1 a))))
+
+(define-fun length1 ((a us_t1)) Int (ite (<= (first4 a) (last4 a))
+ (+ (- (last4 a) (first4 a)) 1) 0))
+
+(declare-fun value__size1 () Int)
+
+(declare-fun object__size1 ((Array Int natural)) Int)
+
+(declare-fun value__component__size1 () Int)
+
+(declare-fun object__component__size1 ((Array Int natural)) Int)
+
+(declare-fun value__alignment1 () Int)
+
+(declare-fun object__alignment1 ((Array Int natural)) Int)
+
+;; value__size_axiom
+ (assert (<= 0 value__size1))
+
+;; object__size_axiom
+ (assert (forall ((a (Array Int natural))) (<= 0 (object__size1 a))))
+
+;; value__component__size_axiom
+ (assert (<= 0 value__component__size1))
+
+;; object__component__size_axiom
+ (assert
+ (forall ((a (Array Int natural))) (<= 0 (object__component__size1 a))))
+
+;; value__alignment_axiom
+ (assert (<= 0 value__alignment1))
+
+;; object__alignment_axiom
+ (assert (forall ((a (Array Int natural))) (<= 0 (object__alignment1
+a))))
+
+(define-fun bool_eq6 ((x us_t1)
+ (y us_t1)) Bool (bool_eq3 (elts1 x) (to_rep (first3 (rt1 x)))
+ (to_rep (last3 (rt1 x))) (elts1 y)
+ (to_rep (first3 (rt1 y))) (to_rep (last3 (rt1 y)))))
+
+(declare-fun user_eq5 (us_t1 us_t1) Bool)
+
+(declare-fun dummy5 () us_t1)
+
+(declare-datatypes () ((t16s__ref (mk_t16s__ref (t16s__content us_t1)))))
+(define-fun t16s__ref___projection ((a t16s__ref)) us_t1 (t16s__content
+a))
+
+;; remove_last__post_axiom
+ (assert
+ (forall ((a us_t))
+ (! (=> (and (dynamic_invariant2 a true true true) (< 0 (length a)))
+ (dynamic_invariant2 (remove_last a) true false true)) :pattern (
+ (remove_last a)) )))
+
+;; remove_last__def_axiom
+ (assert
+ (forall ((a us_t))
+ (! (=> (dynamic_invariant2 a true true true)
+ (= (remove_last a) (let ((temp___163 (let ((temp___162 (- (last1 a)
+1)))
+ (let ((temp___161 (first1 a)))
+ (of_array1 (to_array a)
+temp___161
+ temp___162)))))
+ (of_array (to_array1 temp___163) (first4
+temp___163)
+ (last4 temp___163))))) :pattern ((remove_last a))
+)))
+
+(declare-fun occ (us_t Int) Int)
+
+(declare-sort nb_occ 0)
+
+(define-fun in_range4 ((x Int)) Bool (and (<= 0 x) (<= x 100)))
+
+(define-fun bool_eq7 ((x Int) (y Int)) Bool (ite (= x y) true false))
+
+(declare-fun attr__ATTRIBUTE_IMAGE5 (Int) us_image)
+
+(declare-fun attr__ATTRIBUTE_VALUE__pre_check5 (us_image) Bool)
+
+(declare-fun attr__ATTRIBUTE_VALUE5 (us_image) Int)
+
+(declare-fun to_rep3 (nb_occ) Int)
+
+(declare-fun of_rep3 (Int) nb_occ)
+
+(declare-fun user_eq6 (nb_occ nb_occ) Bool)
+
+(declare-fun dummy6 () nb_occ)
+
+;; inversion_axiom
+ (assert
+ (forall ((x nb_occ))
+ (! (= (of_rep3 (to_rep3 x)) x) :pattern ((to_rep3 x)) )))
+
+;; range_axiom
+ (assert
+ (forall ((x nb_occ)) (! (in_range4 (to_rep3 x)) :pattern ((to_rep3 x))
+)))
+
+;; coerce_axiom
+ (assert
+ (forall ((x Int))
+ (! (=> (in_range4 x) (= (to_rep3 (of_rep3 x)) x)) :pattern ((to_rep3
+ (of_rep3
+x))) )))
+
+(declare-datatypes ()
+((nb_occ__ref (mk_nb_occ__ref (nb_occ__content nb_occ)))))
+(define-fun nb_occ__ref___projection ((a nb_occ__ref)) nb_occ
+(nb_occ__content
+ a))
+
+(define-fun dynamic_invariant3 ((temp___expr_155 Int)
+ (temp___is_init_152 Bool) (temp___do_constant_153 Bool)
+ (temp___do_toplevel_154 Bool)) Bool (=>
+ (or (= temp___is_init_152 true)
+ (<= 0 100)) (in_range4
+ temp___expr_155)))
+
+(declare-fun occ_def (us_t Int) Int)
+
+;; occ__post_axiom
+ (assert
+ (forall ((a us_t))
+ (forall ((e Int))
+ (! (=> (and (dynamic_invariant2 a true true true) (in_range2 e))
+ (let ((result (occ a e)))
+ (and (<= result (length a)) (dynamic_invariant3 result true false
+true)))) :pattern (
+ (occ a e)) ))))
+
+;; occ__def_axiom
+ (assert
+ (forall ((a us_t))
+ (forall ((e Int))
+ (! (=> (and (dynamic_invariant2 a true true true) (in_range2 e))
+ (= (occ a e) (occ_def a e))) :pattern ((occ a e)) ))))
+
+(declare-fun is_set (us_t Int Int us_t) Bool)
+
+;; is_set__def_axiom
+ (assert
+ (forall ((a us_t) (r us_t))
+ (forall ((i Int) (v Int))
+ (! (= (= (is_set a i v r) true)
+ (and
+ (and (and (= (first1 r) (first1 a)) (= (last1 r) (last1 a)))
+ (= (to_rep1 (select (to_array r) i)) v))
+ (forall ((j Int))
+ (=> (and (<= (first1 a) j) (<= j (last1 a)))
+ (=> (not (= i j))
+ (= (to_rep1 (select (to_array r) j)) (to_rep1 (select (to_array a)
+j)))))))) :pattern (
+ (is_set a i v r)) ))))
+
+(declare-fun a () us_t)
+
+(declare-fun attr__ATTRIBUTE_ADDRESS () Int)
+
+(declare-fun i () Int)
+
+(declare-fun attr__ATTRIBUTE_ADDRESS1 () Int)
+
+(declare-fun v () Int)
+
+(declare-fun attr__ATTRIBUTE_ADDRESS2 () Int)
+
+(declare-fun e () Int)
+
+(declare-fun attr__ATTRIBUTE_ADDRESS3 () Int)
+
+(declare-fun r () us_t)
+
+(declare-fun attr__ATTRIBUTE_ADDRESS4 () Int)
+
+(declare-fun b__first () integer)
+
+(declare-fun b__last () integer)
+
+(declare-fun attr__ATTRIBUTE_ADDRESS5 () Int)
+
+(define-fun dynamic_invariant4 ((temp___expr_15 Int) (temp___is_init_12
+Bool)
+ (temp___do_constant_13 Bool)
+ (temp___do_toplevel_14 Bool)) Bool (=>
+ (or (= temp___is_init_12 true)
+ (<= (- 2147483648) 2147483647))
+ (in_range1 temp___expr_15)))
+
+;; occ_def__def_axiom
+ (assert
+ (forall ((a1 us_t))
+ (forall ((e1 Int))
+ (! (=> (and (dynamic_invariant2 a1 true true true) (in_range2 e1))
+ (= (occ_def a1 e1) (ite (= (length a1) 0) 0
+ (ite (= (to_rep1 (select (to_array a1) (last1
+a1))) e1)
+ (+ (occ_def (remove_last a1) e1) 1)
+ (occ_def (remove_last a1) e1))))) :pattern
+((occ_def
+ a1
+e1)) ))))
+
+(declare-fun b () (Array Int natural))
+
+(declare-fun perm__occ_set__b__assume () (Array Int natural))
+
+(declare-fun perm__occ_set__b__assume1 () t)
+
+(declare-fun o () natural)
+
+(declare-fun o1 () Int)
+
+(declare-fun o2 () (Array Int natural))
+
+(declare-fun o3 () (Array Int natural))
+
+(declare-fun o4 () t)
+
+(declare-fun result () (Array Int natural))
+
+(declare-fun b1 () (Array Int natural))
+
+(declare-fun result1 () (Array Int natural))
+
+(declare-fun b2 () (Array Int natural))
+
+(define-fun o5 () us_t (mk___t o3 o4))
+
+(define-fun perm__occ_set__b__assume2 () us_t (mk___t
+ perm__occ_set__b__assume
+ perm__occ_set__b__assume1))
+
+;; H
+ (assert (dynamic_invariant2 a true false true))
+
+;; H
+ (assert (in_range3 i))
+
+;; H
+ (assert (in_range2 v))
+
+;; H
+ (assert (in_range2 e))
+
+;; H
+ (assert (dynamic_invariant2 r true false true))
+
+;; H
+ (assert
+ (and (and (<= (to_rep (first (rt a))) i) (<= i (to_rep (last (rt a)))))
+ (= (is_set a i v r) true)))
+
+;; H
+ (assert
+ (and (= perm__occ_set__b__assume2 (remove_last a))
+ (and (dynamic_invariant2 perm__occ_set__b__assume2 true false true)
+ (and (= (elts a) perm__occ_set__b__assume)
+ (= (mk
+ (to_rep
+ (first3 (mk1 (to_rep (first (rt a))) (- (to_rep (last (rt a))) 1))))
+ (to_rep
+ (last3 (mk1 (to_rep (first (rt a))) (- (to_rep (last (rt a))) 1)))))
+ perm__occ_set__b__assume1)))))
+
+;; H
+ (assert (= (mk_map__ref result) (mk_map__ref b)))
+
+;; H
+ (assert (= b1 perm__occ_set__b__assume))
+
+;; H
+ (assert (= (to_rep b__first) (to_rep (first
+perm__occ_set__b__assume1))))
+
+;; H
+ (assert (= (to_rep b__last) (to_rep (last perm__occ_set__b__assume1))))
+
+;; H
+ (assert (dynamic_property 1 100 (to_rep b__first) (to_rep b__last)))
+
+;; H
+ (assert (not (= (length a) 0)))
+
+;; H
+ (assert (not (= i (to_rep (last (rt a))))))
+
+;; H
+ (assert (= (to_rep1 o) v))
+
+;; H
+ (assert (and (<= (to_rep b__first) i) (<= i (to_rep b__last))))
+
+;; H
+ (assert (= o1 i))
+
+;; H
+ (assert (= o2 (store b1 o1 o)))
+
+;; H
+ (assert (= b1 result1))
+
+;; H
+ (assert (= b2 o2))
+
+;; H
+ (assert
+ (and (= o5 (remove_last r))
+ (and (dynamic_invariant2 o5 true false true)
+ (and (= (elts r) o3)
+ (= (mk
+ (to_rep
+ (first3 (mk1 (to_rep (first (rt r))) (- (to_rep (last (rt r))) 1))))
+ (to_rep
+ (last3 (mk1 (to_rep (first (rt r))) (- (to_rep (last (rt r))) 1)))))
+ o4)))))
+
+(assert
+;; WP_parameter_def
+ ;; File "perm.ads", line 21, characters 0-0
+ (not
+ (= (bool_eq3 o3 (to_rep (first o4)) (to_rep (last o4)) b2
+ (to_rep (first (mk (to_rep b__first) (to_rep b__last))))
+ (to_rep (last (mk (to_rep b__first) (to_rep b__last))))) true)))
+(check-sat)
+
projects / cvc5.git / commitdiff