diff options
Diffstat (limited to 'test/regress/regress0/quantifiers/set3.smt2')
| -rw-r--r-- | test/regress/regress0/quantifiers/set3.smt2 | 29 |
1 files changed, 29 insertions, 0 deletions
diff --git a/test/regress/regress0/quantifiers/set3.smt2 b/test/regress/regress0/quantifiers/set3.smt2 new file mode 100644 index 000000000..d3e51d996 --- /dev/null +++ b/test/regress/regress0/quantifiers/set3.smt2 @@ -0,0 +1,29 @@ +(set-logic AUFLIA) +(set-info :source | Assertion verification of simple set manipulation programs. |) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status unsat) +(declare-sort Set 0) +(declare-fun member (Int Set) Bool) +(declare-fun insert (Set Int) Set) +(declare-fun delete (Set Int) Set) +(declare-fun sup (Set) Int) +(assert (forall ((?x Int) (?s Set)) (member ?x (insert ?s ?x)))) +(assert (forall ((?x Int) (?y Int) (?s Set)) (=> (not (= ?x ?y)) (= (member ?x (insert ?s ?y)) (member ?x ?s))))) +(assert (forall ((?x Int) (?s Set)) (=> (not (member ?x ?s)) (= (delete ?s ?x) ?s)))) +(assert (forall ((?x Int) (?s Set)) (= (delete (insert ?s ?x) ?x) (delete ?s ?x)))) +(assert (forall ((?x Int) (?y Int) (?s Set)) (=> (not (= ?x ?y)) (= (delete (insert ?s ?y) ?x) (insert (delete ?s ?x) ?y))))) +(assert (forall ((?s Set)) (member (sup ?s) ?s))) +(assert (forall ((?s Set) (?x Int)) (=> (member ?x ?s) (<= ?x (sup ?s))))) +(assert (forall ((?s Set) (?x Int)) (=> (< (sup ?s) ?x) (= (sup (insert ?s ?x)) ?x)))) +(declare-fun arr () (Array Int Int)) +(declare-fun s0 () Set) +(assert (forall ((?i Int)) (=> (> ?i 0) (< (select arr ?i) (sup s0))))) +(declare-fun i1 () Int) +(declare-fun s1 () Set) +(declare-fun g (Int) Int) +(assert (forall ((?i Int)) (> (g ?i) 0))) +(assert (= s1 (insert s0 (select arr (g i1))))) +(assert (not (= (sup s1) (sup s0)))) +(check-sat) +(exit) |