1 files changed, 276 insertions, 0 deletions
diff --git a/test/regress/regress0/quantifiers/opisavailable-12.smt2 b/test/regress/regress0/quantifiers/opisavailable-12.smt2
new file mode 100644
index 000000000..c529b409f
--- /dev/null
+++ b/test/regress/regress0/quantifiers/opisavailable-12.smt2
@@ -0,0 +1,276 @@
+(set-logic AUFLIA)
+(set-info :source |
+      Tokeneer case study <http://www.adacore.com/home/products/gnatpro/tokeneer/>
+  |)
+(set-info :smt-lib-version 2.0)
+(set-info :category "industrial")
+(set-info :status unsat)
+(declare-fun field.datat.length () Int)
+(declare-fun field.datat.minmatchlength () Int)
+(declare-fun field.datat.text () Int)
+(declare-fun field.keyboard__datat.length () Int)
+(declare-fun field.keyboard__datat.text () Int)
+(declare-fun field.t.rolepresent () Int)
+(declare-fun field.t.currentop () Int)
+(declare-fun archivelog () Int)
+(declare-fun character__base__first () Int)
+(declare-fun character__base__last () Int)
+(declare-fun character__first () Int)
+(declare-fun character__last () Int)
+(declare-fun character__size () Int)
+(declare-fun datai__base__first () Int)
+(declare-fun datai__base__last () Int)
+(declare-fun datai__first () Int)
+(declare-fun datai__last () Int)
+(declare-fun datai__size () Int)
+(declare-fun datalengtht__base__first () Int)
+(declare-fun datalengtht__base__last () Int)
+(declare-fun datalengtht__first () Int)
+(declare-fun datalengtht__last () Int)
+(declare-fun datalengtht__size () Int)
+(declare-fun integer__base__first () Int)
+(declare-fun integer__base__last () Int)
+(declare-fun integer__first () Int)
+(declare-fun integer__last () Int)
+(declare-fun integer__size () Int)
+(declare-fun isavailable () Int)
+(declare-fun keyboard__datai__base__first () Int)
+(declare-fun keyboard__datai__base__last () Int)
+(declare-fun keyboard__datai__first () Int)
+(declare-fun keyboard__datai__last () Int)
+(declare-fun keyboard__datai__size () Int)
+(declare-fun keyboard__datalengtht__base__first () Int)
+(declare-fun keyboard__datalengtht__base__last () Int)
+(declare-fun keyboard__datalengtht__first () Int)
+(declare-fun keyboard__datalengtht__last () Int)
+(declare-fun keyboard__datalengtht__size () Int)
+(declare-fun null__string () Int)
+(declare-fun nullop () Int)
+(declare-fun opandnullt__base__first () Int)
+(declare-fun opandnullt__base__last () Int)
+(declare-fun opandnullt__first () Int)
+(declare-fun opandnullt__last () Int)
+(declare-fun opandnullt__size () Int)
+(declare-fun opt__base__first () Int)
+(declare-fun opt__base__last () Int)
+(declare-fun opt__first () Int)
+(declare-fun opt__last () Int)
+(declare-fun opt__size () Int)
+(declare-fun optokeyed () Int)
+(declare-fun overridelock () Int)
+(declare-fun positive__base__first () Int)
+(declare-fun positive__base__last () Int)
+(declare-fun positive__first () Int)
+(declare-fun positive__last () Int)
+(declare-fun positive__size () Int)
+(declare-fun privtypes__adminprivileget__base__first () Int)
+(declare-fun privtypes__adminprivileget__base__last () Int)
+(declare-fun privtypes__adminprivileget__first () Int)
+(declare-fun privtypes__adminprivileget__last () Int)
+(declare-fun privtypes__adminprivileget__size () Int)
+(declare-fun privtypes__auditmanager () Int)
+(declare-fun privtypes__guard () Int)
+(declare-fun privtypes__privileget__base__first () Int)
+(declare-fun privtypes__privileget__base__last () Int)
+(declare-fun privtypes__privileget__first () Int)
+(declare-fun privtypes__privileget__last () Int)
+(declare-fun privtypes__privileget__size () Int)
+(declare-fun privtypes__securityofficer () Int)
+(declare-fun privtypes__useronly () Int)
+(declare-fun shutdownop () Int)
+(declare-fun updateconfigdata () Int)
+(declare-fun keyedop () Int)
+(declare-fun keyedop__entry__loop__2 () Int)
+(declare-fun init.keyedop__entry__loop__2 () Int)
+(declare-fun init.keyedop () Int)
+(declare-fun loop__1__op () Int)
+(declare-fun init.loop__1__op () Int)
+(declare-fun loop__2__i () Int)
+(declare-fun init.loop__2__i () Int)
+(declare-fun theadmin () Int)
+(declare-fun init.theadmin () Int)
+(declare-fun theop () Int)
+(declare-fun init.theop () Int)
+(declare-fun bit__and (Int Int) Int)
+(declare-fun bit__not (Int Int) Int)
+(declare-fun bit__or (Int Int) Int)
+(declare-fun bit__xor (Int Int) Int)
+(declare-fun character__pos (Int) Int)
+(declare-fun character__val (Int) Int)
+(declare-fun integer__pred (Int) Int)
+(declare-fun integer__succ (Int) Int)
+(declare-fun opandnullt__pos (Int) Int)
+(declare-fun opandnullt__pred (Int) Int)
+(declare-fun opandnullt__succ (Int) Int)
+(declare-fun opandnullt__val (Int) Int)
+(declare-fun privtypes__privileget__pos (Int) Int)
+(declare-fun privtypes__privileget__pred (Int) Int)
+(declare-fun privtypes__privileget__succ (Int) Int)
+(declare-fun privtypes__privileget__val (Int) Int)
+(declare-fun round__ (Int) Int)
+(declare-fun i.div (Int Int) Int)
+(declare-fun i.mod (Int Int) Int)
+(declare-fun i.mult (Int Int) Int)
+(declare-fun i.exp (Int Int) Int)
+(declare-fun tm.true () Int)
+(declare-fun tm.false () Int)
+(declare-fun tm.not (Int) Int)
+(declare-fun tm.and (Int Int) Int)
+(declare-fun tm.or (Int Int) Int)
+(declare-fun tm.iff (Int Int) Int)
+(declare-fun tm.eq (Int Int) Int)
+(declare-fun tm.ne (Int Int) Int)
+(declare-fun tm.lt (Int Int) Int)
+(declare-fun tm.le (Int Int) Int)
+(declare-fun tuple.2 (Int Int) Int)
+(declare-fun a.store (Int Int Int) Int)
+(declare-fun a.select (Int Int) Int)
+(declare-fun a.mk_const_array (Int) Int)
+(declare-fun a.default_array () Int)
+(declare-fun r.default_record () Int)
+(declare-fun matched () Bool)
+(declare-fun init.matched () Bool)
+(declare-fun ispresent (Int) Bool)
+(declare-fun opandnullt__LE (Int Int) Bool)
+(declare-fun opandnullt__LT (Int Int) Bool)
+(declare-fun privtypes__privileget__LE (Int Int) Bool)
+(declare-fun privtypes__privileget__LT (Int Int) Bool)
+(assert (forall ((?i Int)) (=> (and (<= 0 ?i) (< ?i 4)) (= (privtypes__privileget__pos ?i) ?i))))
+(assert (forall ((?i Int)) (=> (and (<= 0 ?i) (< ?i 4)) (= (privtypes__privileget__val ?i) ?i))))
+(assert (forall ((?i Int)) (=> (and (<= 0 ?i) (< ?i 3)) (= (privtypes__privileget__succ ?i) (+ ?i 1)))))
+(assert (forall ((?i Int)) (=> (and (<= 1 ?i) (< ?i 4)) (= (privtypes__privileget__pred ?i) (- ?i 1)))))
+(assert (= privtypes__useronly 0))
+(assert (= privtypes__guard 1))
+(assert (= privtypes__auditmanager 2))
+(assert (= privtypes__securityofficer 3))
+(assert (forall ((?i Int)) (=> (and (<= 0 ?i) (< ?i 5)) (= (opandnullt__pos ?i) ?i))))
+(assert (forall ((?i Int)) (=> (and (<= 0 ?i) (< ?i 5)) (= (opandnullt__val ?i) ?i))))
+(assert (forall ((?i Int)) (=> (and (<= 0 ?i) (< ?i 4)) (= (opandnullt__succ ?i) (+ ?i 1)))))
+(assert (forall ((?i Int)) (=> (and (<= 1 ?i) (< ?i 5)) (= (opandnullt__pred ?i) (- ?i 1)))))
+(assert (= nullop 0))
+(assert (= archivelog 1))
+(assert (= updateconfigdata 2))
+(assert (= overridelock 3))
+(assert (= shutdownop 4))
+(assert (forall ((?I Int)) (=> (and (<= archivelog ?I) (<= ?I shutdownop)) (<= datalengtht__first (a.select (a.select optokeyed ?I) field.datat.length)))))
+(assert (forall ((?I Int)) (=> (and (<= archivelog ?I) (<= ?I shutdownop)) (<= (a.select (a.select optokeyed ?I) field.datat.length) datalengtht__last))))
+(assert (forall ((?I Int)) (=> (and (<= archivelog ?I) (<= ?I shutdownop)) (<= datai__first (a.select (a.select optokeyed ?I) field.datat.minmatchlength)))))
+(assert (forall ((?I Int)) (=> (and (<= archivelog ?I) (<= ?I shutdownop)) (<= (a.select (a.select optokeyed ?I) field.datat.minmatchlength) datai__last))))
+(assert (forall ((?I Int) (?J Int)) (=> (and (<= archivelog ?I) (<= ?I shutdownop) (<= 1 ?J) (<= ?J 18)) (<= character__first (a.select (a.select (a.select optokeyed ?I) field.datat.text) ?J)))))
+(assert (forall ((?I Int) (?J Int)) (=> (and (<= archivelog ?I) (<= ?I shutdownop) (<= 1 ?J) (<= ?J 18)) (<= (a.select (a.select (a.select optokeyed ?I) field.datat.text) ?J) character__last))))
+(assert (<= 0 integer__size))
+(assert (= integer__first (- 2147483648)))
+(assert (= integer__last 2147483647))
+(assert (= integer__base__first (- 2147483648)))
+(assert (= integer__base__last 2147483647))
+(assert (<= 0 character__size))
+(assert (= character__first 0))
+(assert (= character__last 255))
+(assert (= character__base__first 0))
+(assert (= character__base__last 255))
+(assert (<= 0 positive__size))
+(assert (= positive__first 1))
+(assert (= positive__last 2147483647))
+(assert (= positive__base__first (- 2147483648)))
+(assert (= positive__base__last 2147483647))
+(assert (<= 0 privtypes__privileget__size))
+(assert (= privtypes__privileget__first privtypes__useronly))
+(assert (= privtypes__privileget__last privtypes__securityofficer))
+(assert (= privtypes__privileget__base__first privtypes__useronly))
+(assert (= privtypes__privileget__base__last privtypes__securityofficer))
+(assert (<= 0 privtypes__adminprivileget__size))
+(assert (= privtypes__adminprivileget__first privtypes__guard))
+(assert (= privtypes__adminprivileget__last privtypes__securityofficer))
+(assert (= privtypes__adminprivileget__base__first privtypes__useronly))
+(assert (= privtypes__adminprivileget__base__last privtypes__securityofficer))
+(assert (<= 0 keyboard__datalengtht__size))
+(assert (= keyboard__datalengtht__first 0))
+(assert (= keyboard__datalengtht__last 78))
+(assert (= keyboard__datalengtht__base__first (- 2147483648)))
+(assert (= keyboard__datalengtht__base__last 2147483647))
+(assert (<= 0 keyboard__datai__size))
+(assert (= keyboard__datai__first 1))
+(assert (= keyboard__datai__last 78))
+(assert (= keyboard__datai__base__first (- 2147483648)))
+(assert (= keyboard__datai__base__last 2147483647))
+(assert (<= 0 opandnullt__size))
+(assert (= opandnullt__first nullop))
+(assert (= opandnullt__last shutdownop))
+(assert (= opandnullt__base__first nullop))
+(assert (= opandnullt__base__last shutdownop))
+(assert (<= 0 opt__size))
+(assert (= opt__first archivelog))
+(assert (= opt__last shutdownop))
+(assert (= opt__base__first nullop))
+(assert (= opt__base__last shutdownop))
+(assert (<= 0 datalengtht__size))
+(assert (= datalengtht__first 0))
+(assert (= datalengtht__last 18))
+(assert (= datalengtht__base__first (- 2147483648)))
+(assert (= datalengtht__base__last 2147483647))
+(assert (<= 0 datai__size))
+(assert (= datai__first 1))
+(assert (= datai__last 18))
+(assert (= datai__base__first (- 2147483648)))
+(assert (= datai__base__last 2147483647))
+(assert (forall ((?X Int) (?Y Int)) (=> (< 0 ?Y) (<= 0 (i.mod ?X ?Y)))))
+(assert (forall ((?X Int) (?Y Int)) (=> (< 0 ?Y) (< (i.mod ?X ?Y) ?Y))))
+(assert (forall ((?X Int) (?Y Int)) (=> (and (<= 0 ?X) (< 0 ?Y)) (<= (i.mult ?Y (i.div ?X ?Y)) ?X))))
+(assert (forall ((?X Int) (?Y Int)) (=> (and (<= 0 ?X) (< 0 ?Y)) (< (- ?X ?Y) (i.mult ?Y (i.div ?X ?Y))))))
+(assert (forall ((?X Int) (?Y Int)) (=> (and (<= ?X 0) (< 0 ?Y)) (<= ?X (i.mult ?Y (i.div ?X ?Y))))))
+(assert (forall ((?X Int) (?Y Int)) (=> (and (<= ?X 0) (< 0 ?Y)) (< (i.mult ?Y (i.div ?X ?Y)) (+ ?X ?Y)))))
+(assert (forall ((?X Int) (?Y Int)) (=> (and (<= 0 ?X) (<= 0 ?Y)) (<= 0 (bit__or ?X ?Y)))))
+(assert (forall ((?X Int) (?Y Int)) (=> (and (<= 0 ?X) (<= 0 ?Y)) (<= ?X (bit__or ?X ?Y)))))
+(assert (forall ((?X Int) (?Y Int)) (=> (and (<= 0 ?X) (<= 0 ?Y)) (<= ?Y (bit__or ?X ?Y)))))
+(assert (forall ((?X Int) (?Y Int)) (=> (and (<= 0 ?X) (<= 0 ?Y)) (<= (bit__or ?X ?Y) (+ ?X ?Y)))))
+(assert (distinct field.datat.length field.datat.minmatchlength field.datat.text))
+(assert (distinct field.keyboard__datat.length field.keyboard__datat.text))
+(assert (distinct field.t.rolepresent field.t.currentop))
+(assert (distinct tm.true tm.false))
+(assert (forall ((?x Int)) (! (= (= (tm.not ?x) tm.true) (not (= ?x tm.true))) :pattern ((tm.not ?x)) )))
+(assert (forall ((?x Int) (?y Int)) (! (= (= (tm.and ?x ?y) tm.true) (and (= ?x tm.true) (= ?y tm.true))) :pattern ((tm.and ?x ?y)) )))
+(assert (forall ((?x Int) (?y Int)) (! (= (= (tm.or ?x ?y) tm.true) (or (= ?x tm.true) (= ?y tm.true))) :pattern ((tm.or ?x ?y)) )))
+(assert (forall ((?x Int) (?y Int)) (! (= (= (tm.iff ?x ?y) tm.true) (= (= ?x tm.true) (= ?y tm.true))) :pattern ((tm.iff ?x ?y)) )))
+(assert (forall ((?x Int) (?y Int)) (! (= (= (tm.eq ?x ?y) tm.true) (= ?x ?y)) :pattern ((tm.eq ?x ?y)) )))
+(assert (forall ((?x Int) (?y Int)) (! (= (= (tm.ne ?x ?y) tm.true) (not (= ?x ?y))) :pattern ((tm.ne ?x ?y)) )))
+(assert (forall ((?x Int) (?y Int)) (! (= (= (tm.lt ?x ?y) tm.true) (< ?x ?y)) :pattern ((tm.lt ?x ?y)) )))
+(assert (forall ((?x Int) (?y Int)) (! (= (= (tm.le ?x ?y) tm.true) (<= ?x ?y)) :pattern ((tm.le ?x ?y)) )))
+(assert (forall ((?a Int) (?i Int) (?v Int)) (! (= (a.select (a.store ?a ?i ?v) ?i) ?v) :pattern ((a.select (a.store ?a ?i ?v) ?i)) )))
+(assert (forall ((?a Int) (?i Int) (?v Int) (?j Int)) (! (or (= ?i ?j) (= (a.select (a.store ?a ?i ?v) ?j) (a.select ?a ?j))) :pattern ((a.select (a.store ?a ?i ?v) ?j)) )))
+(assert (forall ((?i Int) (?v Int)) (! (= (a.select (a.mk_const_array ?v) ?i) ?v) :pattern ((a.select (a.mk_const_array ?v) ?i)) )))
+(assert (<= opt__first loop__1__op))
+(assert (<= loop__1__op opt__last))
+(assert (<= datai__first loop__2__i))
+(assert (<= loop__2__i datai__last))
+(assert (<= loop__2__i (a.select keyedop field.keyboard__datat.length)))
+(assert (<= datai__first (a.select keyedop field.keyboard__datat.length)))
+(assert (<= (a.select keyedop field.keyboard__datat.length) datai__last))
+(assert (= keyedop keyedop__entry__loop__2))
+(assert (<= privtypes__adminprivileget__first (a.select theadmin field.t.rolepresent)))
+(assert (<= (a.select theadmin field.t.rolepresent) privtypes__adminprivileget__last))
+(assert (= theop nullop))
+(assert (<= opandnullt__first (a.select theadmin field.t.currentop)))
+(assert (<= (a.select theadmin field.t.currentop) opandnullt__last))
+(assert (<= privtypes__privileget__first (a.select theadmin field.t.rolepresent)))
+(assert (<= (a.select theadmin field.t.rolepresent) privtypes__privileget__last))
+(assert (forall ((?i___1 Int)) (let ((?v_0 (a.select (a.select keyedop field.keyboard__datat.text) ?i___1))) (=> (and (<= keyboard__datai__first ?i___1) (<= ?i___1 keyboard__datai__last)) (and (<= character__first ?v_0) (<= ?v_0 character__last))))))
+(assert (<= keyboard__datalengtht__first (a.select keyedop field.keyboard__datat.length)))
+(assert (<= (a.select keyedop field.keyboard__datat.length) keyboard__datalengtht__last))
+(assert (ispresent theadmin))
+(assert (<= datai__first loop__2__i))
+(assert (<= loop__2__i datai__last))
+(assert (<= loop__2__i (a.select keyedop__entry__loop__2 field.keyboard__datat.length)))
+(assert (<= opt__first loop__1__op))
+(assert (<= loop__1__op opt__last))
+(assert (<= loop__1__op opt__last))
+(assert (<= keyboard__datai__first loop__2__i))
+(assert (<= loop__2__i keyboard__datai__last))
+(assert (<= datai__first loop__2__i))
+(assert (<= loop__2__i datai__last))
+(assert (<= opt__first loop__1__op))
+(assert (<= loop__1__op opt__last))
+(assert (not (not (= (a.select (a.select (a.select optokeyed loop__1__op) field.datat.text) loop__2__i) (a.select (a.select keyedop field.keyboard__datat.text) loop__2__i)))))
+(assert (not (= loop__2__i (a.select keyedop__entry__loop__2 field.keyboard__datat.length))))
+(assert (let ((?v_6 (<= opt__first loop__1__op)) (?v_7 (<= loop__1__op opt__last)) (?v_1 (a.select keyedop field.keyboard__datat.length)) (?v_2 (a.select theadmin field.t.rolepresent)) (?v_3 (a.select theadmin field.t.currentop)) (?v_0 (+ loop__2__i 1))) (let ((?v_4 (<= datai__first ?v_0)) (?v_5 (<= ?v_0 datai__last))) (not (and ?v_6 ?v_7 ?v_4 ?v_5 (<= ?v_0 ?v_1) (<= datai__first ?v_1) (<= ?v_1 datai__last) (= keyedop keyedop__entry__loop__2) (<= privtypes__adminprivileget__first ?v_2) (<= ?v_2 privtypes__adminprivileget__last) (= theop nullop) (<= opandnullt__first ?v_3) (<= ?v_3 opandnullt__last) (<= privtypes__privileget__first ?v_2) (<= ?v_2 privtypes__privileget__last) (forall ((?i___1 Int)) (let ((?v_8 (a.select (a.select keyedop field.keyboard__datat.text) ?i___1))) (=> (and (<= keyboard__datai__first ?i___1) (<= ?i___1 keyboard__datai__last)) (and (<= character__first ?v_8) (<= ?v_8 character__last))))) (<= keyboard__datalengtht__first ?v_1) (<= ?v_1 keyboard__datalengtht__last) (ispresent theadmin) ?v_4 ?v_5 (<= ?v_0 (a.select keyedop__entry__loop__2 field.keyboard__datat.length)) ?v_6 ?v_7 ?v_7)))))
+(check-sat)
+(exit)