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/regress1/quantifiers/inst-max-level-segf.smt2 | |
parent | 52a39aca19b7238d08c3cebcfa46436a73194008 (diff) |
Refactor regressions (#1581)
Diffstat (limited to 'test/regress/regress1/quantifiers/inst-max-level-segf.smt2')
-rw-r--r-- | test/regress/regress1/quantifiers/inst-max-level-segf.smt2 | 326 |
1 files changed, 326 insertions, 0 deletions
diff --git a/test/regress/regress1/quantifiers/inst-max-level-segf.smt2 b/test/regress/regress1/quantifiers/inst-max-level-segf.smt2 new file mode 100644 index 000000000..d85f3d094 --- /dev/null +++ b/test/regress/regress1/quantifiers/inst-max-level-segf.smt2 @@ -0,0 +1,326 @@ +; COMMAND-LINE: --inst-max-level=0 --simplification=none +; EXPECT: unsat +(set-logic UF) +(set-info :status unsat) +(declare-sort Node 0) +(declare-sort GrassPat 0) +(declare-sort GrassArray 1) +(declare-sort ArrayCell 1) +(declare-sort Loc 1) +(declare-sort Set 1) +(declare-sort Map 2) +(declare-sort GrassByte 0) +(declare-fun grass_null$0 () (Loc Node)) +(declare-fun grass_read$0 ((Map (Loc Node) (Loc Node)) (Loc Node)) + (Loc Node)) +(declare-fun grass_emptyset$0 () (Set (Loc Node))) +(declare-fun grass_singleton$0 ((Loc Node)) (Set (Loc Node))) +(declare-fun grass_union$0 ((Set (Loc Node)) (Set (Loc Node))) + (Set (Loc Node))) +(declare-fun grass_intersection$0 ((Set (Loc Node)) (Set (Loc Node))) + (Set (Loc Node))) +(declare-fun grass_setminus$0 ((Set (Loc Node)) (Set (Loc Node))) + (Set (Loc Node))) +(declare-fun grass_Btwn$0 ((Map (Loc Node) (Loc Node)) (Loc Node) (Loc Node) + (Loc Node)) Bool) +(declare-fun grass_member$0 ((Loc Node) (Set (Loc Node))) Bool) +(declare-fun grass_known$0 ((Map (Loc Node) (Loc Node))) GrassPat) +(declare-fun grass_known$1 (Bool) GrassPat) +(declare-fun Alloc_Node$0 () (Set (Loc Node))) +(declare-fun FP_Caller_Node$0 () (Set (Loc Node))) +(declare-fun FP_Caller_Node_1$0 () (Set (Loc Node))) +(declare-fun FP_Caller_final_Node_2$0 () (Set (Loc Node))) +(declare-fun FP_Node$0 () (Set (Loc Node))) +(declare-fun Label$0 () Bool) +(declare-fun Label_1$0 () Bool) +(declare-fun Label_2$0 () Bool) +(declare-fun Label_3$0 () Bool) +(declare-fun elt$0 () (Loc Node)) +(declare-fun lseg$0 ((Map (Loc Node) (Loc Node)) (Loc Node) (Loc Node) + (Set (Loc Node))) Bool) +(declare-fun lst$0 () (Loc Node)) +(declare-fun next$0 () (Map (Loc Node) (Loc Node))) +(declare-fun res_2$0 () (Loc Node)) +(declare-fun set_compr$0 ((Map (Loc Node) (Loc Node)) (Loc Node) (Loc Node)) + (Set (Loc Node))) +(declare-fun sk_?X$0 () (Set (Loc Node))) +(declare-fun sk_?X_1$0 () (Set (Loc Node))) +(declare-fun sk_?X_2$0 () (Set (Loc Node))) +(declare-fun sk_?X_3$0 () (Set (Loc Node))) +(declare-fun sk_?X_4$0 () (Set (Loc Node))) +(declare-fun sk_?e$0 () (Loc Node)) + +(assert (not (grass_member$0 grass_null$0 Alloc_Node$0))) +(assert + (and + (or + (or + (and (and (grass_member$0 sk_?e$0 sk_?X_4$0) Label_1$0) + (and + (not + (grass_member$0 sk_?e$0 + (set_compr$0 next$0 res_2$0 grass_null$0))) + Label_1$0)) + (and + (and + (grass_member$0 sk_?e$0 + (set_compr$0 next$0 res_2$0 grass_null$0)) + Label_1$0) + (and (not (grass_member$0 sk_?e$0 sk_?X_4$0)) Label_1$0))) + (and + (not (grass_Btwn$0 next$0 res_2$0 grass_null$0 grass_null$0)) + Label$0)) + Label_2$0)) +(assert (forall ((x (Loc Node))) (not (grass_member$0 x grass_emptyset$0)))) +(assert + (forall ((y (Loc Node)) (x (Loc Node))) + (or (and (= x y) (grass_member$0 x (grass_singleton$0 y))) + (and (not (= x y)) + (not (grass_member$0 x (grass_singleton$0 y))))))) +(assert + (forall ((x (Loc Node))) + (or + (and (grass_member$0 x FP_Caller_Node$0) + (grass_member$0 x + (grass_setminus$0 FP_Caller_Node$0 FP_Node$0)) + (not (grass_member$0 x FP_Node$0))) + (and + (or (grass_member$0 x FP_Node$0) + (not (grass_member$0 x FP_Caller_Node$0))) + (not + (grass_member$0 x + (grass_setminus$0 FP_Caller_Node$0 FP_Node$0))))))) +(assert + (forall ((x (Loc Node))) + (or + (and (grass_member$0 x Alloc_Node$0) + (grass_member$0 x + (grass_setminus$0 Alloc_Node$0 Alloc_Node$0)) + (not (grass_member$0 x Alloc_Node$0))) + (and + (or (grass_member$0 x Alloc_Node$0) + (not (grass_member$0 x Alloc_Node$0))) + (not + (grass_member$0 x + (grass_setminus$0 Alloc_Node$0 Alloc_Node$0))))))) +(assert + (forall ((x (Loc Node))) + (or + (and (grass_member$0 x Alloc_Node$0) + (grass_member$0 x FP_Node$0) + (grass_member$0 x + (grass_intersection$0 Alloc_Node$0 FP_Node$0))) + (and + (or (not (grass_member$0 x Alloc_Node$0)) + (not (grass_member$0 x FP_Node$0))) + (not + (grass_member$0 x + (grass_intersection$0 Alloc_Node$0 FP_Node$0))))))) +(assert + (forall ((x (Loc Node))) + (or + (and (grass_member$0 x sk_?X$0) + (grass_member$0 x sk_?X_1$0) + (grass_member$0 x + (grass_intersection$0 sk_?X$0 sk_?X_1$0))) + (and + (or (not (grass_member$0 x sk_?X$0)) + (not (grass_member$0 x sk_?X_1$0))) + (not + (grass_member$0 x + (grass_intersection$0 sk_?X$0 sk_?X_1$0))))))) +(assert + (forall ((x (Loc Node))) + (or + (and + (grass_member$0 x + (grass_union$0 + (grass_intersection$0 Alloc_Node$0 FP_Node$0) + (grass_setminus$0 Alloc_Node$0 Alloc_Node$0))) + (or + (grass_member$0 x + (grass_intersection$0 Alloc_Node$0 FP_Node$0)) + (grass_member$0 x + (grass_setminus$0 Alloc_Node$0 Alloc_Node$0)))) + (and + (not + (grass_member$0 x + (grass_intersection$0 Alloc_Node$0 FP_Node$0))) + (not + (grass_member$0 x + (grass_setminus$0 Alloc_Node$0 Alloc_Node$0))) + (not + (grass_member$0 x + (grass_union$0 + (grass_intersection$0 Alloc_Node$0 FP_Node$0) + (grass_setminus$0 Alloc_Node$0 Alloc_Node$0)))))))) +(assert + (forall ((x (Loc Node))) + (or + (and (grass_member$0 x (grass_union$0 sk_?X$0 sk_?X_1$0)) + (or (grass_member$0 x sk_?X$0) + (grass_member$0 x sk_?X_1$0))) + (and (not (grass_member$0 x sk_?X$0)) + (not (grass_member$0 x sk_?X_1$0)) + (not + (grass_member$0 x (grass_union$0 sk_?X$0 sk_?X_1$0))))))) +(assert + (forall ((x (Loc Node))) + (or + (and + (grass_member$0 x + (grass_union$0 FP_Caller_Node_1$0 FP_Node$0)) + (or (grass_member$0 x FP_Caller_Node_1$0) + (grass_member$0 x FP_Node$0))) + (and (not (grass_member$0 x FP_Caller_Node_1$0)) + (not (grass_member$0 x FP_Node$0)) + (not + (grass_member$0 x + (grass_union$0 FP_Caller_Node_1$0 FP_Node$0))))))) +(assert + (forall ((x (Loc Node))) + (or + (and + (grass_member$0 x + (grass_union$0 FP_Node$0 FP_Caller_Node$0)) + (or (grass_member$0 x FP_Node$0) + (grass_member$0 x FP_Caller_Node$0))) + (and (not (grass_member$0 x FP_Node$0)) + (not (grass_member$0 x FP_Caller_Node$0)) + (not + (grass_member$0 x + (grass_union$0 FP_Node$0 FP_Caller_Node$0))))))) +(assert + (forall ((x (Loc Node))) + (or + (and + (grass_member$0 x + (grass_union$0 FP_Caller_Node$0 Alloc_Node$0)) + (or (grass_member$0 x FP_Caller_Node$0) + (grass_member$0 x Alloc_Node$0))) + (and (not (grass_member$0 x FP_Caller_Node$0)) + (not (grass_member$0 x Alloc_Node$0)) + (not + (grass_member$0 x + (grass_union$0 FP_Caller_Node$0 Alloc_Node$0))))))) +(assert + (or (grass_Btwn$0 next$0 lst$0 lst$0 lst$0) + (not (lseg$0 next$0 lst$0 lst$0 sk_?X$0)))) +(assert + (forall + ((next (Map (Loc Node) (Loc Node))) (x (Loc Node)) + (y (Loc Node)) (z (Loc Node))) + (or + (and (grass_Btwn$0 next x z y) + (grass_member$0 z (set_compr$0 next x y)) (not (= z y))) + (and (or (= z y) (not (grass_Btwn$0 next x z y))) + (not (grass_member$0 z (set_compr$0 next x y))))))) +(assert + (forall + ((?u (Loc Node)) (?x (Loc Node)) (?y (Loc Node)) + (?z (Loc Node))) + (or (not (grass_Btwn$0 next$0 ?x ?y ?z)) + (not (grass_Btwn$0 next$0 ?x ?u ?y)) + (and (grass_Btwn$0 next$0 ?x ?u ?z) + (grass_Btwn$0 next$0 ?u ?y ?z))))) +(assert + (forall + ((?u (Loc Node)) (?x (Loc Node)) (?y (Loc Node)) + (?z (Loc Node))) + (or (not (grass_Btwn$0 next$0 ?x ?y ?z)) + (not (grass_Btwn$0 next$0 ?y ?u ?z)) + (and (grass_Btwn$0 next$0 ?x ?y ?u) + (grass_Btwn$0 next$0 ?x ?u ?z))))) +(assert + (forall ((?x (Loc Node)) (?y (Loc Node)) (?z (Loc Node))) + (or (not (grass_Btwn$0 next$0 ?x ?y ?y)) + (not (grass_Btwn$0 next$0 ?y ?z ?z)) + (grass_Btwn$0 next$0 ?x ?z ?z)))) +(assert + (forall ((?x (Loc Node)) (?y (Loc Node)) (?z (Loc Node))) + (or (not (grass_Btwn$0 next$0 ?x ?y ?z)) + (and (grass_Btwn$0 next$0 ?x ?y ?y) + (grass_Btwn$0 next$0 ?y ?z ?z))))) +(assert + (forall ((?x (Loc Node)) (?y (Loc Node)) (?z (Loc Node))) + (or (not (grass_Btwn$0 next$0 ?x ?y ?y)) + (not (grass_Btwn$0 next$0 ?x ?z ?z)) + (grass_Btwn$0 next$0 ?x ?y ?z) + (grass_Btwn$0 next$0 ?x ?z ?y)))) +(assert + (forall ((?x (Loc Node)) (?y (Loc Node))) + (or (not (grass_Btwn$0 next$0 ?x ?y ?x)) (= ?x ?y)))) +(assert + (forall ((?y (Loc Node))) + (or (not (grass_Btwn$0 next$0 res_2$0 ?y ?y)) (= res_2$0 ?y) + (grass_Btwn$0 next$0 res_2$0 (grass_read$0 next$0 res_2$0) + ?y)))) +(assert + (forall ((?y (Loc Node))) + (or (not (grass_Btwn$0 next$0 lst$0 ?y ?y)) (= lst$0 ?y) + (grass_Btwn$0 next$0 lst$0 (grass_read$0 next$0 lst$0) ?y)))) +(assert + (forall ((?y (Loc Node))) + (or (not (= (grass_read$0 next$0 res_2$0) res_2$0)) + (not (grass_Btwn$0 next$0 res_2$0 ?y ?y)) (= res_2$0 ?y)))) +(assert + (forall ((?y (Loc Node))) + (or (not (= (grass_read$0 next$0 lst$0) lst$0)) + (not (grass_Btwn$0 next$0 lst$0 ?y ?y)) (= lst$0 ?y)))) +(assert + (grass_Btwn$0 next$0 res_2$0 (grass_read$0 next$0 res_2$0) + (grass_read$0 next$0 res_2$0))) +(assert + (grass_Btwn$0 next$0 lst$0 (grass_read$0 next$0 lst$0) + (grass_read$0 next$0 lst$0))) +(assert (forall ((?x (Loc Node))) (grass_Btwn$0 next$0 ?x ?x ?x))) +(assert + (or (= sk_?X$0 (set_compr$0 next$0 lst$0 lst$0)) + (not (lseg$0 next$0 lst$0 lst$0 sk_?X$0)))) +(assert (= (grass_read$0 next$0 grass_null$0) grass_null$0)) +(assert (= FP_Caller_Node_1$0 (grass_setminus$0 FP_Caller_Node$0 FP_Node$0))) +(assert (and (= lst$0 grass_null$0) Label_3$0)) +(assert (= Alloc_Node$0 (grass_union$0 FP_Caller_Node$0 Alloc_Node$0))) +(assert + (= sk_?X_4$0 + (grass_union$0 (grass_intersection$0 Alloc_Node$0 FP_Node$0) + (grass_setminus$0 Alloc_Node$0 Alloc_Node$0)))) +(assert (= sk_?X_3$0 (grass_union$0 sk_?X$0 sk_?X_2$0))) +(assert (= sk_?X_2$0 sk_?X_1$0)) +(assert (= sk_?X_1$0 (grass_singleton$0 elt$0))) +(assert (= (grass_read$0 next$0 elt$0) grass_null$0)) +(assert (= FP_Node$0 sk_?X_3$0)) +(assert (= FP_Caller_Node$0 (grass_union$0 FP_Node$0 FP_Caller_Node$0))) +(assert (= grass_emptyset$0 (grass_intersection$0 sk_?X$0 sk_?X_2$0))) +(assert (= grass_emptyset$0 grass_emptyset$0)) +(assert (lseg$0 next$0 lst$0 grass_null$0 sk_?X$0)) +(assert + (= FP_Caller_final_Node_2$0 + (grass_union$0 FP_Caller_Node_1$0 FP_Node$0))) +(assert (= res_2$0 elt$0)) +(assert (= (grass_union$0 FP_Caller_Node$0 Alloc_Node$0) Alloc_Node$0)) +(assert (= (grass_read$0 next$0 grass_null$0) grass_null$0)) +(assert (= (grass_read$0 next$0 grass_null$0) lst$0)) +(assert (= (grass_read$0 next$0 grass_null$0) (grass_read$0 next$0 elt$0))) +(assert + (= (grass_known$1 (lseg$0 next$0 lst$0 grass_null$0 sk_?X$0)) + (grass_known$1 (lseg$0 next$0 lst$0 lst$0 sk_?X$0)))) +(assert (= (grass_intersection$0 sk_?X$0 sk_?X_2$0) grass_emptyset$0)) +(assert + (= + (grass_union$0 (grass_intersection$0 Alloc_Node$0 FP_Node$0) + (grass_setminus$0 Alloc_Node$0 Alloc_Node$0)) + sk_?X_4$0)) +(assert (= res_2$0 elt$0)) +(assert (= (grass_union$0 FP_Node$0 FP_Caller_Node$0) FP_Caller_Node$0)) +(assert (= sk_?X_1$0 (grass_singleton$0 elt$0))) +(assert (= sk_?X_1$0 sk_?X_2$0)) +(assert + (= FP_Caller_final_Node_2$0 + (grass_union$0 FP_Caller_Node_1$0 FP_Node$0))) +(assert (= FP_Node$0 sk_?X_3$0)) +(assert (= FP_Node$0 (grass_union$0 sk_?X$0 sk_?X_2$0))) +(assert (= FP_Caller_Node_1$0 (grass_setminus$0 FP_Caller_Node$0 FP_Node$0))) +(assert (= sk_?X$0 (set_compr$0 next$0 lst$0 lst$0))) +(assert (= sk_?X$0 (set_compr$0 next$0 lst$0 grass_null$0))) +(check-sat) |