diff options
Diffstat (limited to 'test/regress/regress0/quantifiers/bug_743.smt2')
| -rw-r--r-- | test/regress/regress0/quantifiers/bug_743.smt2 | 777 |
1 files changed, 0 insertions, 777 deletions
diff --git a/test/regress/regress0/quantifiers/bug_743.smt2 b/test/regress/regress0/quantifiers/bug_743.smt2 deleted file mode 100644 index ec5a5149e..000000000 --- a/test/regress/regress0/quantifiers/bug_743.smt2 +++ /dev/null @@ -1,777 +0,0 @@ -; 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) - |