; COMMAND-LINE: --full-saturate-quant
(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)