From 2792c50ced51d681a5206ac00421ca18cb5e487e Mon Sep 17 00:00:00 2001 From: Lucas Pena Date: Tue, 5 May 2020 14:34:09 -0500 Subject: [PATCH] testlists: skl3-vc10 goes through --- prover/lib/testlists.py | 32 ++++++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) diff --git a/prover/lib/testlists.py b/prover/lib/testlists.py index abe401a3b..dc72339b6 100644 --- a/prover/lib/testlists.py +++ b/prover/lib/testlists.py @@ -211,6 +211,37 @@ def read_list(file): ) . """.replace('\n', ' ') +skl3_vc10_strategy = """ + normalize . or-split-rhs . lift-constraints + . instantiate-existentials . substitute-equals-for-equals + . kt + . normalize . or-split-rhs . lift-constraints + . instantiate-existentials . substitute-equals-for-equals + . ( ( right-unfold-Nth(0, 1) + . right-unfold-Nth(0, 1) . right-unfold-Nth(0, 1) . right-unfold-Nth(0, 0) + . right-unfold-Nth(0, 1) + . right-unfold-Nth(0, 1) . right-unfold-Nth(0, 0) + . right-unfold-Nth(0, 0) + . right-unfold-Nth(0, 0) + . normalize . or-split-rhs . lift-constraints + . instantiate-existentials . substitute-equals-for-equals + . instantiate-separation-logic-axioms + . normalize . or-split-rhs . lift-constraints + . instantiate-existentials . substitute-equals-for-equals + . match . spatial-patterns-equal . spatial-patterns-match . smt-cvc4 + ) + | ( match . spatial-patterns-equal . spatial-patterns-match . smt-cvc4 ) + | ( right-unfold-Nth(0, 1) + . normalize . or-split-rhs . lift-constraints + . instantiate-existentials . substitute-equals-for-equals + . instantiate-separation-logic-axioms + . normalize . or-split-rhs . lift-constraints + . instantiate-existentials . substitute-equals-for-equals + . match . spatial-patterns-equal . spatial-patterns-match . smt-cvc4 + ) + ) . +""".replace('\n', ' ') + # prefix KT RU timeout tests test_lists = [ ('unfold-mut-recs . ', 3, 3, '5m', read_list('t/test-lists/passing-3-3-5')) , ('unfold-mut-recs . ', 5, 12, '40m', read_list('t/test-lists/passing-5-12-40')) @@ -329,6 +360,7 @@ def read_list(file): , (nll_vc08_10_strategy, 2, 2, '10m', ['t/SL-COMP18/bench/qf_shid_entl/nll-vc10.smt2']) , ('', 3, 2, '10m', ['t/SL-COMP18/bench/qf_shid_entl/tseg_join_tree_entail_tseg.sb.smt2']) , (lsegex4_slk_1_strategy, 2, 2, '10m', ['t/SL-COMP18/bench/qf_shid_entl/lsegex4_slk-1.smt2']) + , (skl3_vc10_strategy, 2, 2, '10m', ['t/SL-COMP18/bench/qf_shid_entl/skl3-vc10.smt2']) ] qf_shid_entl_unsat_tests = read_list('t/test-lists/qf_shid_entl.unsat')