diff --git a/examples/WP_revisited/wp2/why3session.xml b/examples/WP_revisited/wp2/why3session.xml index 1ba226ad97fff41728c03bae6c18f328598ff701..f987a74923a0e50571acf9a949be54d3c6ce9184 100644 --- a/examples/WP_revisited/wp2/why3session.xml +++ b/examples/WP_revisited/wp2/why3session.xml @@ -9,9 +9,6 @@ <prover id="10" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/> <file name="../wp2.mlw" proved="true"> <theory name="Imp" proved="true"> - <goal name="VC subst_term" expl="VC for subst_term" proved="true"> - <proof prover="2"><result status="valid" time="0.01" steps="1"/></proof> - </goal> <goal name="eval_subst_term" proved="true"> <transf name="induction_ty_lex" proved="true" > <goal name="eval_subst_term.0" proved="true"> @@ -26,9 +23,6 @@ </goal> </transf> </goal> - <goal name="VC subst" expl="VC for subst" proved="true"> - <proof prover="2"><result status="valid" time="0.01" steps="1"/></proof> - </goal> <goal name="eval_subst" proved="true"> <transf name="induction_ty_lex" proved="true" > <goal name="eval_subst.0" proved="true"> diff --git a/examples/WP_revisited/wp2/why3shapes.gz b/examples/WP_revisited/wp2/why3shapes.gz index f2e405810475f5a5be62050c3946007de79b5f74..238b4512b103cc4993fe20f0e93d9ebadcf05a2b 100644 Binary files a/examples/WP_revisited/wp2/why3shapes.gz and b/examples/WP_revisited/wp2/why3shapes.gz differ diff --git a/examples/avl/avl/why3session.xml b/examples/avl/avl/why3session.xml index 3369bb5197cdecb9e62ac3558f8b476c8b0327f3..423251f65e7feb8e5c76d664117611cb83aee397 100644 --- a/examples/avl/avl/why3session.xml +++ b/examples/avl/avl/why3session.xml @@ -4,20 +4,6 @@ <why3session shape_version="4"> <prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/> <file name="../avl.mlw" proved="true"> -<theory name="SelectionTypes" proved="true"> - <goal name="VC option_to_seq" expl="VC for option_to_seq" proved="true"> - <proof prover="1"><result status="valid" time="0.00" steps="1"/></proof> - </goal> - <goal name="VC rebuild" expl="VC for rebuild" proved="true"> - <proof prover="1"><result status="valid" time="0.01" steps="1"/></proof> - </goal> - <goal name="VC left_extend" expl="VC for left_extend" proved="true"> - <proof prover="1"><result status="valid" time="0.01" steps="1"/></proof> - </goal> - <goal name="VC right_extend" expl="VC for right_extend" proved="true"> - <proof prover="1"><result status="valid" time="0.00" steps="1"/></proof> - </goal> -</theory> <theory name="AVL" proved="true"> <goal name="M.M.assoc" proved="true"> <proof prover="1"><result status="valid" time="0.00" steps="4"/></proof> @@ -25,18 +11,6 @@ <goal name="M.M.neutral" proved="true"> <proof prover="1"><result status="valid" time="0.00" steps="5"/></proof> </goal> - <goal name="VC balancing" expl="VC for balancing" proved="true"> - <proof prover="1"><result status="valid" time="0.01" steps="3"/></proof> - </goal> - <goal name="VC node_model" expl="VC for node_model" proved="true"> - <proof prover="1"><result status="valid" time="0.01" steps="4"/></proof> - </goal> - <goal name="VC seq_model" expl="VC for seq_model" proved="true"> - <proof prover="1"><result status="valid" time="0.01" steps="4"/></proof> - </goal> - <goal name="VC real_height" expl="VC for real_height" proved="true"> - <proof prover="1"><result status="valid" time="0.00" steps="4"/></proof> - </goal> <goal name="VC real_height_nonnegative" expl="VC for real_height_nonnegative" proved="true"> <proof prover="1"><result status="valid" time="0.01" steps="56"/></proof> </goal> @@ -226,9 +200,6 @@ <goal name="VC concat" expl="VC for concat" proved="true"> <proof prover="1"><result status="valid" time="0.24" steps="765"/></proof> </goal> - <goal name="VC default_split" expl="VC for default_split" proved="true"> - <proof prover="1"><result status="valid" time="0.01" steps="4"/></proof> - </goal> <goal name="VC insert" expl="VC for insert" proved="true"> <transf name="split_goal_right" proved="true" > <goal name="VC insert.0" expl="postcondition" proved="true"> diff --git a/examples/avl/avl/why3shapes.gz b/examples/avl/avl/why3shapes.gz index 555e7c99c9a1e12ae0b3432eeecc3fa53f30611f..4ad4f7bb5c2828fbe9b1f204ee95255eebde0e27 100644 Binary files a/examples/avl/avl/why3shapes.gz and b/examples/avl/avl/why3shapes.gz differ diff --git a/examples/avl/priority_queue/why3session.xml b/examples/avl/priority_queue/why3session.xml index 92dc8ee60527b6c8872c447b0d0d9565b961b5b3..d4722c200c4aee33e41a60acbc5cef5dae6280bc 100644 --- a/examples/avl/priority_queue/why3session.xml +++ b/examples/avl/priority_queue/why3session.xml @@ -7,9 +7,6 @@ <prover id="4" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/> <file name="../priority_queue.mlw" proved="true"> <theory name="PQueue" proved="true"> - <goal name="VC balancing" expl="VC for balancing" proved="true"> - <proof prover="4"><result status="valid" time="0.00" steps="3"/></proof> - </goal> <goal name="M.VC assoc_m" expl="VC for assoc_m" proved="true"> <transf name="split_goal_right" proved="true" > <goal name="VC assoc_m.0" expl="assertion" proved="true"> @@ -94,9 +91,6 @@ </goal> </transf> </goal> - <goal name="D.VC measure" expl="VC for measure" proved="true"> - <proof prover="4"><result status="valid" time="0.01" steps="4"/></proof> - </goal> <goal name="VC monoid_sum_is_min" expl="VC for monoid_sum_is_min" proved="true"> <transf name="split_goal_right" proved="true" > <goal name="VC monoid_sum_is_min.0" expl="precondition" proved="true"> @@ -364,9 +358,6 @@ <goal name="Sel.M.agg_cat" proved="true"> <proof prover="4"><result status="valid" time="0.02" steps="5"/></proof> </goal> - <goal name="Sel.D.VC measure" expl="VC for measure" proved="true"> - <proof prover="4"><result status="valid" time="0.02" steps="4"/></proof> - </goal> <goal name="Sel.VC balancing" expl="VC for balancing" proved="true"> <proof prover="4"><result status="valid" time="0.01" steps="4"/></proof> </goal> @@ -376,9 +367,6 @@ <goal name="Sel.VC selected_part" expl="VC for selected_part" proved="true"> <proof prover="4"><result status="valid" time="0.04" steps="257"/></proof> </goal> - <goal name="VC to_bag" expl="VC for to_bag" proved="true"> - <proof prover="4"><result status="valid" time="0.01" steps="4"/></proof> - </goal> <goal name="VC to_bag_mem" expl="VC for to_bag_mem" proved="true"> <transf name="split_goal_right" proved="true" > <goal name="VC to_bag_mem.0" expl="assertion" proved="true"> diff --git a/examples/avl/priority_queue/why3shapes.gz b/examples/avl/priority_queue/why3shapes.gz index 8563cdad2a2ad3c8c632d4ba1674a2a1d050ac24..03b493d71ab6b3c4d464c93b12077ec01abfb08b 100644 Binary files a/examples/avl/priority_queue/why3shapes.gz and b/examples/avl/priority_queue/why3shapes.gz differ diff --git a/examples/avl/ral/why3session.xml b/examples/avl/ral/why3session.xml index 8e38b36be261d5f1f651cf069aaefd4e2b01a820..fcd8bc6a818064cdd8c047dcae5423d51add4663 100644 --- a/examples/avl/ral/why3session.xml +++ b/examples/avl/ral/why3session.xml @@ -5,9 +5,6 @@ <prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/> <file name="../ral.mlw" proved="true"> <theory name="RAL" proved="true"> - <goal name="VC balancing" expl="VC for balancing" proved="true"> - <proof prover="1"><result status="valid" time="0.01" steps="3"/></proof> - </goal> <goal name="M.assoc" proved="true"> <proof prover="1"><result status="valid" time="0.01" steps="4"/></proof> </goal> @@ -26,9 +23,6 @@ <goal name="M.VC op" expl="VC for op" proved="true"> <proof prover="1"><result status="valid" time="0.01" steps="4"/></proof> </goal> - <goal name="D.VC measure" expl="VC for measure" proved="true"> - <proof prover="1"><result status="valid" time="0.01" steps="4"/></proof> - </goal> <goal name="VC agg_measure_is_length" expl="VC for agg_measure_is_length" proved="true"> <proof prover="1"><result status="valid" time="0.01" steps="50"/></proof> </goal> @@ -56,9 +50,6 @@ <goal name="Sel.M.agg_cat" proved="true"> <proof prover="1"><result status="valid" time="0.01" steps="5"/></proof> </goal> - <goal name="Sel.D.VC measure" expl="VC for measure" proved="true"> - <proof prover="1"><result status="valid" time="0.01" steps="4"/></proof> - </goal> <goal name="Sel.VC balancing" expl="VC for balancing" proved="true"> <proof prover="1"><result status="valid" time="0.01" steps="4"/></proof> </goal> diff --git a/examples/avl/ral/why3shapes.gz b/examples/avl/ral/why3shapes.gz index f6814056bbc9e360170c197592f0271c30148b85..1a9e26ed1f2e98971c36a7ee4436c1a76be7b2ec 100644 Binary files a/examples/avl/ral/why3shapes.gz and b/examples/avl/ral/why3shapes.gz differ diff --git a/examples/avl/tables/why3session.xml b/examples/avl/tables/why3session.xml index 1a34b98735d31bd592b2fe7ec697309c809a2c97..a4113da33a5fb7192d4ec642eadd189ce2eca6e9 100644 --- a/examples/avl/tables/why3session.xml +++ b/examples/avl/tables/why3session.xml @@ -6,12 +6,6 @@ <prover id="5" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/> <file name="../tables.mlw" proved="true"> <theory name="MapBase" proved="true"> - <goal name="VC balancing" expl="VC for balancing" proved="true"> - <proof prover="5"><result status="valid" time="0.01" steps="3"/></proof> - </goal> - <goal name="D.VC measure" expl="VC for measure" proved="true"> - <proof prover="5"><result status="valid" time="0.01" steps="4"/></proof> - </goal> <goal name="M.VC neutral_" expl="VC for neutral_" proved="true"> <proof prover="5"><result status="valid" time="0.01" steps="4"/></proof> </goal> @@ -93,9 +87,6 @@ <goal name="Sel.M.agg_cat" proved="true"> <proof prover="5"><result status="valid" time="0.01" steps="4"/></proof> </goal> - <goal name="Sel.D.VC measure" expl="VC for measure" proved="true"> - <proof prover="5"><result status="valid" time="0.01" steps="4"/></proof> - </goal> <goal name="Sel.VC balancing" expl="VC for balancing" proved="true"> <proof prover="5"><result status="valid" time="0.01" steps="4"/></proof> </goal> @@ -821,18 +812,9 @@ </goal> </theory> <theory name="Map" proved="true"> - <goal name="VC balancing" expl="VC for balancing" proved="true"> - <proof prover="5"><result status="valid" time="0.00" steps="3"/></proof> - </goal> - <goal name="D.VC key" expl="VC for key" proved="true"> - <proof prover="5"><result status="valid" time="0.01" steps="4"/></proof> - </goal> <goal name="MB.VC balancing" expl="VC for balancing" proved="true"> <proof prover="5"><result status="valid" time="0.01" steps="4"/></proof> </goal> - <goal name="MB.VC key" expl="VC for key" proved="true"> - <proof prover="5"><result status="valid" time="0.01" steps="4"/></proof> - </goal> <goal name="MB.CO.Refl" proved="true"> <proof prover="5"><result status="valid" time="0.01" steps="5"/></proof> </goal> @@ -905,18 +887,9 @@ </goal> </theory> <theory name="Set" proved="true"> - <goal name="VC balancing" expl="VC for balancing" proved="true"> - <proof prover="5"><result status="valid" time="0.01" steps="3"/></proof> - </goal> - <goal name="D.VC key" expl="VC for key" proved="true"> - <proof prover="5"><result status="valid" time="0.01" steps="4"/></proof> - </goal> <goal name="MB.VC balancing" expl="VC for balancing" proved="true"> <proof prover="5"><result status="valid" time="0.00" steps="4"/></proof> </goal> - <goal name="MB.VC key" expl="VC for key" proved="true"> - <proof prover="5"><result status="valid" time="0.01" steps="4"/></proof> - </goal> <goal name="MB.CO.Refl" proved="true"> <proof prover="5"><result status="valid" time="0.01" steps="5"/></proof> </goal> @@ -994,9 +967,6 @@ </goal> </theory> <theory name="IMapAndSet" proved="true"> - <goal name="VC balancing" expl="VC for balancing" proved="true"> - <proof prover="5"><result status="valid" time="0.00" steps="3"/></proof> - </goal> <goal name="VC compare" expl="VC for compare" proved="true"> <proof prover="5"><result status="valid" time="0.01" steps="4"/></proof> </goal> diff --git a/examples/avl/tables/why3shapes.gz b/examples/avl/tables/why3shapes.gz index c3694b2a24525165540e6b20f052cb2b552f63da..566195b04746fc6f9681e710c085675e55363e94 100644 Binary files a/examples/avl/tables/why3shapes.gz and b/examples/avl/tables/why3shapes.gz differ diff --git a/examples/bag/why3session.xml b/examples/bag/why3session.xml index 0cebeb6f1a3073635df13ba3d64837153c4b7fba..fd55ec4e583aceef31d7cd43b0052b4f6f5fd423 100644 --- a/examples/bag/why3session.xml +++ b/examples/bag/why3session.xml @@ -6,17 +6,6 @@ <prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="2" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/> <file name="../bag.mlw" proved="true"> -<theory name="Bag" proved="true"> - <goal name="VC empty" expl="VC for empty" proved="true"> - <proof prover="1"><result status="valid" time="0.00" steps="1"/></proof> - </goal> - <goal name="VC add" expl="VC for add" proved="true"> - <proof prover="1"><result status="valid" time="0.00" steps="1"/></proof> - </goal> - <goal name="VC remove" expl="VC for remove" proved="true"> - <proof prover="1"><result status="valid" time="0.00" steps="1"/></proof> - </goal> -</theory> <theory name="BagSpec" proved="true"> <goal name="VC t" expl="VC for t" proved="true"> <proof prover="1"><result status="valid" time="0.00" steps="1"/></proof> diff --git a/examples/bag/why3shapes.gz b/examples/bag/why3shapes.gz index 83219eec6c6a0733fe32d185927e21836c948d3e..3538642d2c4d9be204d228a70538bdf0f779d029 100644 Binary files a/examples/bag/why3shapes.gz and b/examples/bag/why3shapes.gz differ diff --git a/examples/bellman_ford/why3session.xml b/examples/bellman_ford/why3session.xml index 6dd59b9a2c83264b774dd327581959417b13c7ef..0de5cb2530a11080e960f33f9e159a76b30ac520 100644 --- a/examples/bellman_ford/why3session.xml +++ b/examples/bellman_ford/why3session.xml @@ -6,15 +6,9 @@ <prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/> <file name="../bellman_ford.mlw" proved="true"> <theory name="Graph" proved="true"> - <goal name="VC s" expl="VC for s" proved="true"> - <proof prover="1"><result status="valid" time="0.00" steps="1"/></proof> - </goal> <goal name="vertices_cardinal_pos" proved="true"> <proof prover="1"><result status="valid" time="0.00" steps="5"/></proof> </goal> - <goal name="VC nb_vertices" expl="VC for nb_vertices" proved="true"> - <proof prover="1"><result status="valid" time="0.00" steps="3"/></proof> - </goal> <goal name="path_in_vertices" proved="true"> <proof prover="1"><result status="valid" time="0.01" steps="30"/></proof> </goal> diff --git a/examples/bellman_ford/why3shapes.gz b/examples/bellman_ford/why3shapes.gz index fcb033b40d75aa22b831dae59964da01eae65565..785f5cd7c11796b23626f9e9d63002b751ca5fac 100644 Binary files a/examples/bellman_ford/why3shapes.gz and b/examples/bellman_ford/why3shapes.gz differ diff --git a/examples/bignum/why3session.xml b/examples/bignum/why3session.xml index 0ab43f2aa22433325e0f4d20468dd05ce98cf5b3..d8adc20b522812fce4cddd15f963c4ef606f14f7 100644 --- a/examples/bignum/why3session.xml +++ b/examples/bignum/why3session.xml @@ -8,9 +8,6 @@ <prover id="4" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/> <file name="../bignum.mlw" proved="true"> <theory name="BigNum" proved="true"> - <goal name="VC base" expl="VC for base" proved="true"> - <proof prover="4"><result status="valid" time="0.00" steps="1"/></proof> - </goal> <goal name="VC nonneg" expl="VC for nonneg" proved="true"> <transf name="split_goal_right" proved="true" > <goal name="VC nonneg.0" expl="variant decrease" proved="true"> diff --git a/examples/bignum/why3shapes.gz b/examples/bignum/why3shapes.gz index 1a3d9522393a049bce8a7e943dce4016aa844323..5c3e7e855e9d22a952fb0ce39eaca9e76589441a 100644 Binary files a/examples/bignum/why3shapes.gz and b/examples/bignum/why3shapes.gz differ diff --git a/examples/binomial_heap/why3session.xml b/examples/binomial_heap/why3session.xml index bca383d3e15f99ec8f9936b1422abb7c8877285d..a52440e5aea11bd7690fe60ac588afc1ba12e408 100644 --- a/examples/binomial_heap/why3session.xml +++ b/examples/binomial_heap/why3session.xml @@ -142,9 +142,6 @@ </goal> </transf> </goal> - <goal name="VC link" expl="VC for link" proved="true"> - <proof prover="1"><result status="valid" time="0.00" steps="4"/></proof> - </goal> <goal name="VC add_tree" expl="VC for add_tree" proved="true"> <transf name="split_goal_right" proved="true" > <goal name="VC add_tree.0" expl="assertion" proved="true"> diff --git a/examples/binomial_heap/why3shapes.gz b/examples/binomial_heap/why3shapes.gz index 949348155f67d403d15b2f81083103fccf2bf993..c1adf123bf2c5cfc8e3a7c5c9f3d5bb3a615622a 100644 Binary files a/examples/binomial_heap/why3shapes.gz and b/examples/binomial_heap/why3shapes.gz differ diff --git a/examples/bitwalker/why3session.xml b/examples/bitwalker/why3session.xml index e18fb42b33df8df8fd6dee257e1d901a6df47d97..4a549cdbb53e0c73f65999bf2306af3925d59a4d 100644 --- a/examples/bitwalker/why3session.xml +++ b/examples/bitwalker/why3session.xml @@ -13,10 +13,6 @@ <goal name="nth8" proved="true"> <proof prover="0"><result status="valid" time="0.06" steps="208"/></proof> </goal> - <goal name="VC maxvalue" expl="VC for maxvalue" proved="true"> - <transf name="compute_in_goal" proved="true" > - </transf> - </goal> <goal name="VC nth_ultpre0" expl="VC for nth_ultpre0" proved="true"> <transf name="split_goal_right" proved="true" > <goal name="VC nth_ultpre0.0" expl="assertion" proved="true"> diff --git a/examples/bitwalker/why3shapes.gz b/examples/bitwalker/why3shapes.gz index 5d34f6f8f97d7af7c6550b2c3cdd8779c1692127..3ce0cd2ae6cd721bb89432677f10188d044493cb 100644 Binary files a/examples/bitwalker/why3shapes.gz and b/examples/bitwalker/why3shapes.gz differ diff --git a/examples/braun_trees/why3session.xml b/examples/braun_trees/why3session.xml index fb49406c5b6fc1457b5736dc1cd9b55c13a3f5c2..f2f27a91bdffe32633464fccb3d5c361423e2a59 100644 --- a/examples/braun_trees/why3session.xml +++ b/examples/braun_trees/why3session.xml @@ -6,9 +6,6 @@ <prover id="3" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/> <file name="../braun_trees.mlw" proved="true"> <theory name="BraunHeaps" proved="true"> - <goal name="VC le_root" expl="VC for le_root" proved="true"> - <proof prover="2"><result status="valid" time="0.00" steps="1"/></proof> - </goal> <goal name="VC root_is_min" expl="VC for root_is_min" proved="true"> <proof prover="2"><result status="valid" time="0.70" steps="1275"/></proof> </goal> diff --git a/examples/braun_trees/why3shapes.gz b/examples/braun_trees/why3shapes.gz index 3d01b14ab74f7f82a00262e59d5540d90d88f285..a8bb83c2302191657dfed988d8846f3a421a31ae 100644 Binary files a/examples/braun_trees/why3shapes.gz and b/examples/braun_trees/why3shapes.gz differ diff --git a/examples/bts/13375/why3session.xml b/examples/bts/13375/why3session.xml index b1c874d6afd8bbaab6e42de6df59cf4de62a5501..36c0246a3925e6027c0d7c37c0a1b5cb608f9353 100644 --- a/examples/bts/13375/why3session.xml +++ b/examples/bts/13375/why3session.xml @@ -2,12 +2,6 @@ <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN" "http://why3.lri.fr/why3session.dtd"> <why3session shape_version="4"> -<prover id="0" name="Alt-Ergo" version="2.2.0" timelimit="5" steplimit="0" memlimit="1000"/> <file name="../13375.mlw" proved="true"> -<theory name="Spec" proved="true"> - <goal name="VC to_int_" expl="VC for to_int_" proved="true"> - <proof prover="0"><result status="valid" time="0.00" steps="4"/></proof> - </goal> -</theory> </file> </why3session> diff --git a/examples/bts/13375/why3shapes.gz b/examples/bts/13375/why3shapes.gz index 08ebd9a710741f6c55c397dd6a464a216370f4ea..0239669d57f6148035ad2dc4a6d54ae7db678e85 100644 Binary files a/examples/bts/13375/why3shapes.gz and b/examples/bts/13375/why3shapes.gz differ diff --git a/examples/bts/13853/why3session.xml b/examples/bts/13853/why3session.xml index 2e296ed16482eb473cd65547dbafd08be9f02ea4..6b6f85ec8661d6033752ade32ccadc9481c6c0f9 100644 --- a/examples/bts/13853/why3session.xml +++ b/examples/bts/13853/why3session.xml @@ -5,9 +5,6 @@ <prover id="0" name="Alt-Ergo" version="2.2.0" timelimit="5" steplimit="0" memlimit="1000"/> <file name="../13853.mlw" proved="true"> <theory name="T" proved="true"> - <goal name="VC f" expl="VC for f" proved="true"> - <proof prover="0"><result status="valid" time="0.00" steps="0"/></proof> - </goal> <goal name="VC g" expl="VC for g" proved="true"> <proof prover="0"><result status="valid" time="0.00" steps="0"/></proof> </goal> diff --git a/examples/bts/13853/why3shapes.gz b/examples/bts/13853/why3shapes.gz index ea349f75eff7e6f25850f26d560638e5effbf71a..b2bd6c243fceed3dbc2bf124a6918c94bc0aab7d 100644 Binary files a/examples/bts/13853/why3shapes.gz and b/examples/bts/13853/why3shapes.gz differ diff --git a/examples/counting_sort/why3session.xml b/examples/counting_sort/why3session.xml index 0ee1eb952e3a9456fc4f6debba5c32ef3810f016..1299829ea3bd2fa6bd94d4b1788ff85a9e20b8fb 100644 --- a/examples/counting_sort/why3session.xml +++ b/examples/counting_sort/why3session.xml @@ -6,9 +6,6 @@ <prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/> <file name="../counting_sort.mlw" proved="true"> <theory name="Spec" proved="true"> - <goal name="VC k" expl="VC for k" proved="true"> - <proof prover="1"><result status="valid" time="0.00" steps="1"/></proof> - </goal> <goal name="VC eqlt" expl="VC for eqlt" proved="true"> <proof prover="1"><result status="valid" time="0.76" steps="777"/></proof> </goal> diff --git a/examples/counting_sort/why3shapes.gz b/examples/counting_sort/why3shapes.gz index 20cfe834fd114056c404677d9691fa0846d3bb12..3be22db9561f777ed68a86bde1001429130b13b5 100644 Binary files a/examples/counting_sort/why3shapes.gz and b/examples/counting_sort/why3shapes.gz differ diff --git a/examples/defunctionalization/why3session.xml b/examples/defunctionalization/why3session.xml index 49295bdba4061b59926fd8f9ce25e5f83c507bb9..8624d8a4547a715e3fd505bbe460469dfd97a8e9 100644 --- a/examples/defunctionalization/why3session.xml +++ b/examples/defunctionalization/why3session.xml @@ -9,33 +9,7 @@ <prover id="10" name="CVC4" version="1.5" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="11" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/> <file name="../defunctionalization.mlw" proved="true"> -<theory name="Expr" proved="true"> - <goal name="VC p0" expl="VC for p0" proved="true"> - <proof prover="11"><result status="valid" time="0.00" steps="1"/></proof> - </goal> - <goal name="VC p1" expl="VC for p1" proved="true"> - <proof prover="11"><result status="valid" time="0.00" steps="1"/></proof> - </goal> - <goal name="VC p2" expl="VC for p2" proved="true"> - <proof prover="11"><result status="valid" time="0.00" steps="1"/></proof> - </goal> - <goal name="VC p3" expl="VC for p3" proved="true"> - <proof prover="11"><result status="valid" time="0.00" steps="1"/></proof> - </goal> - <goal name="VC p4" expl="VC for p4" proved="true"> - <proof prover="11"><result status="valid" time="0.00" steps="1"/></proof> - </goal> -</theory> <theory name="DirectSem" proved="true"> - <goal name="VC eval_0" expl="VC for eval_0" proved="true"> - <proof prover="11"><result status="valid" time="0.00" steps="1"/></proof> - </goal> - <goal name="VC interpret_0" expl="VC for interpret_0" proved="true"> - <proof prover="11"><result status="valid" time="0.00" steps="1"/></proof> - </goal> - <goal name="VC test" expl="VC for test" proved="true"> - <proof prover="11"><result status="valid" time="0.00" steps="1"/></proof> - </goal> <goal name="eval_p3" proved="true"> <proof prover="0"><result status="valid" time="0.01"/></proof> <proof prover="6" memlimit="4000"><result status="valid" time="0.02"/></proof> @@ -76,9 +50,6 @@ <goal name="VC interpret_2" expl="VC for interpret_2" proved="true"> <proof prover="11"><result status="valid" time="0.01" steps="18"/></proof> </goal> - <goal name="VC test" expl="VC for test" proved="true"> - <proof prover="11"><result status="valid" time="0.00" steps="3"/></proof> - </goal> </theory> <theory name="Defunctionalization2" proved="true"> <goal name="VC continue_2" expl="VC for continue_2" proved="true"> @@ -100,9 +71,6 @@ <goal name="VC interpret_2" expl="VC for interpret_2" proved="true"> <proof prover="11"><result status="valid" time="0.00" steps="15"/></proof> </goal> - <goal name="VC test" expl="VC for test" proved="true"> - <proof prover="11"><result status="valid" time="0.00" steps="3"/></proof> - </goal> </theory> <theory name="SemWithError" proved="true"> <goal name="cps_correct_expr" proved="true"> @@ -221,17 +189,11 @@ <goal name="VC interpret_4" expl="VC for interpret_4" proved="true"> <proof prover="11"><result status="valid" time="0.01" steps="40"/></proof> </goal> - <goal name="VC test" expl="VC for test" proved="true"> - <proof prover="11"><result status="valid" time="0.01" steps="6"/></proof> - </goal> </theory> <theory name="ReductionSemantics" proved="true"> <goal name="VC contract" expl="VC for contract" proved="true"> <proof prover="11"><result status="valid" time="0.01" steps="44"/></proof> </goal> - <goal name="VC recompose" expl="VC for recompose" proved="true"> - <proof prover="11"><result status="valid" time="0.00" steps="2"/></proof> - </goal> <goal name="VC recompose_values" expl="VC for recompose_values" proved="true"> <proof prover="11"><result status="valid" time="0.04" steps="294"/></proof> </goal> @@ -291,9 +253,6 @@ <goal name="VC interpret" expl="VC for interpret" proved="true"> <proof prover="11"><result status="valid" time="0.00" steps="6"/></proof> </goal> - <goal name="VC test" expl="VC for test" proved="true"> - <proof prover="11"><result status="valid" time="0.00" steps="5"/></proof> - </goal> </theory> <theory name="RWithError" proved="true"> <goal name="size_c_pos" proved="true"> @@ -318,9 +277,6 @@ <goal name="VC interpret" expl="VC for interpret" proved="true"> <proof prover="11"><result status="valid" time="0.01" steps="9"/></proof> </goal> - <goal name="VC test" expl="VC for test" proved="true"> - <proof prover="11"><result status="valid" time="0.01" steps="8"/></proof> - </goal> </theory> </file> </why3session> diff --git a/examples/defunctionalization/why3shapes.gz b/examples/defunctionalization/why3shapes.gz index e8afc15515f4164d28af2ab03eedb7b702f7477c..b4cf5c38e82c38ea880ef69ce2062d3f583f0476 100644 Binary files a/examples/defunctionalization/why3shapes.gz and b/examples/defunctionalization/why3shapes.gz differ diff --git a/examples/dfs/why3session.xml b/examples/dfs/why3session.xml index 32f50991dd4fe5ce1cc5f07cdec316b40207a551..4408c1282f34906234695aa78b87ed8aac7ec6f7 100644 --- a/examples/dfs/why3session.xml +++ b/examples/dfs/why3session.xml @@ -6,12 +6,6 @@ <prover id="2" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/> <file name="../dfs.mlw" proved="true"> <theory name="DFS" proved="true"> - <goal name="VC null" expl="VC for null" proved="true"> - <proof prover="2"><result status="valid" time="0.00" steps="1"/></proof> - </goal> - <goal name="VC root" expl="VC for root" proved="true"> - <proof prover="2"><result status="valid" time="0.00" steps="1"/></proof> - </goal> <goal name="VC set" expl="VC for set" proved="true"> <proof prover="2"><result status="valid" time="0.00" steps="4"/></proof> </goal> diff --git a/examples/dfs/why3shapes.gz b/examples/dfs/why3shapes.gz index 60c8c123082ec823abb8cb79609ea3ee17feacb7..6b744b8d457ce03628108963c1bb1732eb1f4430 100644 Binary files a/examples/dfs/why3shapes.gz and b/examples/dfs/why3shapes.gz differ diff --git a/examples/double_wp/compiler/why3session.xml b/examples/double_wp/compiler/why3session.xml index 6120841c6ca5b35ced2391e593b2da87bff6a6da..260da502ca627a709f3ab375ba6696acc6e00361 100644 --- a/examples/double_wp/compiler/why3session.xml +++ b/examples/double_wp/compiler/why3session.xml @@ -636,12 +636,6 @@ <goal name="VC compile_program" expl="VC for compile_program" proved="true"> <proof prover="1"><result status="valid" time="0.44"/></proof> </goal> - <goal name="VC test" expl="VC for test" proved="true"> - <proof prover="2"><result status="valid" time="0.03" steps="8"/></proof> - </goal> - <goal name="VC test2" expl="VC for test2" proved="true"> - <proof prover="2"><result status="valid" time="0.04" steps="8"/></proof> - </goal> </theory> </file> </why3session> diff --git a/examples/double_wp/compiler/why3shapes.gz b/examples/double_wp/compiler/why3shapes.gz index d84dc0d08d15d8e482a0452e57ee26a5397b5d65..c3f7fd6a60df9ac16fef356c2607b8683ea47441 100644 Binary files a/examples/double_wp/compiler/why3shapes.gz and b/examples/double_wp/compiler/why3shapes.gz differ diff --git a/examples/double_wp/vm/why3session.xml b/examples/double_wp/vm/why3session.xml index 5c220678d771c4e9c272d7ac7d2cb81ccebc02ce..b51f64d1bda42ae713b518e7b5be8176c79a67ce 100644 --- a/examples/double_wp/vm/why3session.xml +++ b/examples/double_wp/vm/why3session.xml @@ -35,45 +35,6 @@ <goal name="codeseq_at_app_left" proved="true"> <proof prover="2"><result status="valid" time="0.03" steps="59"/></proof> </goal> - <goal name="VC push" expl="VC for push" proved="true"> - <proof prover="2"><result status="valid" time="0.01" steps="5"/></proof> - </goal> - <goal name="VC iconst" expl="VC for iconst" proved="true"> - <proof prover="2"><result status="valid" time="0.01" steps="5"/></proof> - </goal> - <goal name="VC ivar" expl="VC for ivar" proved="true"> - <proof prover="2"><result status="valid" time="0.01" steps="5"/></proof> - </goal> - <goal name="VC isetvar" expl="VC for isetvar" proved="true"> - <proof prover="2"><result status="valid" time="0.01" steps="5"/></proof> - </goal> - <goal name="VC iadd" expl="VC for iadd" proved="true"> - <proof prover="2"><result status="valid" time="0.01" steps="5"/></proof> - </goal> - <goal name="VC isub" expl="VC for isub" proved="true"> - <proof prover="2"><result status="valid" time="0.01" steps="5"/></proof> - </goal> - <goal name="VC imul" expl="VC for imul" proved="true"> - <proof prover="2"><result status="valid" time="0.01" steps="5"/></proof> - </goal> - <goal name="VC ibeq" expl="VC for ibeq" proved="true"> - <proof prover="2"><result status="valid" time="0.01" steps="5"/></proof> - </goal> - <goal name="VC ible" expl="VC for ible" proved="true"> - <proof prover="2"><result status="valid" time="0.00" steps="5"/></proof> - </goal> - <goal name="VC ibne" expl="VC for ibne" proved="true"> - <proof prover="2"><result status="valid" time="0.01" steps="5"/></proof> - </goal> - <goal name="VC ibgt" expl="VC for ibgt" proved="true"> - <proof prover="2"><result status="valid" time="0.01" steps="5"/></proof> - </goal> - <goal name="VC ibranch" expl="VC for ibranch" proved="true"> - <proof prover="2"><result status="valid" time="0.01" steps="5"/></proof> - </goal> - <goal name="VC ihalt" expl="VC for ihalt" proved="true"> - <proof prover="2"><result status="valid" time="0.01" steps="5"/></proof> - </goal> </theory> </file> </why3session> diff --git a/examples/double_wp/vm/why3shapes.gz b/examples/double_wp/vm/why3shapes.gz index 93ea4a8aa0ee8d40e5979d98427f2634212c6132..faa09e9599298941fdfb0537656c063743663c26 100644 Binary files a/examples/double_wp/vm/why3shapes.gz and b/examples/double_wp/vm/why3shapes.gz differ diff --git a/examples/fibonacci/why3session.xml b/examples/fibonacci/why3session.xml index 16e84666d885ca467b5b0a55a7c8f8da89eb2c84..6a804c8784d8cfad7e40ade6f5d7b5b756496607 100644 --- a/examples/fibonacci/why3session.xml +++ b/examples/fibonacci/why3session.xml @@ -36,9 +36,6 @@ <goal name="VC test42" expl="VC for test42" proved="true"> <proof prover="3"><result status="valid" time="0.00" steps="3"/></proof> </goal> - <goal name="VC bench" expl="VC for bench" proved="true"> - <proof prover="3"><result status="valid" time="0.00" steps="3"/></proof> - </goal> </theory> <theory name="FibRecNoGhost" proved="true"> <goal name="VC fib_aux" expl="VC for fib_aux" proved="true"> @@ -164,9 +161,6 @@ </goal> </theory> <theory name="FibonacciLogarithmic" proved="true"> - <goal name="VC m1110" expl="VC for m1110" proved="true"> - <proof prover="3"><result status="valid" time="0.00" steps="3"/></proof> - </goal> <goal name="VC logfib" expl="VC for logfib" proved="true"> <transf name="split_goal_right" proved="true" > <goal name="VC logfib.0" expl="assertion" proved="true"> @@ -216,9 +210,6 @@ <goal name="VC test2014" expl="VC for test2014" proved="true"> <proof prover="3"><result status="valid" time="0.00" steps="3"/></proof> </goal> - <goal name="VC bench" expl="VC for bench" proved="true"> - <proof prover="3"><result status="valid" time="0.00" steps="3"/></proof> - </goal> </theory> </file> </why3session> diff --git a/examples/fibonacci/why3shapes.gz b/examples/fibonacci/why3shapes.gz index 3bcedae3a72d24e2705002af520503dda36c8c84..561676f940f0e8e8e72c41fd335f8e850e1feebc 100644 Binary files a/examples/fibonacci/why3shapes.gz and b/examples/fibonacci/why3shapes.gz differ diff --git a/examples/find/why3session.xml b/examples/find/why3session.xml index 42376eb4f9991949501a1ded9b79fb3e66287145..49b3c8861a699d914131d8352bcf4dbfadb43a43 100644 --- a/examples/find/why3session.xml +++ b/examples/find/why3session.xml @@ -5,12 +5,6 @@ <prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/> <file name="../find.mlw" proved="true"> <theory name="FIND" proved="true"> - <goal name="VC _N" expl="VC for _N" proved="true"> - <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof> - </goal> - <goal name="VC f" expl="VC for f" proved="true"> - <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof> - </goal> <goal name="VC find" expl="VC for find" proved="true"> <transf name="split_goal_right" proved="true" > <goal name="VC find.0" expl="loop invariant init" proved="true"> diff --git a/examples/find/why3shapes.gz b/examples/find/why3shapes.gz index edc43f3d18afdceff7aa7a534ed9f9be3416938e..8aaf5492f4d577b13e4bd3a1699d20f0779d19b0 100644 Binary files a/examples/find/why3shapes.gz and b/examples/find/why3shapes.gz differ diff --git a/examples/foveoos11-cm/duplets/why3session.xml b/examples/foveoos11-cm/duplets/why3session.xml index d1ec95346c6d89879c149d691767c53f1bb1b288..c4c63eb0fe0761c6bb9f794b75d4b4cc5cbea8e2 100644 --- a/examples/foveoos11-cm/duplets/why3session.xml +++ b/examples/foveoos11-cm/duplets/why3session.xml @@ -5,10 +5,6 @@ <prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/> <file name="../duplets.mlw" proved="true"> <theory name="Duplets" proved="true"> - <goal name="VC eq_opt" expl="VC for eq_opt" proved="true"> - <transf name="split_goal_right" proved="true" > - </transf> - </goal> <goal name="VC duplet" expl="VC for duplet" proved="true"> <transf name="split_goal_right" proved="true" > <goal name="VC duplet.0" expl="loop invariant init" proved="true"> diff --git a/examples/foveoos11-cm/duplets/why3shapes.gz b/examples/foveoos11-cm/duplets/why3shapes.gz index 6423aa7ddb2e3da2617982e6508d2261f2451d4c..5efe8a524916c33f80b339a7b5883468bf98f4e6 100644 Binary files a/examples/foveoos11-cm/duplets/why3shapes.gz and b/examples/foveoos11-cm/duplets/why3shapes.gz differ diff --git a/examples/hackers-delight/why3session.xml b/examples/hackers-delight/why3session.xml index 69756955b4de7da4bf4dd683b02501ebfeec477f..0d2985912545f3c2ff859a485557a090014b179d 100644 --- a/examples/hackers-delight/why3session.xml +++ b/examples/hackers-delight/why3session.xml @@ -7,20 +7,6 @@ <prover id="8" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/> <prover id="9" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/> <file name="../hackers-delight.mlw" proved="true"> -<theory name="Utils" proved="true"> - <goal name="VC one" expl="VC for one" proved="true"> - <proof prover="9"><result status="valid" time="0.01"/></proof> - </goal> - <goal name="VC two" expl="VC for two" proved="true"> - <proof prover="9"><result status="valid" time="0.01"/></proof> - </goal> - <goal name="VC lastbit" expl="VC for lastbit" proved="true"> - <proof prover="9"><result status="valid" time="0.01"/></proof> - </goal> - <goal name="VC count" expl="VC for count" proved="true"> - <proof prover="9"><result status="valid" time="0.00"/></proof> - </goal> -</theory> <theory name="Utils_Spec" proved="true"> <goal name="countZero" proved="true"> <proof prover="9"><result status="valid" time="0.01"/></proof> diff --git a/examples/hackers-delight/why3shapes.gz b/examples/hackers-delight/why3shapes.gz index d14f6d4931efa80d3e2261714cda4c93b4d00fa8..0a30ebc3edf606cce8fb5926359b616ecd74c7a7 100644 Binary files a/examples/hackers-delight/why3shapes.gz and b/examples/hackers-delight/why3shapes.gz differ diff --git a/examples/hillel_challenge/why3session.xml b/examples/hillel_challenge/why3session.xml index 6b6ad97eabd6518fdccda4325349039297ac5332..bae514426cbd0738326cb96a46e4cc052150a548 100644 --- a/examples/hillel_challenge/why3session.xml +++ b/examples/hillel_challenge/why3session.xml @@ -207,12 +207,6 @@ <goal name="VC big_zero" expl="VC for big_zero" proved="true"> <proof prover="0"><result status="valid" time="0.03"/></proof> </goal> - <goal name="VC min_int32" expl="VC for min_int32" proved="true"> - <proof prover="0"><result status="valid" time="0.02"/></proof> - </goal> - <goal name="VC max_int32" expl="VC for max_int32" proved="true"> - <proof prover="0"><result status="valid" time="0.02"/></proof> - </goal> <goal name="VC add_big" expl="VC for add_big" proved="true"> <transf name="split_vc" proved="true" > <goal name="VC add_big.0" expl="integer overflow" proved="true"> diff --git a/examples/hillel_challenge/why3shapes.gz b/examples/hillel_challenge/why3shapes.gz index f55c758351b25ed602f3c664d1a053393b4130b5..a1cdaf1012cb3d48aba753b518e2f8bbc9fee542 100644 Binary files a/examples/hillel_challenge/why3shapes.gz and b/examples/hillel_challenge/why3shapes.gz differ diff --git a/examples/inverse_in_place/why3session.xml b/examples/inverse_in_place/why3session.xml index f09d02ccf0047cbaa1b41cecc09fab904c71e406..18fc49368e746a2b868274fffb2b1c2fe99d0309 100644 --- a/examples/inverse_in_place/why3session.xml +++ b/examples/inverse_in_place/why3session.xml @@ -7,9 +7,6 @@ <prover id="2" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/> <file name="../inverse_in_place.mlw" proved="true"> <theory name="InverseInPlace" proved="true"> - <goal name="VC prefix ~" expl="VC for prefix ~" proved="true"> - <proof prover="2"><result status="valid" time="0.00" steps="1"/></proof> - </goal> <goal name="is_permutation_inverse" proved="true"> <proof prover="2"><result status="valid" time="0.00" steps="28"/></proof> </goal> diff --git a/examples/inverse_in_place/why3shapes.gz b/examples/inverse_in_place/why3shapes.gz index ff8c26961c594527830d4abfc40360f364861e8e..312e38aed87f713774273ea6682498cd6171a763 100644 Binary files a/examples/inverse_in_place/why3shapes.gz and b/examples/inverse_in_place/why3shapes.gz differ diff --git a/examples/leftist_heap/why3session.xml b/examples/leftist_heap/why3session.xml index ebb40512a5b42a8b8588e5dafbd7db909cd7ee63..e5cbf71b9924b7ba623467fb4b95cbd121efd8d3 100644 --- a/examples/leftist_heap/why3session.xml +++ b/examples/leftist_heap/why3session.xml @@ -6,9 +6,6 @@ <prover id="3" name="CVC4" version="1.5" timelimit="5" steplimit="0" memlimit="1000"/> <file name="../leftist_heap.mlw" proved="true"> <theory name="Size" proved="true"> - <goal name="VC size" expl="VC for size" proved="true"> - <proof prover="1"><result status="valid" time="0.00" steps="1"/></proof> - </goal> <goal name="size_nonneg" proved="true"> <transf name="induction_ty_lex" proved="true" > <goal name="size_nonneg.0" proved="true"> diff --git a/examples/leftist_heap/why3shapes.gz b/examples/leftist_heap/why3shapes.gz index ea7672f1ecfbab0be1e4b532e2214b4f66d797c5..b66ed57f4e6a315aa6bf0ccd1deda868c87e5ac2 100644 Binary files a/examples/leftist_heap/why3shapes.gz and b/examples/leftist_heap/why3shapes.gz differ diff --git a/examples/linear_probing/why3session.xml b/examples/linear_probing/why3session.xml index ea7fe5d112ece5efeca0b167e051623d5dbf5fac..297bb268fedbe738dd16228bf3bfc4294ce762e6 100644 --- a/examples/linear_probing/why3session.xml +++ b/examples/linear_probing/why3session.xml @@ -13,9 +13,6 @@ <goal name="VC neq" expl="VC for neq" proved="true"> <proof prover="6"><result status="valid" time="0.00" steps="1"/></proof> </goal> - <goal name="VC dummy" expl="VC for dummy" proved="true"> - <proof prover="6"><result status="valid" time="0.00" steps="1"/></proof> - </goal> </theory> <theory name="LinearProbing" proved="true"> <goal name="VC bucket" expl="VC for bucket" proved="true"> @@ -55,9 +52,6 @@ <goal name="VC clear" expl="VC for clear" proved="true"> <proof prover="6"><result status="valid" time="0.07" steps="219"/></proof> </goal> - <goal name="VC next" expl="VC for next" proved="true"> - <proof prover="6"><result status="valid" time="0.01" steps="1"/></proof> - </goal> <goal name="VC find" expl="VC for find" proved="true"> <transf name="split_goal_right" proved="true" > <goal name="VC find.0" expl="precondition" proved="true"> diff --git a/examples/linear_probing/why3shapes.gz b/examples/linear_probing/why3shapes.gz index cc8d36a84a6612246961ed927ff7510f1ea4f86f..157043bcb0cf5dc3e4d5e6c9863d6ca795e63930 100644 Binary files a/examples/linear_probing/why3shapes.gz and b/examples/linear_probing/why3shapes.gz differ diff --git a/examples/linked_list_rev/why3session.xml b/examples/linked_list_rev/why3session.xml index ff58294c79e15b3b172ecedc3f3684870b8308b2..8bd7be91ee661411cb12f9ca4145c7bd90b60f1f 100644 --- a/examples/linked_list_rev/why3session.xml +++ b/examples/linked_list_rev/why3session.xml @@ -9,9 +9,6 @@ <prover id="5" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/> <file name="../linked_list_rev.mlw" proved="true"> <theory name="InPlaceRev" proved="true"> - <goal name="VC null" expl="VC for null" proved="true"> - <proof prover="2"><result status="valid" time="0.01"/></proof> - </goal> <goal name="VC mem_decomp" expl="VC for mem_decomp" proved="true"> <proof prover="2"><result status="valid" time="0.04"/></proof> </goal> @@ -145,9 +142,6 @@ </goal> </theory> <theory name="InPlaceRevSeq" proved="true"> - <goal name="VC null" expl="VC for null" proved="true"> - <proof prover="2"><result status="valid" time="0.01"/></proof> - </goal> <goal name="non_empty_seq" proved="true"> <proof prover="5"><result status="valid" time="0.31"/></proof> </goal> diff --git a/examples/linked_list_rev/why3shapes.gz b/examples/linked_list_rev/why3shapes.gz index cf4c3a703ed60cd2e4329d672455b3a0ad4a5083..8e310ad1194544fc3db765d987bf34a70fce36ac 100644 Binary files a/examples/linked_list_rev/why3shapes.gz and b/examples/linked_list_rev/why3shapes.gz differ diff --git a/examples/max_matrix/why3session.xml b/examples/max_matrix/why3session.xml index 89d0cf50fef0dae7a75ebb2bbd7ad1e226ad9b8b..ebb6dc8a2b41ca753d926dbdddc62552c019c553 100644 --- a/examples/max_matrix/why3session.xml +++ b/examples/max_matrix/why3session.xml @@ -8,12 +8,6 @@ <prover id="4" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/> <file name="../max_matrix.mlw" proved="true"> <theory name="MaxMatrixMemo" proved="true"> - <goal name="VC n" expl="VC for n" proved="true"> - <proof prover="4"><result status="valid" time="0.00" steps="1"/></proof> - </goal> - <goal name="VC m" expl="VC for m" proved="true"> - <proof prover="4"><result status="valid" time="0.00" steps="3"/></proof> - </goal> <goal name="sum_ind" proved="true"> <proof prover="4"><result status="valid" time="0.03" steps="66"/></proof> </goal> diff --git a/examples/max_matrix/why3shapes.gz b/examples/max_matrix/why3shapes.gz index ee5207c3abc941ce917e41b7b0bda3b9eb98d3d7..9e83295f21a41e310fb6b67ab8d8121b99e3c69c 100644 Binary files a/examples/max_matrix/why3shapes.gz and b/examples/max_matrix/why3shapes.gz differ diff --git a/examples/multiprecision/lineardecision/why3session.xml b/examples/multiprecision/lineardecision/why3session.xml index b36d2da7f07b82c195621df2efb49841062bf254..a6d0cca7d5aa2fd40d4740cde3d6f6417580f39d 100644 --- a/examples/multiprecision/lineardecision/why3session.xml +++ b/examples/multiprecision/lineardecision/why3session.xml @@ -8,13 +8,6 @@ <prover id="4" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/> <file name="../lineardecision.mlw" proved="true"> <theory name="LinearEquationsCoeffs" proved="true"> - <goal name="VC czero" expl="VC for czero" proved="true"> - <proof prover="2"><result status="valid" time="0.02"/></proof> - </goal> - <goal name="VC cone" expl="VC for cone" proved="true"> - <transf name="split_goal_right" proved="true" > - </transf> - </goal> <goal name="neg_mul" proved="true"> <proof prover="3"><result status="valid" time="0.06"/></proof> </goal> @@ -26,18 +19,6 @@ <goal name="VC expr_bound" expl="VC for expr_bound" proved="true"> <proof prover="2"><result status="valid" time="0.01"/></proof> </goal> - <goal name="VC valid_eq" expl="VC for valid_eq" proved="true"> - <proof prover="2"><result status="valid" time="0.01"/></proof> - </goal> - <goal name="VC eq_bound" expl="VC for eq_bound" proved="true"> - <proof prover="2"><result status="valid" time="0.01"/></proof> - </goal> - <goal name="VC valid_ctx" expl="VC for valid_ctx" proved="true"> - <proof prover="2"><result status="valid" time="0.01"/></proof> - </goal> - <goal name="VC ctx_bound" expl="VC for ctx_bound" proved="true"> - <proof prover="2"><result status="valid" time="0.01"/></proof> - </goal> <goal name="VC expr_bound_w" expl="VC for expr_bound_w" proved="true"> <transf name="split_goal_right" proved="true" > <goal name="VC expr_bound_w.0" expl="variant decrease" proved="true"> @@ -1587,12 +1568,6 @@ <goal name="VC valid_expr'" expl="VC for valid_expr'" proved="true"> <proof prover="2"><result status="valid" time="0.17"/></proof> </goal> - <goal name="VC valid_eq'" expl="VC for valid_eq'" proved="true"> - <proof prover="2"><result status="valid" time="0.02"/></proof> - </goal> - <goal name="VC valid_ctx'" expl="VC for valid_ctx'" proved="true"> - <proof prover="2"><result status="valid" time="0.01"/></proof> - </goal> <goal name="VC simp" expl="VC for simp" proved="true"> <transf name="split_goal_right" proved="true" > <goal name="VC simp.0" expl="postcondition" proved="true"> @@ -1735,12 +1710,6 @@ </goal> </theory> <theory name="RationalCoeffs" proved="true"> - <goal name="VC rzero" expl="VC for rzero" proved="true"> - <proof prover="2"><result status="valid" time="0.02"/></proof> - </goal> - <goal name="VC rone" expl="VC for rone" proved="true"> - <proof prover="2"><result status="valid" time="0.01"/></proof> - </goal> <goal name="VC prod_compat_eq" expl="VC for prod_compat_eq" proved="true"> <proof prover="2"><result status="valid" time="0.03"/></proof> </goal> @@ -2107,12 +2076,6 @@ <goal name="C.sub_def" proved="true"> <proof prover="2"><result status="valid" time="0.01"/></proof> </goal> - <goal name="C.VC czero" expl="VC for czero" proved="true"> - <proof prover="2"><result status="valid" time="0.01"/></proof> - </goal> - <goal name="C.VC cone" expl="VC for cone" proved="true"> - <proof prover="2"><result status="valid" time="0.01"/></proof> - </goal> <goal name="C.zero_def" proved="true"> <proof prover="2"><result status="valid" time="0.03"/></proof> </goal> @@ -2147,15 +2110,6 @@ </goal> </theory> <theory name="LinearDecisionInt" proved="true"> - <goal name="VC izero" expl="VC for izero" proved="true"> - <proof prover="2"><result status="valid" time="0.02"/></proof> - </goal> - <goal name="VC ione" expl="VC for ione" proved="true"> - <proof prover="2"><result status="valid" time="0.00"/></proof> - </goal> - <goal name="VC ieq" expl="VC for ieq" proved="true"> - <proof prover="2"><result status="valid" time="0.01"/></proof> - </goal> <goal name="VC iadd" expl="VC for iadd" proved="true"> <proof prover="2"><result status="valid" time="0.02"/></proof> </goal> @@ -2228,12 +2182,6 @@ <goal name="C.sub_def" proved="true"> <proof prover="2"><result status="valid" time="0.01"/></proof> </goal> - <goal name="C.VC czero" expl="VC for czero" proved="true"> - <proof prover="2"><result status="valid" time="0.01"/></proof> - </goal> - <goal name="C.VC cone" expl="VC for cone" proved="true"> - <proof prover="2"><result status="valid" time="0.02"/></proof> - </goal> <goal name="C.zero_def" proved="true"> <proof prover="2"><result status="valid" time="0.03"/></proof> </goal> @@ -2326,12 +2274,6 @@ </goal> </theory> <theory name="MP64Coeffs" proved="true"> - <goal name="VC mzero" expl="VC for mzero" proved="true"> - <proof prover="2"><result status="valid" time="0.02"/></proof> - </goal> - <goal name="VC mone" expl="VC for mone" proved="true"> - <proof prover="2"><result status="valid" time="0.01"/></proof> - </goal> <goal name="qinterp_def" proved="true"> <transf name="compute_in_goal" proved="true" > </transf> @@ -2969,12 +2911,6 @@ <goal name="C.sub_def" proved="true"> <proof prover="2"><result status="valid" time="0.01"/></proof> </goal> - <goal name="C.VC czero" expl="VC for czero" proved="true"> - <proof prover="2"><result status="valid" time="0.01"/></proof> - </goal> - <goal name="C.VC cone" expl="VC for cone" proved="true"> - <proof prover="2"><result status="valid" time="0.01"/></proof> - </goal> <goal name="C.zero_def" proved="true"> <proof prover="2"><result status="valid" time="0.02"/></proof> </goal> @@ -2998,12 +2934,6 @@ </goal> </theory> <theory name="LinearDecisionIntMP" proved="true"> - <goal name="VC mpzero" expl="VC for mpzero" proved="true"> - <proof prover="2"><result status="valid" time="0.02"/></proof> - </goal> - <goal name="VC mpone" expl="VC for mpone" proved="true"> - <proof prover="2"><result status="valid" time="0.01"/></proof> - </goal> <goal name="VC mpadd" expl="VC for mpadd" proved="true"> <proof prover="2"><result status="valid" time="0.02"/></proof> </goal> @@ -3079,12 +3009,6 @@ <goal name="C.sub_def" proved="true"> <proof prover="2"><result status="valid" time="0.01"/></proof> </goal> - <goal name="C.VC czero" expl="VC for czero" proved="true"> - <proof prover="2"><result status="valid" time="0.02"/></proof> - </goal> - <goal name="C.VC cone" expl="VC for cone" proved="true"> - <proof prover="2"><result status="valid" time="0.02"/></proof> - </goal> <goal name="C.zero_def" proved="true"> <transf name="compute_in_goal" proved="true" > </transf> @@ -3207,14 +3131,6 @@ </goal> </transf> </goal> - <goal name="VC eq_bound'" expl="VC for eq_bound'" proved="true"> - <transf name="split_goal_right" proved="true" > - </transf> - </goal> - <goal name="VC ctx_bound'" expl="VC for ctx_bound'" proved="true"> - <transf name="split_goal_right" proved="true" > - </transf> - </goal> <goal name="VC expr_bound_w'" expl="VC for expr_bound_w'" proved="true"> <transf name="split_goal_right" proved="true" > <goal name="VC expr_bound_w'.0" expl="variant decrease" proved="true"> diff --git a/examples/multiprecision/lineardecision/why3shapes.gz b/examples/multiprecision/lineardecision/why3shapes.gz index e197ecdde53de5044fc921efa816dd9a0b17e8fc..df6dfcf6762eecb8eee972cbb34b83a522d24759 100644 Binary files a/examples/multiprecision/lineardecision/why3shapes.gz and b/examples/multiprecision/lineardecision/why3shapes.gz differ diff --git a/examples/multiprecision/toom/why3session.xml b/examples/multiprecision/toom/why3session.xml index 254d1aaa7f26d967bd63748051ab50c59f023317..4380dad552219471bfe28161f26aa7fe7c7cf5be 100644 --- a/examples/multiprecision/toom/why3session.xml +++ b/examples/multiprecision/toom/why3session.xml @@ -9,10 +9,6 @@ <prover id="5" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/> <file name="../toom.mlw" proved="true"> <theory name="Toom" proved="true"> - <goal name="VC toom22_threshold" expl="VC for toom22_threshold" proved="true"> - <transf name="split_vc" proved="true" > - </transf> - </goal> <goal name="VC no_borrow" expl="VC for no_borrow" proved="true"> <transf name="split_goal_right" proved="true" > <goal name="VC no_borrow.0" expl="assertion" proved="true"> diff --git a/examples/multiprecision/toom/why3shapes.gz b/examples/multiprecision/toom/why3shapes.gz index d007990eaac63942a539cdb55df9e76a67851d78..5914877e2a86be830382c42688ad24fa8876a211 100644 Binary files a/examples/multiprecision/toom/why3shapes.gz and b/examples/multiprecision/toom/why3shapes.gz differ diff --git a/examples/optimal_replay/why3session.xml b/examples/optimal_replay/why3session.xml index d4f30bbfa9a1f5626411264510e67ff13a707926..eefa44bdf4aafa5461fc418561c65fb94ba8188e 100644 --- a/examples/optimal_replay/why3session.xml +++ b/examples/optimal_replay/why3session.xml @@ -10,9 +10,6 @@ <prover id="6" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/> <file name="../optimal_replay.mlw" proved="true"> <theory name="OptimalReplay" proved="true"> - <goal name="VC n" expl="VC for n" proved="true"> - <proof prover="6"><result status="valid" time="0.00" steps="1"/></proof> - </goal> <goal name="VC distance" expl="VC for distance" proved="true"> <transf name="split_goal_right" proved="true" > <goal name="VC distance.0" expl="array creation size" proved="true"> diff --git a/examples/optimal_replay/why3shapes.gz b/examples/optimal_replay/why3shapes.gz index 7e418f62a38a3a8ddf1386ad28c3994473ee32d8..37752287e7ca1da8d0e81c62f031bb3342c4caef 100644 Binary files a/examples/optimal_replay/why3shapes.gz and b/examples/optimal_replay/why3shapes.gz differ diff --git a/examples/pairing_heap_bin/why3session.xml b/examples/pairing_heap_bin/why3session.xml index 12ef25fdb31f4f1941e87c55d193138b633865b1..64ef1a8f81b867b5ebf435b33b80295d65a91489 100644 --- a/examples/pairing_heap_bin/why3session.xml +++ b/examples/pairing_heap_bin/why3session.xml @@ -6,9 +6,6 @@ <prover id="3" name="CVC4" version="1.5" timelimit="5" steplimit="0" memlimit="1000"/> <file name="../pairing_heap_bin.mlw" proved="true"> <theory name="Size" proved="true"> - <goal name="VC size" expl="VC for size" proved="true"> - <proof prover="1"><result status="valid" time="0.00" steps="2"/></proof> - </goal> <goal name="VC size_nonneg" expl="VC for size_nonneg" proved="true"> <proof prover="1"><result status="valid" time="0.00" steps="14"/></proof> </goal> diff --git a/examples/pairing_heap_bin/why3shapes.gz b/examples/pairing_heap_bin/why3shapes.gz index 2aeff4b5cf911ffb54981679261ca2ee45251e2d..db9d0b63d64904a6a64011572285505b2178317f 100644 Binary files a/examples/pairing_heap_bin/why3shapes.gz and b/examples/pairing_heap_bin/why3shapes.gz differ diff --git a/examples/patience/why3session.xml b/examples/patience/why3session.xml index 882fc19a3402dc8c35fc72a6b0dc8fbb064321b3..f2f460735c4d2eab702278ec05e280418d137916 100644 --- a/examples/patience/why3session.xml +++ b/examples/patience/why3session.xml @@ -75,9 +75,6 @@ <goal name="VC play_game" expl="VC for play_game" proved="true"> <proof prover="3"><result status="valid" time="0.00" steps="2"/></proof> </goal> - <goal name="VC test" expl="VC for test" proved="true"> - <proof prover="3"><result status="valid" time="0.00" steps="2"/></proof> - </goal> </theory> <theory name="PatienceAbstract" proved="true"> <goal name="VC play_card" expl="VC for play_card" proved="true"> @@ -349,9 +346,6 @@ </goal> </transf> </goal> - <goal name="VC test" expl="VC for test" proved="true"> - <proof prover="3"><result status="valid" time="0.00" steps="1"/></proof> - </goal> </theory> </file> </why3session> diff --git a/examples/patience/why3shapes.gz b/examples/patience/why3shapes.gz index 9058e837a9d003200de9574a2685f29d643f5e73..95d27581310d68dcf2ed89ae83dd1f4a7d317c7d 100644 Binary files a/examples/patience/why3shapes.gz and b/examples/patience/why3shapes.gz differ diff --git a/examples/prover/BacktrackArray/why3session.xml b/examples/prover/BacktrackArray/why3session.xml index c51746e37e56e20c24fdc98604f7977ac9cbde0d..0be17f05e30359d2c95f7abd86ee1d2daeb25c15 100644 --- a/examples/prover/BacktrackArray/why3session.xml +++ b/examples/prover/BacktrackArray/why3session.xml @@ -10,18 +10,6 @@ <prover id="6" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/> <file name="../BacktrackArray.mlw" proved="true"> <theory name="Impl" proved="true"> - <goal name="VC mone" expl="VC for mone" proved="true"> - <proof prover="3"><result status="valid" time="0.04"/></proof> - </goal> - <goal name="VC zero" expl="VC for zero" proved="true"> - <proof prover="3"><result status="valid" time="0.04"/></proof> - </goal> - <goal name="VC one" expl="VC for one" proved="true"> - <proof prover="3"><result status="valid" time="0.04"/></proof> - </goal> - <goal name="VC two" expl="VC for two" proved="true"> - <proof prover="3"><result status="valid" time="0.04"/></proof> - </goal> <goal name="VC create" expl="VC for create" proved="true"> <proof prover="2"><result status="valid" time="0.05" steps="135"/></proof> </goal> diff --git a/examples/prover/BacktrackArray/why3shapes.gz b/examples/prover/BacktrackArray/why3shapes.gz index 4b032ee92af4c1e3f617ba3f7bcff61fd396d0a1..6f5e8d1d70a9bca1cd75c0165bf160c34b03ad71 100644 Binary files a/examples/prover/BacktrackArray/why3shapes.gz and b/examples/prover/BacktrackArray/why3shapes.gz differ diff --git a/examples/prover/Firstorder_symbol_spec/why3session.xml b/examples/prover/Firstorder_symbol_spec/why3session.xml index 01d37168f6b8cc040e55fc22036980a8a75847a6..f00c9cb4f326621d2bb1c2d2c740fce9154b7707 100644 --- a/examples/prover/Firstorder_symbol_spec/why3session.xml +++ b/examples/prover/Firstorder_symbol_spec/why3session.xml @@ -5,7 +5,6 @@ <prover id="0" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="2" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/> -<prover id="3" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/> <prover id="7" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="1000"/> <file name="../Firstorder_symbol_spec.mlw" proved="true"> <theory name="Spec" proved="true"> @@ -14,9 +13,6 @@ <proof prover="1"><result status="valid" time="0.02"/></proof> <proof prover="2"><result status="valid" time="0.02" steps="5"/></proof> </goal> - <goal name="VC rename_symbol" expl="VC for rename_symbol" proved="true"> - <proof prover="3"><result status="valid" time="0.01"/></proof> - </goal> <goal name="VC renaming_composition_lemma_symbol" expl="VC for renaming_composition_lemma_symbol" proved="true"> <proof prover="0"><result status="valid" time="0.04"/></proof> <proof prover="1"><result status="valid" time="0.07"/></proof> diff --git a/examples/prover/Firstorder_symbol_spec/why3shapes.gz b/examples/prover/Firstorder_symbol_spec/why3shapes.gz index b39839d427d202343ce8ebe09ad374b66e3aabab..75ddc72b09958ae8b92a0af2b10f65936d39ffd5 100644 Binary files a/examples/prover/Firstorder_symbol_spec/why3shapes.gz and b/examples/prover/Firstorder_symbol_spec/why3shapes.gz differ diff --git a/examples/random_access_list/why3session.xml b/examples/random_access_list/why3session.xml index 57cc82763ea78c434c979b8d586919c59704d2c5..e5df45628f7de79c3db4188d81090147b2b25d66 100644 --- a/examples/random_access_list/why3session.xml +++ b/examples/random_access_list/why3session.xml @@ -232,9 +232,6 @@ </goal> </transf> </goal> - <goal name="VC f" expl="VC for f" proved="true"> - <proof prover="4"><result status="valid" time="0.02"/></proof> - </goal> <goal name="VC update" expl="VC for update" proved="true"> <proof prover="4"><result status="valid" time="0.06"/></proof> </goal> diff --git a/examples/random_access_list/why3shapes.gz b/examples/random_access_list/why3shapes.gz index 7033906adc2b588fc2065c6bfb87d950368f7c1f..3ffebde23708d789769f09409562c7e4977e6aa0 100644 Binary files a/examples/random_access_list/why3shapes.gz and b/examples/random_access_list/why3shapes.gz differ diff --git a/examples/register_allocation/why3session.xml b/examples/register_allocation/why3session.xml index 1cdfacb960cd4d87aebdd30875c17108ebdf3074..22507f8af120b2c9dd48216ca07bad23b5b2e7f4 100644 --- a/examples/register_allocation/why3session.xml +++ b/examples/register_allocation/why3session.xml @@ -142,9 +142,6 @@ </goal> </theory> <theory name="FiniteNumberOfRegisters" proved="true"> - <goal name="VC k" expl="VC for k" proved="true"> - <proof prover="1"><result status="valid" time="0.01" steps="1"/></proof> - </goal> <goal name="VC compile" expl="VC for compile" proved="true"> <transf name="split_goal_right" proved="true" > <goal name="VC compile.0" expl="precondition" proved="true"> @@ -318,9 +315,6 @@ </goal> </theory> <theory name="OptimalNumberOfRegisters" proved="true"> - <goal name="VC k" expl="VC for k" proved="true"> - <proof prover="1"><result status="valid" time="0.01" steps="1"/></proof> - </goal> <goal name="VC n" expl="VC for n" proved="true"> <proof prover="1"><result status="valid" time="0.03" steps="60"/></proof> </goal> diff --git a/examples/register_allocation/why3shapes.gz b/examples/register_allocation/why3shapes.gz index 4bb601f7658c15486a345af7892a15dc59b6aba1..60973321f833c5fa6003f34724e9381be095731c 100644 Binary files a/examples/register_allocation/why3shapes.gz and b/examples/register_allocation/why3shapes.gz differ diff --git a/examples/residual/why3session.xml b/examples/residual/why3session.xml index ca8fc56d7fb6f1aac7b047bb4db02de2a3623583..09a413b1365f98853ee7cba1fc2448d66b610185 100644 --- a/examples/residual/why3session.xml +++ b/examples/residual/why3session.xml @@ -149,20 +149,5 @@ </transf> </goal> </theory> -<theory name="Test" proved="true"> - <goal name="VC a" expl="VC for a" proved="true"> - <proof prover="1"><result status="valid" time="0.01" steps="4"/></proof> - </goal> - <goal name="VC aa" expl="VC for aa" proved="true"> - <proof prover="1"><result status="valid" time="0.00" steps="4"/></proof> - </goal> - <goal name="VC astar" expl="VC for astar" proved="true"> - <proof prover="1"><result status="valid" time="0.01" steps="4"/></proof> - </goal> - <goal name="VC test_astar" expl="VC for test_astar" proved="true"> - <transf name="split_goal_right" proved="true" > - </transf> - </goal> -</theory> </file> </why3session> diff --git a/examples/residual/why3shapes.gz b/examples/residual/why3shapes.gz index 361188fba8951be4282240efed1bfa83530292ef..3ea77a98c739a84d41f56d9ed4e3b8eb7b15cf2a 100644 Binary files a/examples/residual/why3shapes.gz and b/examples/residual/why3shapes.gz differ diff --git a/examples/ropes/why3session.xml b/examples/ropes/why3session.xml index 1d3d1363d4d455726284b56aa29cf1f6b3b7ba66..53aff6517d5552a04f95ffcd785e57dbb946b284 100644 --- a/examples/ropes/why3session.xml +++ b/examples/ropes/why3session.xml @@ -8,17 +8,11 @@ <prover id="5" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/> <file name="../ropes.mlw" proved="true"> <theory name="String" proved="true"> - <goal name="VC empty" expl="VC for empty" proved="true"> - <proof prover="5"><result status="valid" time="0.00"/></proof> - </goal> <goal name="app_assoc" proved="true"> <proof prover="5"><result status="valid" time="0.02"/></proof> </goal> </theory> <theory name="Rope" proved="true"> - <goal name="VC length" expl="VC for length" proved="true"> - <proof prover="5"><result status="valid" time="0.00"/></proof> - </goal> <goal name="rope_length_is_string_length" proved="true"> <transf name="induction_ty_lex" proved="true" > <goal name="rope_length_is_string_length.0" proved="true"> @@ -46,9 +40,6 @@ </goal> </theory> <theory name="Balance" proved="true"> - <goal name="VC max" expl="VC for max" proved="true"> - <proof prover="5"><result status="valid" time="0.01"/></proof> - </goal> <goal name="VC string_of_array_concat" expl="VC for string_of_array_concat" proved="true"> <proof prover="5"><result status="valid" time="0.09"/></proof> </goal> diff --git a/examples/ropes/why3shapes.gz b/examples/ropes/why3shapes.gz index 0e2f578b43b2b3dd8170d28349830226d669823b..66fae3bb0438eaba6ede232104a7698bba009c0e 100644 Binary files a/examples/ropes/why3shapes.gz and b/examples/ropes/why3shapes.gz differ diff --git a/examples/same_fringe/why3session.xml b/examples/same_fringe/why3session.xml index 7240f931525f0fc063a7d2606f547de515999663..12eb008f5ee99fcaba1cd933292ace80ebe00198 100644 --- a/examples/same_fringe/why3session.xml +++ b/examples/same_fringe/why3session.xml @@ -14,53 +14,9 @@ <goal name="VC same_fringe" expl="VC for same_fringe" proved="true"> <proof prover="0"><result status="valid" time="0.01" steps="15"/></proof> </goal> - <goal name="VC test1" expl="VC for test1" proved="true"> - <proof prover="0"><result status="valid" time="0.00" steps="5"/></proof> - </goal> - <goal name="VC test2" expl="VC for test2" proved="true"> - <proof prover="0"><result status="valid" time="0.00" steps="5"/></proof> - </goal> - <goal name="VC test3" expl="VC for test3" proved="true"> - <proof prover="0"><result status="valid" time="0.00" steps="5"/></proof> - </goal> - <goal name="VC a" expl="VC for a" proved="true"> - <proof prover="0"><result status="valid" time="0.00" steps="5"/></proof> - </goal> - <goal name="VC b" expl="VC for b" proved="true"> - <proof prover="0"><result status="valid" time="0.00" steps="5"/></proof> - </goal> - <goal name="VC leaf" expl="VC for leaf" proved="true"> - <proof prover="0"><result status="valid" time="0.00" steps="5"/></proof> - </goal> - <goal name="VC test4" expl="VC for test4" proved="true"> - <proof prover="0"><result status="valid" time="0.00" steps="5"/></proof> - </goal> - <goal name="VC test5" expl="VC for test5" proved="true"> - <proof prover="0"><result status="valid" time="0.00" steps="5"/></proof> - </goal> <goal name="VC bench" expl="VC for bench" proved="true"> <proof prover="0"><result status="valid" time="0.00" steps="5"/></proof> </goal> </theory> -<theory name="Test" proved="true"> - <goal name="VC test1" expl="VC for test1" proved="true"> - <proof prover="0"><result status="valid" time="0.00" steps="5"/></proof> - </goal> - <goal name="VC test2" expl="VC for test2" proved="true"> - <proof prover="0"><result status="valid" time="0.00" steps="5"/></proof> - </goal> - <goal name="VC test3" expl="VC for test3" proved="true"> - <proof prover="0"><result status="valid" time="0.00" steps="5"/></proof> - </goal> - <goal name="VC leaf" expl="VC for leaf" proved="true"> - <proof prover="0"><result status="valid" time="0.00" steps="5"/></proof> - </goal> - <goal name="VC test4" expl="VC for test4" proved="true"> - <proof prover="0"><result status="valid" time="0.00" steps="5"/></proof> - </goal> - <goal name="VC test5" expl="VC for test5" proved="true"> - <proof prover="0"><result status="valid" time="0.00" steps="5"/></proof> - </goal> -</theory> </file> </why3session> diff --git a/examples/same_fringe/why3shapes.gz b/examples/same_fringe/why3shapes.gz index c4d08255d3a7cfd627eaa54d8ad88e11fef86791..e1e9b1e5c10abdd6f63b9bf706d57801306788e2 100644 Binary files a/examples/same_fringe/why3shapes.gz and b/examples/same_fringe/why3shapes.gz differ diff --git a/examples/schorr_waite/why3session.xml b/examples/schorr_waite/why3session.xml index 69013a8e263aaef4b326365f043971d2bde3483d..d876172fad6d1b200139487d5e7d63ae5936ff6a 100644 --- a/examples/schorr_waite/why3session.xml +++ b/examples/schorr_waite/why3session.xml @@ -7,9 +7,6 @@ <prover id="3" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/> <file name="../schorr_waite.mlw" proved="true"> <theory name="SchorrWaite" proved="true"> - <goal name="VC null" expl="VC for null" proved="true"> - <proof prover="3"><result status="valid" time="0.01" steps="1"/></proof> - </goal> <goal name="VC tl_stackNodes" expl="VC for tl_stackNodes" proved="true"> <proof prover="3"><result status="valid" time="0.01" steps="19"/></proof> </goal> diff --git a/examples/schorr_waite/why3shapes.gz b/examples/schorr_waite/why3shapes.gz index af02140beac8985031eb921f483fb702aeb78af3..de5dba6463cc1244b25f25a109fd84e12fab7499 100644 Binary files a/examples/schorr_waite/why3shapes.gz and b/examples/schorr_waite/why3shapes.gz differ diff --git a/examples/stdlib/bintree/why3session.xml b/examples/stdlib/bintree/why3session.xml index 8eb404876f088e93505820fb2bd3885682f1599e..b365650742f6ca5754debeb221e7890edbb6c723 100644 --- a/examples/stdlib/bintree/why3session.xml +++ b/examples/stdlib/bintree/why3session.xml @@ -17,10 +17,6 @@ </goal> </theory> <theory name="Size" proved="true"> - <goal name="VC size" expl="VC for size" proved="true"> - <transf name="split_goal_right" proved="true" > - </transf> - </goal> <goal name="size_nonneg" proved="true"> <transf name="induction_ty_lex" proved="true" > <goal name="size_nonneg.0" proved="true"> @@ -46,10 +42,6 @@ </goal> </theory> <theory name="Height" proved="true"> - <goal name="VC height" expl="VC for height" proved="true"> - <transf name="split_goal_right" proved="true" > - </transf> - </goal> <goal name="height_nonneg" proved="true"> <transf name="induction_ty_lex" proved="true" > <goal name="height_nonneg.0" proved="true"> @@ -58,18 +50,6 @@ </transf> </goal> </theory> -<theory name="Inorder" proved="true"> - <goal name="VC inorder" expl="VC for inorder" proved="true"> - <transf name="split_goal_right" proved="true" > - </transf> - </goal> -</theory> -<theory name="Preorder" proved="true"> - <goal name="VC preorder" expl="VC for preorder" proved="true"> - <transf name="split_goal_right" proved="true" > - </transf> - </goal> -</theory> <theory name="InorderLength" proved="true"> <goal name="inorder_length" proved="true"> <transf name="induction_ty_lex" proved="true" > @@ -79,31 +59,5 @@ </transf> </goal> </theory> -<theory name="Zipper" proved="true"> - <goal name="VC zip" expl="VC for zip" proved="true"> - <transf name="split_goal_right" proved="true" > - </transf> - </goal> - <goal name="VC start" expl="VC for start" proved="true"> - <transf name="split_goal_right" proved="true" > - </transf> - </goal> - <goal name="VC up" expl="VC for up" proved="true"> - <transf name="split_goal_right" proved="true" > - </transf> - </goal> - <goal name="VC top" expl="VC for top" proved="true"> - <transf name="split_goal_right" proved="true" > - </transf> - </goal> - <goal name="VC down_left" expl="VC for down_left" proved="true"> - <transf name="split_goal_right" proved="true" > - </transf> - </goal> - <goal name="VC down_right" expl="VC for down_right" proved="true"> - <transf name="split_goal_right" proved="true" > - </transf> - </goal> -</theory> </file> </why3session> diff --git a/examples/stdlib/bintree/why3shapes.gz b/examples/stdlib/bintree/why3shapes.gz index 11bd3d199e58e6421d8f4f7ed0f9e4f856a5741b..b2bb07ee015240c5352646b7c689713cbd23e963 100644 Binary files a/examples/stdlib/bintree/why3shapes.gz and b/examples/stdlib/bintree/why3shapes.gz differ diff --git a/examples/stdlib/list/why3session.xml b/examples/stdlib/list/why3session.xml index cb4eccb0bc411682f9e8d67acf756e7cb6119e88..b2d032002280146b915df2666180db48ab66447b 100644 --- a/examples/stdlib/list/why3session.xml +++ b/examples/stdlib/list/why3session.xml @@ -14,9 +14,6 @@ </goal> </theory> <theory name="Length" proved="true"> - <goal name="VC length" expl="VC for length" proved="true"> - <proof prover="7"><result status="valid" time="0.00" steps="1"/></proof> - </goal> <goal name="Length_nonnegative" proved="true"> <transf name="induction_ty_lex" proved="true" > <goal name="Length_nonnegative.0" proved="true"> @@ -36,17 +33,6 @@ </transf> </goal> </theory> -<theory name="Quant" proved="true"> - <goal name="VC for_all" expl="VC for for_all" proved="true"> - <proof prover="7"><result status="valid" time="0.00" steps="1"/></proof> - </goal> - <goal name="VC for_some" expl="VC for for_some" proved="true"> - <proof prover="7"><result status="valid" time="0.00" steps="1"/></proof> - </goal> - <goal name="VC mem" expl="VC for mem" proved="true"> - <proof prover="7"><result status="valid" time="0.00" steps="1"/></proof> - </goal> -</theory> <theory name="Elements" proved="true"> <goal name="elements_mem" proved="true"> <transf name="induction_ty_lex" proved="true" > @@ -56,11 +42,6 @@ </transf> </goal> </theory> -<theory name="Nth" proved="true"> - <goal name="VC nth" expl="VC for nth" proved="true"> - <proof prover="7"><result status="valid" time="0.00" steps="1"/></proof> - </goal> -</theory> <theory name="NthLength" proved="true"> <goal name="nth_none_1" proved="true"> <transf name="induction_ty_lex" proved="true" > @@ -84,14 +65,6 @@ </transf> </goal> </theory> -<theory name="HdTl" proved="true"> - <goal name="VC hd" expl="VC for hd" proved="true"> - <proof prover="7"><result status="valid" time="0.00" steps="1"/></proof> - </goal> - <goal name="VC tl" expl="VC for tl" proved="true"> - <proof prover="7"><result status="valid" time="0.00" steps="1"/></proof> - </goal> -</theory> <theory name="NthHdTl" proved="true"> <goal name="Nth_tl" proved="true"> <proof prover="7"><result status="valid" time="0.00" steps="21"/></proof> @@ -101,9 +74,6 @@ </goal> </theory> <theory name="Append" proved="true"> - <goal name="VC infix ++" expl="VC for infix ++" proved="true"> - <proof prover="7"><result status="valid" time="0.00" steps="1"/></proof> - </goal> <goal name="Append_assoc" proved="true"> <transf name="induction_ty_lex" proved="true" > <goal name="Append_assoc.0" proved="true"> @@ -171,9 +141,6 @@ </goal> </theory> <theory name="Reverse" proved="true"> - <goal name="VC reverse" expl="VC for reverse" proved="true"> - <proof prover="7"><result status="valid" time="0.00" steps="1"/></proof> - </goal> <goal name="reverse_append" proved="true"> <transf name="induction_ty_lex" proved="true" > <goal name="reverse_append.0" proved="true"> @@ -214,9 +181,6 @@ </goal> </theory> <theory name="RevAppend" proved="true"> - <goal name="VC rev_append" expl="VC for rev_append" proved="true"> - <proof prover="7"><result status="valid" time="0.00" steps="1"/></proof> - </goal> <goal name="rev_append_append_l" proved="true"> <transf name="induction_ty_lex" proved="true" > <goal name="rev_append_append_l.0" proved="true"> @@ -242,11 +206,6 @@ <proof prover="7"><result status="valid" time="0.01" steps="40"/></proof> </goal> </theory> -<theory name="Combine" proved="true"> - <goal name="VC combine" expl="VC for combine" proved="true"> - <proof prover="7"><result status="valid" time="0.00" steps="1"/></proof> - </goal> -</theory> <theory name="Sorted" proved="true"> <goal name="sorted_mem" proved="true"> <transf name="split_goal_right" proved="true" > @@ -537,16 +496,6 @@ </transf> </goal> </theory> -<theory name="Prefix" proved="true"> - <goal name="VC prefix" expl="VC for prefix" proved="true"> - <proof prover="7"><result status="valid" time="0.00" steps="1"/></proof> - </goal> -</theory> -<theory name="Sum" proved="true"> - <goal name="VC sum" expl="VC for sum" proved="true"> - <proof prover="7"><result status="valid" time="0.00" steps="1"/></proof> - </goal> -</theory> <theory name="FoldLeft" proved="true"> <goal name="fold_left_append" proved="true"> <transf name="induction_ty_lex" proved="true" > diff --git a/examples/stdlib/list/why3shapes.gz b/examples/stdlib/list/why3shapes.gz index 0ab06fcb342bdf9412358ec18c9a7f13f8aafd95..df8b599f9bac291735f0cf86e496bdc04902fe8a 100644 Binary files a/examples/stdlib/list/why3shapes.gz and b/examples/stdlib/list/why3shapes.gz differ diff --git a/examples/sumrange/why3session.xml b/examples/sumrange/why3session.xml index bbc10b9a8c8405037299fdcbeff7519653561a3f..b11945276b08eb080cf56e59e1c28fd72e412b82 100644 --- a/examples/sumrange/why3session.xml +++ b/examples/sumrange/why3session.xml @@ -152,9 +152,6 @@ </goal> </theory> <theory name="CumulativeTree" proved="true"> - <goal name="VC indexes" expl="VC for indexes" proved="true"> - <proof prover="3"><result status="valid" time="0.01"/></proof> - </goal> <goal name="VC tree_of_array" expl="VC for tree_of_array" proved="true"> <transf name="split_goal_right" proved="true" > <goal name="VC tree_of_array.0" expl="index in array bounds" proved="true"> diff --git a/examples/sumrange/why3shapes.gz b/examples/sumrange/why3shapes.gz index e7edbad5767fac5f65683aa6261dab50e22fde1c..0904e6da4c895f0edf93c4437306fa18ebd6f1e5 100644 Binary files a/examples/sumrange/why3shapes.gz and b/examples/sumrange/why3shapes.gz differ diff --git a/examples/tortoise_and_hare/why3session.xml b/examples/tortoise_and_hare/why3session.xml index 863b81956c411f1dd49bebd83b3b9c30f70fd4bb..5930b798d87fc7669fc7d465aa242ddf26174102 100644 --- a/examples/tortoise_and_hare/why3session.xml +++ b/examples/tortoise_and_hare/why3session.xml @@ -8,9 +8,6 @@ <prover id="7" name="Eprover" version="1.8-001" timelimit="16" steplimit="0" memlimit="1000"/> <file name="../tortoise_and_hare.mlw" proved="true"> <theory name="TortoiseAndHareAlgorithm" proved="true"> - <goal name="VC x0" expl="VC for x0" proved="true"> - <proof prover="6"><result status="valid" time="0.02"/></proof> - </goal> <goal name="VC x_in_range" expl="VC for x_in_range" proved="true"> <proof prover="2"><result status="valid" time="0.36" steps="311"/></proof> </goal> diff --git a/examples/tortoise_and_hare/why3shapes.gz b/examples/tortoise_and_hare/why3shapes.gz index d45cb720800e501d6ae126576608bf899db2f5e5..ea95e87eeba49ecc7a1ee0a1030ee5b59bbf348b 100644 Binary files a/examples/tortoise_and_hare/why3shapes.gz and b/examples/tortoise_and_hare/why3shapes.gz differ diff --git a/examples/tree_height/why3session.xml b/examples/tree_height/why3session.xml index 13f39ce7f443784cc51644cf73cadb6b3915e799..96dd3a7e879a5062e64ec484dc9807770cf0699a 100644 --- a/examples/tree_height/why3session.xml +++ b/examples/tree_height/why3session.xml @@ -17,12 +17,6 @@ </goal> </theory> <theory name="Iteration" proved="true"> - <goal name="VC is_id" expl="VC for is_id" proved="true"> - <proof prover="5"><result status="valid" time="0.00" steps="1"/></proof> - </goal> - <goal name="VC is_result" expl="VC for is_result" proved="true"> - <proof prover="5"><result status="valid" time="0.00" steps="1"/></proof> - </goal> <goal name="sizek_nonneg" proved="true"> <transf name="induction_ty_lex" proved="true" > <goal name="sizek_nonneg.0" proved="true"> diff --git a/examples/tree_height/why3shapes.gz b/examples/tree_height/why3shapes.gz index e9b2a492d4387b984af2c96cfebda20fbc997128..d5641df7a4942451b29a3cac86e5d9062248e45e 100644 Binary files a/examples/tree_height/why3shapes.gz and b/examples/tree_height/why3shapes.gz differ diff --git a/examples/vacid_0_red_black_trees/why3session.xml b/examples/vacid_0_red_black_trees/why3session.xml index 20b142f3092bb17852ad509c62b4301460ea9c2d..1515ff01743009ad0b251b8f3aa8209fc4e5f80d 100644 --- a/examples/vacid_0_red_black_trees/why3session.xml +++ b/examples/vacid_0_red_black_trees/why3session.xml @@ -241,9 +241,6 @@ </goal> </theory> <theory name="Vacid0" proved="true"> - <goal name="VC default" expl="VC for default" proved="true"> - <proof prover="4"><result status="valid" time="0.01"/></proof> - </goal> <goal name="VC create" expl="VC for create" proved="true"> <proof prover="4"><result status="valid" time="0.03"/></proof> </goal> diff --git a/examples/vacid_0_red_black_trees/why3shapes.gz b/examples/vacid_0_red_black_trees/why3shapes.gz index b05b6e9d3e0f51d85065bd3b9e36176202025818..94ba810619915869ed950fe53fed04ad77d147df 100644 Binary files a/examples/vacid_0_red_black_trees/why3shapes.gz and b/examples/vacid_0_red_black_trees/why3shapes.gz differ diff --git a/examples/vacid_0_sparse_array/why3session.xml b/examples/vacid_0_sparse_array/why3session.xml index 7f242cf9a2c3127567a8f13ff62a132e16c4af07..bacb6160b167242c91ac34f2920f8a1e0e5570d8 100644 --- a/examples/vacid_0_sparse_array/why3session.xml +++ b/examples/vacid_0_sparse_array/why3session.xml @@ -64,15 +64,6 @@ </goal> </theory> <theory name="Harness" proved="true"> - <goal name="VC default" expl="VC for default" proved="true"> - <proof prover="3"><result status="valid" time="0.01" steps="1"/></proof> - </goal> - <goal name="VC c1" expl="VC for c1" proved="true"> - <proof prover="3"><result status="valid" time="0.01" steps="1"/></proof> - </goal> - <goal name="VC c2" expl="VC for c2" proved="true"> - <proof prover="3"><result status="valid" time="0.00" steps="1"/></proof> - </goal> <goal name="VC harness" expl="VC for harness" proved="true"> <proof prover="3"><result status="valid" time="0.12" steps="729"/></proof> </goal> diff --git a/examples/vacid_0_sparse_array/why3shapes.gz b/examples/vacid_0_sparse_array/why3shapes.gz index 0d42be6af3d55066ec9ccfd67db386b35dbd3063..68aa4aef12654466b2c971319d6c2294d1102424 100644 Binary files a/examples/vacid_0_sparse_array/why3shapes.gz and b/examples/vacid_0_sparse_array/why3shapes.gz differ diff --git a/examples/verifythis_2016_matrix_multiplication/strassen/why3session.xml b/examples/verifythis_2016_matrix_multiplication/strassen/why3session.xml index 9dbc750cd346055122365037f54a820a05ef3295..6ae4396ac52ac017d533d52c46ccbf903cf1329e 100644 --- a/examples/verifythis_2016_matrix_multiplication/strassen/why3session.xml +++ b/examples/verifythis_2016_matrix_multiplication/strassen/why3session.xml @@ -11,9 +11,6 @@ <goal name="VC blit" expl="VC for blit" proved="true"> <proof prover="1"><result status="valid" time="0.24" steps="784"/></proof> </goal> - <goal name="VC mdl" expl="VC for mdl" proved="true"> - <proof prover="1"><result status="valid" time="0.02" steps="4"/></proof> - </goal> <goal name="VC block" expl="VC for block" proved="true"> <proof prover="1"><result status="valid" time="0.12" steps="225"/></proof> </goal> diff --git a/examples/verifythis_2016_matrix_multiplication/strassen/why3shapes.gz b/examples/verifythis_2016_matrix_multiplication/strassen/why3shapes.gz index 66ea5cb8ab110711a616910bde88293e087c1134..825c43022815ada5f6eb373a5fa14dd98c983a41 100644 Binary files a/examples/verifythis_2016_matrix_multiplication/strassen/why3shapes.gz and b/examples/verifythis_2016_matrix_multiplication/strassen/why3shapes.gz differ diff --git a/examples/verifythis_2017_tree_buffer/why3session.xml b/examples/verifythis_2017_tree_buffer/why3session.xml index 514c8881373107bcef26c30342b4e5aaa36c3cc4..6055132e7d342bd7996ef3cd130bc58107bc133e 100644 --- a/examples/verifythis_2017_tree_buffer/why3session.xml +++ b/examples/verifythis_2017_tree_buffer/why3session.xml @@ -9,18 +9,6 @@ <prover id="5" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/> <file name="../verifythis_2017_tree_buffer.mlw" proved="true"> <theory name="Spec" proved="true"> - <goal name="VC take" expl="VC for take" proved="true"> - <proof prover="5"><result status="valid" time="0.00" steps="1"/></proof> - </goal> - <goal name="VC empty" expl="VC for empty" proved="true"> - <proof prover="5"><result status="valid" time="0.00" steps="1"/></proof> - </goal> - <goal name="VC add" expl="VC for add" proved="true"> - <proof prover="5"><result status="valid" time="0.00" steps="1"/></proof> - </goal> - <goal name="VC get" expl="VC for get" proved="true"> - <proof prover="5"><result status="valid" time="0.00" steps="1"/></proof> - </goal> <goal name="VC take_lemma" expl="VC for take_lemma" proved="true"> <transf name="split_goal_right" proved="true" > <goal name="VC take_lemma.0" expl="variant decrease" proved="true"> @@ -109,9 +97,6 @@ <goal name="VC rt" expl="VC for rt" proved="true"> <proof prover="5"><result status="valid" time="0.00" steps="6"/></proof> </goal> - <goal name="VC de_allocate" expl="VC for de_allocate" proved="true"> - <proof prover="5"><result status="valid" time="0.00" steps="1"/></proof> - </goal> <goal name="VC process_queue" expl="VC for process_queue" proved="true"> <proof prover="5"><result status="valid" time="0.01" steps="4"/></proof> </goal> diff --git a/examples/verifythis_2017_tree_buffer/why3shapes.gz b/examples/verifythis_2017_tree_buffer/why3shapes.gz index 1248ed971ab2dde7201611c8f0bfa90ff16a4162..d4de00ed8e2f94ff538f813f076289730d902dc3 100644 Binary files a/examples/verifythis_2017_tree_buffer/why3shapes.gz and b/examples/verifythis_2017_tree_buffer/why3shapes.gz differ diff --git a/examples/verifythis_2018_array_based_queuing_lock_1/why3session.xml b/examples/verifythis_2018_array_based_queuing_lock_1/why3session.xml index 017f2e85a241d7b91bf5093eefcc45f567226c98..ca5d76a18051cf8254e8e8a5d1b8d88ff80c02cd 100644 --- a/examples/verifythis_2018_array_based_queuing_lock_1/why3session.xml +++ b/examples/verifythis_2018_array_based_queuing_lock_1/why3session.xml @@ -7,18 +7,9 @@ <prover id="3" name="Z3" version="4.5.0" timelimit="5" steplimit="0" memlimit="1000"/> <file name="../verifythis_2018_array_based_queuing_lock_1.mlw" proved="true"> <theory name="Top" proved="true"> - <goal name="VC k" expl="VC for k" proved="true"> - <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof> - </goal> - <goal name="VC n" expl="VC for n" proved="true"> - <proof prover="0"><result status="valid" time="0.00" steps="2"/></proof> - </goal> <goal name="VC bounded_int" expl="VC for bounded_int" proved="true"> <proof prover="0"><result status="valid" time="0.00" steps="3"/></proof> </goal> - <goal name="VC bzero" expl="VC for bzero" proved="true"> - <proof prover="0"><result status="valid" time="0.00" steps="3"/></proof> - </goal> <goal name="VC bounded_int2" expl="VC for bounded_int2" proved="true"> <proof prover="0"><result status="valid" time="0.00" steps="6"/></proof> </goal> diff --git a/examples/verifythis_2018_array_based_queuing_lock_1/why3shapes.gz b/examples/verifythis_2018_array_based_queuing_lock_1/why3shapes.gz index e9b660c074827833b00bcd4ed77d146d970429f1..c07f4e35f4a714f127df7d39750a97c95e43a3dc 100644 Binary files a/examples/verifythis_2018_array_based_queuing_lock_1/why3shapes.gz and b/examples/verifythis_2018_array_based_queuing_lock_1/why3shapes.gz differ diff --git a/examples/verifythis_2018_array_based_queuing_lock_2/why3session.xml b/examples/verifythis_2018_array_based_queuing_lock_2/why3session.xml index 7f2ecc1a4925b9bda1b60b594a910c7b8c20fcbd..835b49bdbeb1835489d454837dd11ae78c6325cf 100644 --- a/examples/verifythis_2018_array_based_queuing_lock_2/why3session.xml +++ b/examples/verifythis_2018_array_based_queuing_lock_2/why3session.xml @@ -8,12 +8,6 @@ <prover id="4" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/> <file name="../verifythis_2018_array_based_queuing_lock_2.mlw" proved="true"> <theory name="ABQL" proved="true"> - <goal name="VC n" expl="VC for n" proved="true"> - <proof prover="3"><result status="valid" time="0.02"/></proof> - </goal> - <goal name="VC k" expl="VC for k" proved="true"> - <proof prover="4" memlimit="2000"><result status="valid" time="0.00" steps="2"/></proof> - </goal> <goal name="VC tick" expl="VC for tick" proved="true"> <proof prover="3"><result status="valid" time="0.01"/></proof> </goal> diff --git a/examples/verifythis_2018_array_based_queuing_lock_2/why3shapes.gz b/examples/verifythis_2018_array_based_queuing_lock_2/why3shapes.gz index 89d77158ce1cfb6628c31eb404f1b43d1da5d203..9c6f7208a1a07e2dde5ddfbe0faf7401b1e1af09 100644 Binary files a/examples/verifythis_2018_array_based_queuing_lock_2/why3shapes.gz and b/examples/verifythis_2018_array_based_queuing_lock_2/why3shapes.gz differ diff --git a/examples/verifythis_2018_mind_the_gap_1/why3session.xml b/examples/verifythis_2018_mind_the_gap_1/why3session.xml index a3c6f556ad60ad93e657b05d840a3ff8d215072a..57528e362ec17e38b7dbc8f1a704bded27815a03 100644 --- a/examples/verifythis_2018_mind_the_gap_1/why3session.xml +++ b/examples/verifythis_2018_mind_the_gap_1/why3session.xml @@ -5,9 +5,6 @@ <prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/> <file name="../verifythis_2018_mind_the_gap_1.mlw" proved="true"> <theory name="Top" proved="true"> - <goal name="VC any_char" expl="VC for any_char" proved="true"> - <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof> - </goal> <goal name="VC gap_buffer" expl="VC for gap_buffer" proved="true"> <proof prover="0"><result status="valid" time="0.01" steps="6"/></proof> </goal> diff --git a/examples/verifythis_2018_mind_the_gap_1/why3shapes.gz b/examples/verifythis_2018_mind_the_gap_1/why3shapes.gz index 772413a375fbae2b35f23404f5ff6daa6a2cfc8d..1f1525f0bd8c61dce51cb3af1977c8afdcec43e1 100644 Binary files a/examples/verifythis_2018_mind_the_gap_1/why3shapes.gz and b/examples/verifythis_2018_mind_the_gap_1/why3shapes.gz differ diff --git a/examples/verifythis_2018_mind_the_gap_2/why3session.xml b/examples/verifythis_2018_mind_the_gap_2/why3session.xml index ddba0ccd7753c65e592400cfdc46dfbe1a3dd558..69b8e7e841d7c5f1a4008aa9423a24ff316c1fc0 100644 --- a/examples/verifythis_2018_mind_the_gap_2/why3session.xml +++ b/examples/verifythis_2018_mind_the_gap_2/why3session.xml @@ -6,9 +6,6 @@ <prover id="2" name="Z3" version="4.6.0" timelimit="5" steplimit="0" memlimit="1000"/> <file name="../verifythis_2018_mind_the_gap_2.mlw" proved="true"> <theory name="GapBuffer" proved="true"> - <goal name="VC dummy_char" expl="VC for dummy_char" proved="true"> - <proof prover="2"><result status="valid" time="0.00"/></proof> - </goal> <goal name="VC buffer" expl="VC for buffer" proved="true"> <proof prover="2"><result status="valid" time="0.01"/></proof> </goal> @@ -62,9 +59,6 @@ </goal> </transf> </goal> - <goal name="VC k" expl="VC for k" proved="true"> - <proof prover="2"><result status="valid" time="0.02"/></proof> - </goal> <goal name="VC grow" expl="VC for grow" proved="true"> <transf name="split_vc" proved="true" > <goal name="VC grow.0" expl="array creation size" proved="true"> diff --git a/examples/verifythis_2018_mind_the_gap_2/why3shapes.gz b/examples/verifythis_2018_mind_the_gap_2/why3shapes.gz index 1231d795950c34746828dd9731cefc651d3d2262..9190cf14496fb62b673ed852f209f5a002aab49b 100644 Binary files a/examples/verifythis_2018_mind_the_gap_2/why3shapes.gz and b/examples/verifythis_2018_mind_the_gap_2/why3shapes.gz differ diff --git a/examples/verifythis_fm2012_treedel/why3session.xml b/examples/verifythis_fm2012_treedel/why3session.xml index 62cc025e3c0ee3c5a4664687ce79253d1b17968a..f595dd27e3a75e4a8a9b4f7413bc376c875437da 100644 --- a/examples/verifythis_fm2012_treedel/why3session.xml +++ b/examples/verifythis_fm2012_treedel/why3session.xml @@ -7,9 +7,6 @@ <prover id="6" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/> <file name="../verifythis_fm2012_treedel.mlw" proved="true"> <theory name="Memory" proved="true"> - <goal name="VC null" expl="VC for null" proved="true"> - <proof prover="6"><result status="valid" time="0.00" steps="1"/></proof> - </goal> <goal name="VC get_left" expl="VC for get_left" proved="true"> <proof prover="6"><result status="valid" time="0.00" steps="1"/></proof> </goal> @@ -46,9 +43,6 @@ </goal> </transf> </goal> - <goal name="VC zip" expl="VC for zip" proved="true"> - <proof prover="1" timelimit="1"><result status="valid" time="0.01"/></proof> - </goal> <goal name="inorder_zip" proved="true"> <transf name="induction_ty_lex" proved="true" > <goal name="inorder_zip.0" proved="true"> diff --git a/examples/verifythis_fm2012_treedel/why3shapes.gz b/examples/verifythis_fm2012_treedel/why3shapes.gz index 8af1ea7f203f36f12a9befd7fac1a5ad3c912b1e..cad822a7b2b4bd517710e8a9c10e383adb3f25c2 100644 Binary files a/examples/verifythis_fm2012_treedel/why3shapes.gz and b/examples/verifythis_fm2012_treedel/why3shapes.gz differ diff --git a/examples/vstte12_combinators/why3session.xml b/examples/vstte12_combinators/why3session.xml index de881789154c744482ca1e9bafdff0607ec2e4b2..fcf22818b684c2cb8377bd584623871eb01c5c7d 100644 --- a/examples/vstte12_combinators/why3session.xml +++ b/examples/vstte12_combinators/why3session.xml @@ -78,9 +78,6 @@ </goal> </transf> </goal> - <goal name="VC i" expl="VC for i" proved="true"> - <proof prover="0"><result status="valid" time="0.01" steps="12"/></proof> - </goal> <goal name="VC test_SKK" expl="VC for test_SKK" proved="true"> <proof prover="0"><result status="valid" time="0.00" steps="12"/></proof> </goal> diff --git a/examples/vstte12_combinators/why3shapes.gz b/examples/vstte12_combinators/why3shapes.gz index 5c9bd37e1cea643dd3d8493b75dea3ff43ab866c..a3b59bed1a5509d7a01c62f18fa9cdb217904f69 100644 Binary files a/examples/vstte12_combinators/why3shapes.gz and b/examples/vstte12_combinators/why3shapes.gz differ diff --git a/examples/vstte12_tree_reconstruction/why3session.xml b/examples/vstte12_tree_reconstruction/why3session.xml index 381fecb34aa671fbae8eeedd83d11f2e26dae7a1..d79cafc89f145ac2e8ede18bf9332da05928775e 100644 --- a/examples/vstte12_tree_reconstruction/why3session.xml +++ b/examples/vstte12_tree_reconstruction/why3session.xml @@ -9,10 +9,6 @@ <prover id="5" name="Coq" version="8.7.1" timelimit="5" steplimit="0" memlimit="1000"/> <file name="../vstte12_tree_reconstruction.mlw" proved="true"> <theory name="Tree" proved="true"> - <goal name="VC depths" expl="VC for depths" proved="true"> - <transf name="split_goal_right" proved="true" > - </transf> - </goal> <goal name="depths_head" proved="true"> <transf name="induction_ty_lex" proved="true" > <goal name="depths_head.0" proved="true"> @@ -207,9 +203,6 @@ </goal> </transf> </goal> - <goal name="VC map_leaf" expl="VC for map_leaf" proved="true"> - <proof prover="4" timelimit="1"><result status="valid" time="0.02"/></proof> - </goal> <goal name="map_leaf_depths" proved="true"> <transf name="induction_ty_lex" proved="true" > <goal name="map_leaf_depths.0" proved="true"> diff --git a/examples/vstte12_tree_reconstruction/why3shapes.gz b/examples/vstte12_tree_reconstruction/why3shapes.gz index 64eb7c4ee6c15a2a5448dc3a05d07849cea7150e..cb0ae7766119174c73a087be83079cf6dce02fb7 100644 Binary files a/examples/vstte12_tree_reconstruction/why3shapes.gz and b/examples/vstte12_tree_reconstruction/why3shapes.gz differ