diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-02-15 15:31:48 -0600 |
---|---|---|
committer | Aina Niemetz <aina.niemetz@gmail.com> | 2018-02-15 13:31:48 -0800 |
commit | 55037e0bcef45c795f28ff3fcf6c1055af465c70 (patch) | |
tree | 397d89bd10e541e1206c5dafdb8cf731feb34730 /test/regress/regress0/quantifiers/opisavailable-12.smt2 | |
parent | 52a39aca19b7238d08c3cebcfa46436a73194008 (diff) |
Refactor regressions (#1581)
Diffstat (limited to 'test/regress/regress0/quantifiers/opisavailable-12.smt2')
-rw-r--r-- | test/regress/regress0/quantifiers/opisavailable-12.smt2 | 276 |
1 files changed, 0 insertions, 276 deletions
diff --git a/test/regress/regress0/quantifiers/opisavailable-12.smt2 b/test/regress/regress0/quantifiers/opisavailable-12.smt2 deleted file mode 100644 index c529b409f..000000000 --- a/test/regress/regress0/quantifiers/opisavailable-12.smt2 +++ /dev/null @@ -1,276 +0,0 @@ -(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) |