diff options
Diffstat (limited to 'test')
25 files changed, 1077 insertions, 10 deletions
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index 4c657adf1..6608ae22d 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -83,7 +83,10 @@ 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 \ + quaternion_ds1_symm_0428.fof.smt2 \ + bug749-rounding.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine diff --git a/test/regress/regress0/quantifiers/bi-artm-s.smt2 b/test/regress/regress0/quantifiers/bi-artm-s.smt2 index 5fb7522e9..b97c339fc 100644 --- a/test/regress/regress0/quantifiers/bi-artm-s.smt2 +++ b/test/regress/regress0/quantifiers/bi-artm-s.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --fmf-bound-int-lazy +; COMMAND-LINE: --fmf-bound-lazy ; EXPECT: unsat (set-option :incremental "false") (set-info :status unsat) diff --git a/test/regress/regress0/quantifiers/bug749-rounding.smt2 b/test/regress/regress0/quantifiers/bug749-rounding.smt2 new file mode 100644 index 000000000..5fea8d4ff --- /dev/null +++ b/test/regress/regress0/quantifiers/bug749-rounding.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --var-ineq-elim-quant +; EXPECT: unknown +(set-logic UFLIRA) + +(declare-fun round2 (Real) Int) + +(assert (forall ((x Real) (i Int)) (=> (<= x (to_real i)) (<= (round2 x) i)) )) +(assert (forall ((x Real) (i Int)) (=> (<= (to_real i) x) (<= i (round2 x))) )) + + +(check-sat) 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) + diff --git a/test/regress/regress0/quantifiers/quaternion_ds1_symm_0428.fof.smt2 b/test/regress/regress0/quantifiers/quaternion_ds1_symm_0428.fof.smt2 new file mode 100644 index 000000000..9b0216e58 --- /dev/null +++ b/test/regress/regress0/quantifiers/quaternion_ds1_symm_0428.fof.smt2 @@ -0,0 +1,49 @@ +; COMMAND-LINE: --full-saturate-quant +; EXPECT: unsat +(set-logic AUFLIRA) +(set-info :status unsat) +(declare-fun def () Real) +(declare-fun h_ds1_filter () (Array Int (Array Int Real))) +(declare-fun id_ds1_filter () (Array Int (Array Int Real))) +(declare-fun pminus_ds1_filter () (Array Int (Array Int Real))) +(declare-fun pv5 () Int) +(declare-fun q_ds1_filter () (Array Int (Array Int Real))) +(declare-fun r_ds1_filter () (Array Int (Array Int Real))) +(declare-fun use () Real) +(declare-fun uniform_int_rnd (Int Int) Int) +(declare-fun abs_ (Real) Real) +(declare-fun log (Real) Real) +(declare-fun exp (Real) Real) +(declare-fun cos (Real) Real) +(declare-fun sin (Real) Real) +(declare-fun sqrt (Real) Real) +(declare-fun divide (Real Real) Real) +(declare-fun cond (Int Real Real) Real) +(declare-fun tptp_term_equal (Real Real) Int) +(declare-fun tptp_term_equals (Real Real) Int) +(declare-fun tptp_term_and (Real Real) Int) +(declare-fun sum (Int Int Real) Real) +(declare-fun dim (Int Int) Int) +(declare-fun trans ((Array Int (Array Int Real))) (Array Int (Array Int Real))) +(declare-fun inv ((Array Int (Array Int Real))) (Array Int (Array Int Real))) +(declare-fun tptp_mmul ((Array Int (Array Int Real)) (Array Int (Array Int Real))) (Array Int (Array Int Real))) +(declare-fun tptp_madd ((Array Int (Array Int Real)) (Array Int (Array Int Real))) (Array Int (Array Int Real))) +(declare-fun tptp_msub ((Array Int (Array Int Real)) (Array Int (Array Int Real))) (Array Int (Array Int Real))) +(declare-fun tptp_const_array1 (Int Real) (Array Int Real)) +(declare-fun tptp_const_array2 (Int Int Real) (Array Int (Array Int Real))) +(assert (forall ((?X_0 Int) (?C_1 Int)) (=> (>= ?X_0 0) (<= (uniform_int_rnd ?C_1 ?X_0) ?X_0)))) +(assert (forall ((?X_2 Int) (?C_3 Int)) (=> (>= ?X_2 0) (>= (uniform_int_rnd ?C_3 ?X_2) 0)))) +(assert (forall ((?I_4 Int) (?L_5 Int) (?U_6 Int) (?Val_7 Real)) (=> (and (<= ?L_5 ?I_4) (<= ?I_4 ?U_6)) (= (select (tptp_const_array1 (dim ?L_5 ?U_6) ?Val_7) ?I_4) ?Val_7)))) +(assert (forall ((?I_8 Int) (?L1_9 Int) (?U1_10 Int) (?J_11 Int) (?L2_12 Int) (?U2_13 Int) (?Val_14 Real)) (=> (and (and (and (<= ?L1_9 ?I_8) (<= ?I_8 ?U1_10)) (<= ?L2_12 ?J_11)) (<= ?J_11 ?U2_13)) (= (select (select (tptp_const_array2 (dim ?L1_9 ?U1_10) (dim ?L2_12 ?U2_13) ?Val_14) ?I_8) ?J_11) ?Val_14)))) +(assert (forall ((?I0_15 Int) (?J0_16 Int) (?A_17 (Array Int (Array Int Real))) (?B_18 (Array Int (Array Int Real))) (?N_19 Int)) (let ((?v_0 (tptp_mmul ?A_17 (tptp_mmul ?B_18 (trans ?A_17))))) (=> (and (and (and (and (>= ?I0_15 0) (<= ?I0_15 ?N_19)) (>= ?J0_16 0)) (<= ?J0_16 ?N_19)) (= (select (select ?B_18 ?I0_15) ?J0_16) (select (select ?B_18 ?J0_16) ?I0_15))) (= (select (select ?v_0 ?I0_15) ?J0_16) (select (select ?v_0 ?J0_16) ?I0_15)))))) +(assert (forall ((?I0_20 Int) (?J0_21 Int) (?I_22 Int) (?J_23 Int) (?A_24 (Array Int (Array Int Real))) (?B_25 (Array Int (Array Int Real))) (?N_26 Int) (?M_27 Int)) (let ((?v_0 (tptp_mmul ?A_24 (tptp_mmul ?B_25 (trans ?A_24))))) (=> (and (and (and (and (and (and (and (and (>= ?I0_20 0) (<= ?I0_20 ?N_26)) (>= ?J0_21 0)) (<= ?J0_21 ?N_26)) (>= ?I_22 0)) (<= ?I_22 ?M_27)) (>= ?J_23 0)) (<= ?J_23 ?M_27)) (= (select (select ?B_25 ?I_22) ?J_23) (select (select ?B_25 ?J_23) ?I_22))) (= (select (select ?v_0 ?I0_20) ?J0_21) (select (select ?v_0 ?J0_21) ?I0_20)))))) +(assert (forall ((?I_28 Int) (?J_29 Int) (?A_30 (Array Int (Array Int Real))) (?B_31 (Array Int (Array Int Real))) (?N_32 Int)) (let ((?v_0 (tptp_madd ?A_30 ?B_31))) (=> (and (and (and (and (and (>= ?I_28 0) (<= ?I_28 ?N_32)) (>= ?J_29 0)) (<= ?J_29 ?N_32)) (= (select (select ?A_30 ?I_28) ?J_29) (select (select ?A_30 ?J_29) ?I_28))) (= (select (select ?B_31 ?I_28) ?J_29) (select (select ?B_31 ?J_29) ?I_28))) (= (select (select ?v_0 ?I_28) ?J_29) (select (select ?v_0 ?J_29) ?I_28)))))) +(assert (forall ((?I_33 Int) (?J_34 Int) (?A_35 (Array Int (Array Int Real))) (?B_36 (Array Int (Array Int Real))) (?N_37 Int)) (let ((?v_0 (tptp_msub ?A_35 ?B_36))) (=> (and (and (and (and (and (>= ?I_33 0) (<= ?I_33 ?N_37)) (>= ?J_34 0)) (<= ?J_34 ?N_37)) (= (select (select ?A_35 ?I_33) ?J_34) (select (select ?A_35 ?J_34) ?I_33))) (= (select (select ?B_36 ?I_33) ?J_34) (select (select ?B_36 ?J_34) ?I_33))) (= (select (select ?v_0 ?I_33) ?J_34) (select (select ?v_0 ?J_34) ?I_33)))))) +(assert (forall ((?I_38 Int) (?J_39 Int) (?A_40 (Array Int (Array Int Real))) (?N_41 Int)) (let ((?v_0 (trans ?A_40))) (=> (and (and (and (and (>= ?I_38 0) (<= ?I_38 ?N_41)) (>= ?J_39 0)) (<= ?J_39 ?N_41)) (= (select (select ?A_40 ?I_38) ?J_39) (select (select ?A_40 ?J_39) ?I_38))) (= (select (select ?v_0 ?I_38) ?J_39) (select (select ?v_0 ?J_39) ?I_38)))))) +(assert (forall ((?I_42 Int) (?J_43 Int) (?A_44 (Array Int (Array Int Real))) (?N_45 Int)) (let ((?v_0 (inv ?A_44))) (=> (and (and (and (and (>= ?I_42 0) (<= ?I_42 ?N_45)) (>= ?J_43 0)) (<= ?J_43 ?N_45)) (= (select (select ?A_44 ?I_42) ?J_43) (select (select ?A_44 ?J_43) ?I_42))) (= (select (select ?v_0 ?I_42) ?J_43) (select (select ?v_0 ?J_43) ?I_42)))))) +(assert (forall ((?I0_46 Int) (?J0_47 Int) (?I_48 Int) (?J_49 Int) (?A_50 (Array Int (Array Int Real))) (?B_51 (Array Int (Array Int Real))) (?C_52 (Array Int (Array Int Real))) (?D_53 (Array Int (Array Int Real))) (?E_54 (Array Int (Array Int Real))) (?F_55 (Array Int (Array Int Real))) (?N_56 Int) (?M_57 Int)) (let ((?v_0 (tptp_madd ?A_50 (tptp_mmul ?B_51 (tptp_mmul (tptp_madd (tptp_mmul ?C_52 (tptp_mmul ?D_53 (trans ?C_52))) (tptp_mmul ?E_54 (tptp_mmul ?F_55 (trans ?E_54)))) (trans ?B_51)))))) (=> (and (and (and (and (and (and (and (and (and (and (>= ?I0_46 0) (<= ?I0_46 ?N_56)) (>= ?J0_47 0)) (<= ?J0_47 ?N_56)) (>= ?I_48 0)) (<= ?I_48 ?M_57)) (>= ?J_49 0)) (<= ?J_49 ?M_57)) (= (select (select ?D_53 ?I_48) ?J_49) (select (select ?D_53 ?J_49) ?I_48))) (= (select (select ?A_50 ?I0_46) ?J0_47) (select (select ?A_50 ?J0_47) ?I0_46))) (= (select (select ?F_55 ?I0_46) ?J0_47) (select (select ?F_55 ?J0_47) ?I0_46))) (= (select (select ?v_0 ?I0_46) ?J0_47) (select (select ?v_0 ?J0_47) ?I0_46)))))) +(assert (forall ((?Body_58 Real)) (= (sum 0 (- 1) ?Body_58) 0.0))) +(assert (not (= def use))) +(assert (not (=> (and (and (and (and (and (and (>= pv5 0) (<= pv5 998)) (> pv5 0)) (forall ((?A_59 Int) (?B_60 Int)) (=> (and (and (and (>= ?A_59 0) (>= ?B_60 0)) (<= ?A_59 5)) (<= ?B_60 5)) (= (select (select q_ds1_filter ?A_59) ?B_60) (select (select q_ds1_filter ?B_60) ?A_59))))) (forall ((?C_61 Int) (?D_62 Int)) (=> (and (and (and (>= ?C_61 0) (>= ?D_62 0)) (<= ?C_61 2)) (<= ?D_62 2)) (= (select (select r_ds1_filter ?C_61) ?D_62) (select (select r_ds1_filter ?D_62) ?C_61))))) (forall ((?E_63 Int) (?F_64 Int)) (=> (and (and (and (>= ?E_63 0) (>= ?F_64 0)) (<= ?E_63 5)) (<= ?F_64 5)) (= (select (select pminus_ds1_filter ?E_63) ?F_64) (select (select pminus_ds1_filter ?F_64) ?E_63))))) (forall ((?G_65 Int)) (=> (and (>= ?G_65 0) (<= ?G_65 5)) (forall ((?H_66 Int)) (=> (and (>= ?H_66 0) (<= ?H_66 5)) (= (select (select id_ds1_filter ?G_65) ?H_66) (select (select id_ds1_filter ?H_66) ?G_65))))))) (forall ((?I_67 Int) (?J_68 Int)) (let ((?v_0 (trans h_ds1_filter))) (let ((?v_1 (tptp_mmul pminus_ds1_filter (tptp_mmul ?v_0 (inv (tptp_madd r_ds1_filter (tptp_mmul h_ds1_filter (tptp_mmul pminus_ds1_filter ?v_0)))))))) (let ((?v_2 (tptp_mmul ?v_1 (tptp_mmul r_ds1_filter (trans ?v_1))))) (=> (and (and (and (>= ?I_67 0) (>= ?J_68 0)) (<= ?I_67 5)) (<= ?J_68 5)) (= (select (select ?v_2 ?I_67) ?J_68) (select (select ?v_2 ?J_68) ?I_67)))))))))) +(check-sat) +(exit) diff --git a/test/regress/regress0/sep/Makefile.am b/test/regress/regress0/sep/Makefile.am index 9d2abaa18..6078bfa19 100644 --- a/test/regress/regress0/sep/Makefile.am +++ b/test/regress/regress0/sep/Makefile.am @@ -53,7 +53,10 @@ TESTS = \ dispose-list-4-init.smt2 \ wand-0526-sat.smt2 \ quant_wand.smt2 \ - fmf-nemp-2.smt2 + fmf-nemp-2.smt2 \ + trees-1.smt2 \ + wand-false.smt2 \ + dup-nemp.smt2 FAILING_TESTS = diff --git a/test/regress/regress0/sep/dup-nemp.smt2 b/test/regress/regress0/sep/dup-nemp.smt2 new file mode 100644 index 000000000..009561128 --- /dev/null +++ b/test/regress/regress0/sep/dup-nemp.smt2 @@ -0,0 +1,7 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) +(declare-sort Loc 0) +(declare-const l Loc) +(assert (sep (not (emp l)) (not (emp l)))) +(assert (pto l l)) +(check-sat) diff --git a/test/regress/regress0/sep/split-find-unsat.smt2 b/test/regress/regress0/sep/split-find-unsat.smt2 index 54530cbf4..1731174fa 100644 --- a/test/regress/regress0/sep/split-find-unsat.smt2 +++ b/test/regress/regress0/sep/split-find-unsat.smt2 @@ -1,7 +1,7 @@ ; COMMAND-LINE: --no-check-models -; EXPECT: sat +; EXPECT: unsat (set-logic ALL_SUPPORTED) -(set-info :status sat) +(set-info :status unsat) (declare-const x Int) (declare-const y Int) diff --git a/test/regress/regress0/sep/trees-1.smt2 b/test/regress/regress0/sep/trees-1.smt2 new file mode 100644 index 000000000..88e875f70 --- /dev/null +++ b/test/regress/regress0/sep/trees-1.smt2 @@ -0,0 +1,41 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(declare-sort Loc 0) +(declare-const loc0 Loc) + +(declare-datatypes () ((Node (node (data Int) (left Loc) (right Loc))))) + +(declare-const dv Int) +(declare-const v Loc) + +(declare-const dl Int) +(declare-const l Loc) +(declare-const dr Int) +(declare-const r Loc) + +(define-fun ten-tree0 ((x Loc) (d Int)) Bool +(or (and (emp loc0) (= x (as sep.nil Loc))) (and (sep (pto x (node d l r)) (and (emp loc0) (= l (as sep.nil Loc))) (and (emp loc0) (= r (as sep.nil Loc)))) (= dl (- d 10)) (= dr (+ d 10))))) + +(declare-const dy Int) +(declare-const y Loc) +(declare-const dz Int) +(declare-const z Loc) + +(define-fun ord-tree0 ((x Loc) (d Int)) Bool +(or (and (emp loc0) (= x (as sep.nil Loc))) (and (sep (pto x (node d y z)) (and (emp loc0) (= y (as sep.nil Loc))) (and (emp loc0) (= z (as sep.nil Loc)))) (<= dy d) (<= d dz)))) + +;------- f ------- +(assert (= y (as sep.nil Loc))) +(assert (= z (as sep.nil Loc))) + +(assert (= dy dv)) +(assert (= dz (+ dv 10))) +;----------------- + +(assert (not (= v (as sep.nil Loc)))) + +(assert (ten-tree0 v dv)) +(assert (not (ord-tree0 v dv))) + +(check-sat) diff --git a/test/regress/regress0/sep/wand-false.smt2 b/test/regress/regress0/sep/wand-false.smt2 new file mode 100644 index 000000000..642c0a8aa --- /dev/null +++ b/test/regress/regress0/sep/wand-false.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(declare-fun x () Int) +(assert (wand (pto x x) false)) +(check-sat) diff --git a/test/regress/regress0/sep/wand-nterm-simp2.smt2 b/test/regress/regress0/sep/wand-nterm-simp2.smt2 index 69305e95c..c317e8736 100644 --- a/test/regress/regress0/sep/wand-nterm-simp2.smt2 +++ b/test/regress/regress0/sep/wand-nterm-simp2.smt2 @@ -1,6 +1,7 @@ ; COMMAND-LINE: --no-check-models -; EXPECT: unsat +; EXPECT: sat (set-logic ALL_SUPPORTED) +(set-info :status sat) (declare-fun x () Int) (assert (wand (pto x 1) (emp x))) (check-sat) diff --git a/test/regress/regress0/sep/wand-simp-sat2.smt2 b/test/regress/regress0/sep/wand-simp-sat2.smt2 index ebc115fdd..059e91317 100755 --- a/test/regress/regress0/sep/wand-simp-sat2.smt2 +++ b/test/regress/regress0/sep/wand-simp-sat2.smt2 @@ -1,6 +1,7 @@ ; COMMAND-LINE: --no-check-models -; EXPECT: unsat +; EXPECT: sat (set-logic ALL_SUPPORTED) +(set-info :status sat) (declare-fun x () Int) (assert (wand (pto x 1) (pto x 3))) (check-sat) diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am index 5069d061e..4e1806aba 100644 --- a/test/regress/regress0/sets/Makefile.am +++ b/test/regress/regress0/sets/Makefile.am @@ -62,7 +62,9 @@ TESTS = \ union-1a.smt2 \ union-1b-flip.smt2 \ union-1b.smt2 \ - union-2.smt2 + union-2.smt2 \ + dt-simp-mem.smt2 \ + card3-ground.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/sets/card3-ground.smt2 b/test/regress/regress0/sets/card3-ground.smt2 new file mode 100644 index 000000000..54a9a5cfc --- /dev/null +++ b/test/regress/regress0/sets/card3-ground.smt2 @@ -0,0 +1,6 @@ +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(declare-fun S () (Set Int)) +(assert (>= (card S) 3)) +(assert (not (member 1 S))) +(check-sat) diff --git a/test/regress/regress0/sets/dt-simp-mem.smt2 b/test/regress/regress0/sets/dt-simp-mem.smt2 new file mode 100644 index 000000000..a38544aa2 --- /dev/null +++ b/test/regress/regress0/sets/dt-simp-mem.smt2 @@ -0,0 +1,9 @@ +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(declare-datatypes () ((D (A (a Int))))) +(declare-fun x1 () D) +(declare-fun S () (Set D)) +(declare-fun P (D) Bool) +(assert (member x1 S)) +(assert (=> (member (A 0) S) (P x1))) +(check-sat) diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index 477d336e6..2e4fd4e1c 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -67,7 +67,6 @@ TESTS = \ bug612.smt2 \ bug615.smt2 \ kaluza-fl.smt2 \ - norn-ab.smt2 \ idof-rewrites.smt2 \ bug682.smt2 \ bug686dd.smt2 \ @@ -78,7 +77,15 @@ TESTS = \ norn-31.smt2 \ strings-native-simple.cvc \ cmu-2db2-extf-reg.smt2 \ - norn-nel-bug-052116.smt2 + norn-nel-bug-052116.smt2 \ + cmu-disagree-0707-dd.smt2 \ + cmu-5042-0707-2.smt2 \ + cmu-dis-0707-3.smt2 \ + nf-ff-contains-abs.smt2 \ + csp-prefix-exp-bug.smt2 \ + cmu-substr-rw.smt2 \ + gm-inc-071516-2.smt2 \ + cmu-inc-nlpp-071516.smt2 FAILING_TESTS = @@ -87,6 +94,9 @@ EXTRA_DIST = $(TESTS) # and make sure to distribute it EXTRA_DIST += +#norn-dis-0707-3.smt2 +#norn-ab.smt2 + # synonyms for "check" .PHONY: regress regress0 test regress regress0 test: check diff --git a/test/regress/regress0/strings/cmu-5042-0707-2.smt2 b/test/regress/regress0/strings/cmu-5042-0707-2.smt2 new file mode 100644 index 000000000..637142dfb --- /dev/null +++ b/test/regress/regress0/strings/cmu-5042-0707-2.smt2 @@ -0,0 +1,15 @@ +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(set-option :strings-exp true) + +(declare-fun key2 () String) +(declare-fun key1 () String) + +(assert +(and +(not +(str.contains (str.++ (str.replace (str.substr key2 0 (- (+ (str.indexof key2 "X" 0) 1) 0)) "X" "x") (str.++ (str.replace (str.substr (str.substr key2 (+ (str.indexof key2 "X" 0) 1) (- (str.len key2) (+ (str.indexof key2 "X" 0) 1))) 0 (- (+ (str.indexof (str.substr key2 (+ (str.indexof key2 "X" 0) 1) (- (str.len key2) (+ (str.indexof key2 "X" 0) 1))) "X" 0) 1) 0)) "X" "x") (str.substr (str.substr key2 (+ (str.indexof key2 "X" 0) 1) (- (str.len key2) (+ (str.indexof key2 "X" 0) 1))) (+ (str.indexof (str.substr key2 (+ (str.indexof key2 "X" 0) 1) (- (str.len key2) (+ (str.indexof key2 "X" 0) 1))) "X" 0) 1) (- (str.len (str.substr key2 (+ (str.indexof key2 "X" 0) 1) (- (str.len key2) (+ (str.indexof key2 "X" 0) 1)))) (+ (str.indexof (str.substr key2 (+ (str.indexof key2 "X" 0) 1) (- (str.len key2) (+ (str.indexof key2 "X" 0) 1))) "X" 0) 1))))) "Z")) +(str.contains (str.substr key2 (+ (str.indexof key2 "X" 0) 1) (- (str.len key2) (+ (str.indexof key2 "X" 0) 1))) "X"))) + +(check-sat) + diff --git a/test/regress/regress0/strings/cmu-dis-0707-3.smt2 b/test/regress/regress0/strings/cmu-dis-0707-3.smt2 new file mode 100644 index 000000000..209cbb3f9 --- /dev/null +++ b/test/regress/regress0/strings/cmu-dis-0707-3.smt2 @@ -0,0 +1,24 @@ +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(set-option :strings-exp true) +(declare-fun value () String) +(declare-fun name () String) +(assert (not (not (not (= (ite (str.contains value "?") 1 0) 0))))) +(assert (not (not (= (ite (str.contains value "#") 1 0) 0)))) +(assert (not (not (= (ite (= (str.substr value 0 (- 2 0)) "//") 1 0) 0)))) +(assert (not (not (= (ite (> (str.indexof value ":" 0) 0) 1 0) 0)))) +(assert (not (= (ite (not (= (str.len value) 0)) 1 0) 0))) +(assert (not (not (= (ite (str.contains value "'") 1 0) 0)))) +(assert (not (not (= (ite (str.contains value "\"") 1 0) 0)))) +(assert (not (not (= (ite (str.contains value ">") 1 0) 0)))) +(assert (not (not (= (ite (str.contains value "<") 1 0) 0)))) +(assert (not (not (= (ite (str.contains value "&") 1 0) 0)))) +(assert (not (not (= (ite (str.contains name "'") 1 0) 0)))) +(assert (not (not (= (ite (str.contains name "\"") 1 0) 0)))) +(assert (not (not (= (ite (str.contains name ">") 1 0) 0)))) +(assert (not (not (= (ite (str.contains name "<") 1 0) 0)))) +(assert (not (not (= (ite (str.contains name "&") 1 0) 0)))) +(assert (not (= (ite (not (= value "")) 1 0) 0))) +(assert (not (= (ite (str.contains value "javascript:alert(1);") 1 0) 0))) +(assert (not (not (= (ite (str.contains name "javascript:alert(1);") 1 0) 0)))) +(check-sat) diff --git a/test/regress/regress0/strings/cmu-disagree-0707-dd.smt2 b/test/regress/regress0/strings/cmu-disagree-0707-dd.smt2 new file mode 100644 index 000000000..c44dfa396 --- /dev/null +++ b/test/regress/regress0/strings/cmu-disagree-0707-dd.smt2 @@ -0,0 +1,22 @@ +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(set-option :strings-exp true) + +(declare-fun url () String) + +(assert +(and +(and +(and +(and + +(= (str.len (str.substr (str.substr url (str.indexof url "#" 2) (- (str.len url) (str.indexof url "#" 2))) (+ (str.indexof (str.substr url (str.indexof url "#" 2) (- (str.len url) (str.indexof url "#" 2))) "#" 0) 1) (- (str.len (str.substr url (str.indexof url "#" 2) (- (str.len url) (str.indexof url "#" 2)))) (+ (str.indexof (str.substr url (str.indexof url "#" 2) (- (str.len url) (str.indexof url "#" 2))) "#" 0) 1)))) 0) + +(not (= (str.substr url 0 (- (str.indexof url ":" 0) 0)) "http"))) +(> (str.indexof url ":" 0) 0)) +(>= (- (str.indexof url "#" 2) 2) 0)) +(>= (str.indexof url ":" 0) 0)) +) + +(check-sat) + diff --git a/test/regress/regress0/strings/cmu-inc-nlpp-071516.smt2 b/test/regress/regress0/strings/cmu-inc-nlpp-071516.smt2 new file mode 100644 index 000000000..1208ca169 --- /dev/null +++ b/test/regress/regress0/strings/cmu-inc-nlpp-071516.smt2 @@ -0,0 +1,9 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) +(set-option :strings-exp true) + +(declare-fun url () String) + +(assert (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (not (= (ite (> (str.indexof url ":" 0) 0) 1 0) 0))) (not (= (ite (str.contains url "javascript:alert(1);") 1 0) 0))) (not (not (= (ite (= (str.len url) 0) 1 0) 0)))) (not (not (= (ite (= (str.at url 0) " ") 1 0) 0)))) (not (not (= (ite (= (str.at url 0) "\t") 1 0) 0)))) (not (not (= (ite (= (str.at url 0) "\n") 1 0) 0)))) (not (not (= (ite (= (str.at url 0) "\r") 1 0) 0)))) (not (not (= (ite (= (str.at url 0) "\v") 1 0) 0)))) (not (not (= (ite (= (str.at url 0) "\f") 1 0) 0)))) (not (not (= (ite (= (str.at url (- (str.len url) 1)) " ") 1 0) 0)))) (not (not (= (ite (= (str.at url (- (str.len url) 1)) "\t") 1 0) 0)))) (not (not (= (ite (= (str.at url (- (str.len url) 1)) "\n") 1 0) 0)))) (not (not (= (ite (= (str.at url (- (str.len url) 1)) "\r") 1 0) 0)))) (not (not (= (ite (= (str.at url (- (str.len url) 1)) "\v") 1 0) 0)))) (not (not (= (ite (= (str.at url (- (str.len url) 1)) "\f") 1 0) 0)))) (not (= (ite (str.prefixof "javascript:alert(1);" url) 1 0) 0)))) + +(check-sat) diff --git a/test/regress/regress0/strings/cmu-substr-rw.smt2 b/test/regress/regress0/strings/cmu-substr-rw.smt2 new file mode 100644 index 000000000..20bf979dd --- /dev/null +++ b/test/regress/regress0/strings/cmu-substr-rw.smt2 @@ -0,0 +1,12 @@ +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(set-option :strings-exp true) +;(set-option :produce-models true) +;(set-option :rewrite-divk true) + +(declare-fun uri () String) + +(assert (and (and (and (and (and (and (and (and (and (and (and (and (not (not (= (ite (= (str.len (str.substr (str.substr uri (+ (str.indexof uri "%" 0) 1) (- (str.len uri) (+ (str.indexof uri "%" 0) 1))) 0 (- 2 0))) 2) 1 0) 0))) (not (not (= (ite (str.contains (str.substr uri (+ (str.indexof uri "%" 0) 1) (- (str.len uri) (+ (str.indexof uri "%" 0) 1))) "%") 1 0) 0)))) (not (not (= (ite (= (str.len (str.substr uri (+ (str.indexof uri "%" 0) 1) (- (str.len uri) (+ (str.indexof uri "%" 0) 1)))) 0) 1 0) 0)))) (not (= (ite (str.contains uri "%") 1 0) 0))) (not (not (= (ite (= (str.len uri) 0) 1 0) 0)))) (>= (+ (str.indexof uri "%" 0) 1) 0)) (>= (- (str.len uri) (+ (str.indexof uri "%" 0) 1)) 0)) (>= 0 0)) (>= (- 2 0) 0)) (>= (+ (str.indexof uri "%" 0) 1) 0)) (>= (- (str.len uri) (+ (str.indexof uri "%" 0) 1)) 0)) (>= (+ (str.indexof uri "%" 0) 1) 0)) (>= (- (str.len uri) (+ (str.indexof uri "%" 0) 1)) 0))) + +(check-sat) + diff --git a/test/regress/regress0/strings/csp-prefix-exp-bug.smt2 b/test/regress/regress0/strings/csp-prefix-exp-bug.smt2 new file mode 100644 index 000000000..c2fb4175c --- /dev/null +++ b/test/regress/regress0/strings/csp-prefix-exp-bug.smt2 @@ -0,0 +1,10 @@ +(set-logic QF_S) +(set-info :status sat) + +(declare-fun x () String) +(declare-fun y () String) +(declare-fun z () String) + +(assert (= (str.len x) 1)) +(assert (= (str.++ x y "b" z) "aaaba")) +(check-sat) diff --git a/test/regress/regress0/strings/gm-inc-071516-2.smt2 b/test/regress/regress0/strings/gm-inc-071516-2.smt2 new file mode 100644 index 000000000..1650190f8 --- /dev/null +++ b/test/regress/regress0/strings/gm-inc-071516-2.smt2 @@ -0,0 +1,10 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) +(set-option :strings-exp true) + +(declare-fun value2 () String) +(declare-fun key2 () String) + +(assert (and (and (and (and (and (and (not (not (= (ite (str.contains value2 "=") 1 0) 0))) (not (not (= (ite (= (str.len value2) 0) 1 0) 0)))) (not (= (ite (not (= (str.indexof value2 "=" 0) (- 1))) 1 0) 0))) (not (not (= (ite (str.contains value2 ",") 1 0) 0)))) (not (not (= (ite (= (str.len value2) 0) 1 0) 0)))) (not (= (ite (= key2 "cache-control") 1 0) 0))) (not (= (ite (= key2 "cache-control") 1 0) 0)))) + +(check-sat) diff --git a/test/regress/regress0/strings/nf-ff-contains-abs.smt2 b/test/regress/regress0/strings/nf-ff-contains-abs.smt2 new file mode 100644 index 000000000..eb6792666 --- /dev/null +++ b/test/regress/regress0/strings/nf-ff-contains-abs.smt2 @@ -0,0 +1,15 @@ +(set-logic QF_S) +(set-info :status unsat) +(declare-fun a () String) +(declare-fun b () String) +(declare-fun c () String) +(declare-fun d () String) +(declare-fun e () String) +(declare-fun f () String) +(declare-fun g () String) +(assert (= (str.++ "abc" a "def" b "gg" c) (str.++ e g f))) +(assert (or (= a "a") (= a "aaa"))) +(assert (or (= b "b") (= b "bbb"))) +(assert (or (= c "c") (= c "ccc"))) +(assert (or (= g (str.++ ";" d)) (= g (str.++ d ";")))) +(check-sat) diff --git a/test/regress/regress0/strings/norn-dis-0707-3.smt2 b/test/regress/regress0/strings/norn-dis-0707-3.smt2 new file mode 100644 index 000000000..bc0f877ad --- /dev/null +++ b/test/regress/regress0/strings/norn-dis-0707-3.smt2 @@ -0,0 +1,26 @@ +(set-logic QF_S) +(set-info :status sat) +(set-option :strings-exp true) + +(declare-fun var_0 () String) +(declare-fun var_1 () String) +(declare-fun var_2 () String) +(declare-fun var_3 () String) +(declare-fun var_4 () String) +(declare-fun var_5 () String) +(declare-fun var_6 () String) +(declare-fun var_7 () String) +(declare-fun var_8 () String) +(declare-fun var_9 () String) +(declare-fun var_10 () String) +(declare-fun var_11 () String) +(declare-fun var_12 () String) + +(assert (str.in.re (str.++ var_8 "z" var_9 ) (re.++ (re.* (re.union (str.to.re "a") (re.++ (str.to.re "b") (re.++ (re.* (re.union (str.to.re "b") (str.to.re "a"))) (str.to.re "z"))))) (re.++ (str.to.re "b") (re.* (re.union (str.to.re "b") (str.to.re "a"))))))) +(assert (str.in.re (str.++ var_8 "z" var_9 ) (re.++ (re.* (re.union (re.union (str.to.re "z") (str.to.re "a")) (re.++ (str.to.re "b") (re.++ (re.* (str.to.re "b")) (re.union (str.to.re "z") (str.to.re "a")))))) (re.++ (str.to.re "b") (re.* (str.to.re "b")))))) +(assert (str.in.re (str.++ var_8 "z" var_9 ) (re.++ (re.* (re.union (str.to.re "a") (re.++ (str.to.re "b") (re.++ (re.* (re.union (str.to.re "z") (str.to.re "a"))) (str.to.re "b"))))) (re.++ (str.to.re "b") (re.* (re.union (str.to.re "z") (str.to.re "a"))))))) +(assert (str.in.re (str.++ var_8 "z" var_9 ) (re.* (re.++ (re.union (str.to.re "b") (str.to.re "a")) (re.++ (re.* (str.to.re "a")) (re.union (str.to.re "z") (str.to.re "b"))))))) +(assert (str.in.re var_9 (re.* (re.range "a" "u")))) +(assert (str.in.re var_8 (re.* (re.range "a" "u")))) +(assert (not (str.in.re (str.++ "b" var_8 "z" "b" var_9 ) (re.++ (re.* (re.++ (str.to.re "b") (str.to.re "z"))) (str.to.re "b"))))) +(check-sat) |