diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-07-05 15:11:28 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-07-05 15:11:38 -0500 |
commit | 967747b7b279256bd9368e2d392ae71dec1bb1c1 (patch) | |
tree | 18a811b16d7552c1ae52fadfe34e54acde68e6a8 /test | |
parent | a58abbe71fb1fc07129ff9c7568ac544145fb57c (diff) |
Add option --trigger-active-sel. Recognize simple triggers with polarity. Do not drop patterns from merged prenex (fixes bug 743).
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/regress0/quantifiers/Makefile.am | 3 | ||||
-rw-r--r-- | test/regress/regress0/quantifiers/bug_743.smt2 | 774 |
2 files changed, 776 insertions, 1 deletions
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index 4c657adf1..7d02af77d 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -83,7 +83,8 @@ TESTS = \ partial-trigger.smt2 \ inst-max-level-segf.smt2 \ small-bug1-fixpoint-3.smt2 \ - z3.620661-no-fv-trigger.smt2 + z3.620661-no-fv-trigger.smt2 \ + bug_743.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine diff --git a/test/regress/regress0/quantifiers/bug_743.smt2 b/test/regress/regress0/quantifiers/bug_743.smt2 new file mode 100644 index 000000000..4e3ee0c96 --- /dev/null +++ b/test/regress/regress0/quantifiers/bug_743.smt2 @@ -0,0 +1,774 @@ +;; 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) + |