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