path: root/test/regress/regress1/quantifiers/bug_743.smt2

; COMMAND-LINE: --lang=smt2.5
; EXPECT: unsat

;; 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)