From b78f4be5dac08916e0b189ba99f608a44fa08d5d Mon Sep 17 00:00:00 2001 From: ajreynol Date: Tue, 10 May 2016 15:10:10 -0500 Subject: Fix for --inst-max-level --- test/regress/regress0/quantifiers/Makefile.am | 3 +- .../regress0/quantifiers/inst-max-level-segf.smt2 | 326 +++++++++++++++++++++ 2 files changed, 328 insertions(+), 1 deletion(-) create mode 100644 test/regress/regress0/quantifiers/inst-max-level-segf.smt2 (limited to 'test') diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index 6c89c8336..14e7da5da 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -80,7 +80,8 @@ TESTS = \ double-pattern.smt2 \ qcf-rel-dom-opt.smt2 \ parametric-lists.smt2 \ - partial-trigger.smt2 + partial-trigger.smt2 \ + inst-max-level-segf.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine diff --git a/test/regress/regress0/quantifiers/inst-max-level-segf.smt2 b/test/regress/regress0/quantifiers/inst-max-level-segf.smt2 new file mode 100644 index 000000000..d85f3d094 --- /dev/null +++ b/test/regress/regress0/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) -- cgit v1.2.3