Commit 310c51d0 authored by Andrei Paskevich's avatar Andrei Paskevich

rename "split_goal" to "split_goal_wp" in session files

parent 683ec2ad
......@@ -6,7 +6,7 @@
<file name="../algo65.mlw" expanded="true">
<theory name="Algo65" sum="0b5f4012ece51782edee31f59e5f2271" expanded="true">
<goal name="WP_parameter find" expl="VC for find" expanded="true">
<transf name="split_goal" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter find.1" expl="1. precondition">
<proof prover="0"><result status="valid" time="0.00"/></proof>
</goal>
......
......@@ -43,11 +43,11 @@
<proof prover="1" edited="bf_WP_BellmanFord_key_lemma_2_1.v"><result status="valid" time="20.51"/></proof>
</goal>
<goal name="WP_parameter relax" expl="VC for relax" expanded="true">
<transf name="split_goal" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter relax.1" expl="1. postcondition" expanded="true">
<transf name="inline_goal" expanded="true">
<goal name="WP_parameter relax.1.1" expl="1. postcondition" expanded="true">
<transf name="split_goal" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter relax.1.1.1" expl="1. postcondition" expanded="true">
<proof prover="1" timelimit="10" memlimit="0" edited="bf_WP_BellmanFord_WP_parameter_relax_7.v"><result status="valid" time="1.63"/></proof>
</goal>
......@@ -71,7 +71,7 @@
<goal name="WP_parameter relax.2" expl="2. postcondition" expanded="true">
<transf name="inline_goal" expanded="true">
<goal name="WP_parameter relax.2.1" expl="1. postcondition" expanded="true">
<transf name="split_goal" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter relax.2.1.1" expl="1. postcondition" expanded="true">
<proof prover="3" memlimit="0"><result status="valid" time="0.12"/></proof>
<proof prover="4" timelimit="15" memlimit="0"><result status="valid" time="0.04"/></proof>
......@@ -97,7 +97,7 @@
</transf>
</goal>
<goal name="WP_parameter bellman_ford" expl="VC for bellman_ford" expanded="true">
<transf name="split_goal" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter bellman_ford.1" expl="1. assertion" expanded="true">
<transf name="inline_goal" expanded="true">
<goal name="WP_parameter bellman_ford.1.1" expl="1. assertion" expanded="true">
......@@ -142,7 +142,7 @@
<proof prover="4"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="WP_parameter bellman_ford.8" expl="8. postcondition" expanded="true">
<transf name="split_goal" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter bellman_ford.8.1" expl="1. postcondition" expanded="true">
<proof prover="3" memlimit="0"><result status="valid" time="0.07"/></proof>
<proof prover="4"><result status="valid" time="0.06"/></proof>
......@@ -283,7 +283,7 @@
<proof prover="1" memlimit="1000" edited="bf_WP_BellmanFord_WP_parameter_bellman_ford_15.v"><result status="valid" time="3.16"/></proof>
</goal>
<goal name="WP_parameter bellman_ford.22" expl="22. loop invariant preservation" expanded="true">
<transf name="split_goal" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter bellman_ford.22.1" expl="1." expanded="true">
<proof prover="4" timelimit="15" memlimit="0"><result status="valid" time="0.02"/></proof>
</goal>
......@@ -299,7 +299,7 @@
<proof prover="4" timelimit="15" memlimit="0"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="WP_parameter bellman_ford.25" expl="25. postcondition" expanded="true">
<transf name="split_goal" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter bellman_ford.25.1" expl="1. postcondition" expanded="true">
<proof prover="3" memlimit="0"><result status="valid" time="0.13"/></proof>
<proof prover="4" timelimit="15" memlimit="0"><result status="valid" time="0.11"/></proof>
......
......@@ -10,7 +10,7 @@
<file name="../binary_sqrt.mlw" expanded="true">
<theory name="BinarySqrt" sum="e7841ea73be92679fe10f49e39fe670c" expanded="true">
<goal name="WP_parameter sqrt" expl="VC for sqrt" expanded="true">
<transf name="split_goal" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter sqrt.1" expl="1. postcondition">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
......
......@@ -13,7 +13,7 @@
<proof prover="0" edited="bresenham_M_closest_1.v"><result status="valid" time="1.52"/></proof>
</goal>
<goal name="WP_parameter bresenham" expl="VC for bresenham" expanded="true">
<transf name="split_goal" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter bresenham.1" expl="1. loop invariant init" expanded="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
......
......@@ -58,7 +58,7 @@ let () = printf "@[task:@\n%a@]@." Pretty.print_task task
*)
let inline = Trans.lookup_transform "inline_goal" env
let split = Trans.lookup_transform_l "split_goal" env
let split = Trans.lookup_transform_l "split_goal_right" env
let task_inline = Trans.apply inline task
......
......@@ -7,7 +7,7 @@
<file name="../checking_a_large_routine.mlw" expanded="true">
<theory name="CheckingALargeRoutine" sum="205c90ac4815ce20515e224b374c1b29" expanded="true">
<goal name="WP_parameter routine" expl="VC for routine" expanded="true">
<transf name="split_goal" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter routine.1" expl="1. loop invariant init" expanded="true">
<proof prover="1" memlimit="0"><result status="valid" time="0.01"/></proof>
</goal>
......@@ -32,7 +32,7 @@
</transf>
</goal>
<goal name="WP_parameter routine2" expl="VC for routine2" expanded="true">
<transf name="split_goal" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter routine2.1" expl="1. postcondition" expanded="true">
<proof prover="1" memlimit="0"><result status="valid" time="0.01"/></proof>
</goal>
......
......@@ -19,7 +19,7 @@
</theory>
<theory name="CountingSort" sum="865e6abe69816fef0093b6f9c8509aa7">
<goal name="WP_parameter counting_sort" expl="VC for counting_sort">
<transf name="split_goal">
<transf name="split_goal_wp">
<goal name="WP_parameter counting_sort.1" expl="1. array creation size">
<proof prover="3" memlimit="1000"><result status="valid" time="0.01"/></proof>
</goal>
......@@ -255,7 +255,7 @@
</theory>
<theory name="InPlaceCountingSort" sum="0f7e194423cc9d616e20bf0dab301e13">
<goal name="WP_parameter in_place_counting_sort" expl="VC for in_place_counting_sort">
<transf name="split_goal">
<transf name="split_goal_wp">
<goal name="WP_parameter in_place_counting_sort.1" expl="1. array creation size">
<proof prover="3" memlimit="1000"><result status="valid" time="0.01"/></proof>
</goal>
......@@ -492,7 +492,7 @@
</theory>
<theory name="Harness" sum="bb8ec9d065aa47c0593e7a58c0ea4eb8">
<goal name="WP_parameter harness" expl="VC for harness">
<transf name="split_goal">
<transf name="split_goal_wp">
<goal name="WP_parameter harness.1" expl="1. array creation size">
<proof prover="3" timelimit="20"><result status="valid" time="0.02"/></proof>
</goal>
......
......@@ -16,7 +16,7 @@
<proof prover="1" edited="decrease1_Decrease1_decrease1_induction_2.v"><result status="valid" time="1.10"/></proof>
</goal>
<goal name="WP_parameter search" expl="VC for search" expanded="true">
<transf name="split_goal" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter search.1" expl="1. loop invariant init" expanded="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
......@@ -113,7 +113,7 @@
</transf>
</goal>
<goal name="WP_parameter search_rec" expl="VC for search_rec" expanded="true">
<transf name="split_goal" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter search_rec.1" expl="1. index in array bounds" expanded="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
......
......@@ -48,7 +48,7 @@
<proof prover="0" timelimit="20" memlimit="0" edited="edit_distance_WP_EditDistance_suffix_length_1.v"><result status="valid" time="1.16"/></proof>
</goal>
<goal name="WP_parameter distance" expl="VC for distance" expanded="true">
<transf name="split_goal" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter distance.1" expl="1. array creation size" expanded="true">
<proof prover="2" timelimit="30" memlimit="0"><result status="valid" time="0.01"/></proof>
</goal>
......
......@@ -11,7 +11,7 @@
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter memo_fibo" expl="VC for memo_fibo" expanded="true">
<transf name="split_goal" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter memo_fibo.1" expl="1. postcondition" expanded="true">
<proof prover="1" memlimit="0"><result status="valid" time="0.00"/></proof>
</goal>
......
......@@ -355,7 +355,7 @@
</theory>
<theory name="FibonacciLogarithmic" sum="98b45ab695eea24c48e7007e7c054fff">
<goal name="WP_parameter logfib" expl="VC for logfib">
<transf name="split_goal">
<transf name="split_goal_wp">
<goal name="WP_parameter logfib.1" expl="1. postcondition">
<proof prover="1" memlimit="0"><result status="valid" time="0.01"/></proof>
<proof prover="3" memlimit="0"><result status="valid" time="0.00"/></proof>
......
......@@ -9,7 +9,7 @@
<file name="../find.mlw" expanded="true">
<theory name="FIND" sum="4aa63090bb3fc7badaf802a8703db86c" expanded="true">
<goal name="WP_parameter find" expl="VC for find" expanded="true">
<transf name="split_goal" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter find.1" expl="1. loop invariant init">
<proof prover="2" memlimit="0"><result status="valid" time="0.02"/></proof>
</goal>
......@@ -32,7 +32,7 @@
<proof prover="2" memlimit="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter find.8" expl="8. loop invariant preservation">
<transf name="split_goal">
<transf name="split_goal_wp">
<goal name="WP_parameter find.8.1" expl="1.">
<proof prover="1"><result status="valid" time="0.06"/></proof>
<proof prover="2" memlimit="0"><result status="valid" time="0.05"/></proof>
......@@ -56,7 +56,7 @@
</goal>
<goal name="WP_parameter find.11" expl="11. index in array bounds">
<proof prover="2" memlimit="0"><result status="valid" time="0.01"/></proof>
<transf name="split_goal">
<transf name="split_goal_wp">
<goal name="WP_parameter find.11.1" expl="1.">
<proof prover="2" memlimit="0"><result status="valid" time="0.02"/></proof>
</goal>
......@@ -68,7 +68,7 @@
</transf>
</goal>
<goal name="WP_parameter find.12" expl="12. loop invariant preservation">
<transf name="split_goal">
<transf name="split_goal_wp">
<goal name="WP_parameter find.12.1" expl="1.">
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
......@@ -132,7 +132,7 @@
<proof prover="2" memlimit="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter find.29" expl="29. loop invariant preservation">
<transf name="split_goal">
<transf name="split_goal_wp">
<goal name="WP_parameter find.29.1" expl="1.">
<proof prover="2" memlimit="0"><result status="valid" time="0.14"/></proof>
</goal>
......
......@@ -6,7 +6,7 @@
<file name="../flag.mlw" expanded="true">
<theory name="Flag" sum="4eb4d9f1a40b59d554e0446a13fa099c" expanded="true">
<goal name="WP_parameter dutch_flag" expl="VC for dutch_flag" expanded="true">
<transf name="split_goal" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter dutch_flag.1" expl="1. loop invariant init">
<proof prover="0"><result status="valid" time="0.00"/></proof>
</goal>
......
......@@ -46,7 +46,7 @@
<proof prover="7"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="WP_parameter swap" expl="VC for swap" expanded="true">
<transf name="split_goal" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter swap.1" expl="1. postcondition" expanded="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
......@@ -62,7 +62,7 @@
</transf>
</goal>
<goal name="WP_parameter dutch_flag" expl="VC for dutch_flag" expanded="true">
<transf name="split_goal" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter dutch_flag.1" expl="1. loop invariant init" expanded="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
......
......@@ -6,7 +6,7 @@
<file name="../foveoos11_challenge1.mlw" expanded="true">
<theory name="Max" sum="b24dcf21da5e8fb20f2e744bb5b7bcce" expanded="true">
<goal name="WP_parameter max" expl="VC for max" expanded="true">
<transf name="split_goal" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter max.1" expl="1. loop invariant init">
<proof prover="0" memlimit="1000"><result status="valid" time="0.01"/></proof>
</goal>
......
......@@ -8,7 +8,7 @@
<file name="../foveoos11_challenge3.mlw" expanded="true">
<theory name="TwoEqualElements" sum="16607d44c864bb538321cf919e46dd1a" expanded="true">
<goal name="WP_parameter two_equal_elements" expl="VC for two_equal_elements" expanded="true">
<transf name="split_goal" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter two_equal_elements.1" expl="1. array creation size" expanded="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
......
......@@ -14,7 +14,7 @@
<file name="../gcd.mlw" expanded="true">
<theory name="EuclideanAlgorithm" sum="b0df4168cded97647349f707db0a9299" expanded="true">
<goal name="WP_parameter euclid" expl="VC for euclid">
<transf name="split_goal">
<transf name="split_goal_wp">
<goal name="WP_parameter euclid.1" expl="1. postcondition">
<proof prover="2" timelimit="2" memlimit="0"><result status="valid" time="0.01"/></proof>
<proof prover="3" memlimit="0"><result status="valid" time="0.02"/></proof>
......
......@@ -7,7 +7,7 @@
<file name="../gcd_bezout.mlw" expanded="true">
<theory name="GcdBezout" sum="edcb3513e2f4c1021dbba64af48b9083" expanded="true">
<goal name="WP_parameter gcd" expl="VC for gcd" expanded="true">
<transf name="split_goal" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter gcd.1" expl="1. loop invariant init" expanded="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
......
......@@ -26,7 +26,7 @@
<proof prover="4" timelimit="10" memlimit="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter combine" expl="VC for combine" expanded="true">
<transf name="split_goal" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter combine.1" expl="1. postcondition" expanded="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
......@@ -50,7 +50,7 @@
<proof prover="7"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="WP_parameter combine.8" expl="8. postcondition" expanded="true">
<transf name="split_goal" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter combine.8.1" expl="1. postcondition" expanded="true">
<proof prover="1" edited="generate_all_trees_WP_GenerateAllTrees_WP_parameter_combine_2.v"><result status="valid" time="1.15"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
......@@ -74,7 +74,7 @@
<proof prover="4"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="WP_parameter combine.13" expl="13. postcondition" expanded="true">
<transf name="split_goal" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter combine.13.1" expl="1. postcondition" expanded="true">
<proof prover="5"><result status="valid" time="0.05"/></proof>
</goal>
......@@ -90,7 +90,7 @@
<proof prover="4"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter combine.16" expl="16. postcondition" expanded="true">
<transf name="split_goal" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter combine.16.1" expl="1. postcondition" expanded="true">
<proof prover="4" timelimit="10" memlimit="0"><result status="valid" time="0.01"/></proof>
</goal>
......@@ -102,7 +102,7 @@
</transf>
</goal>
<goal name="WP_parameter all_trees" expl="VC for all_trees" expanded="true">
<transf name="split_goal" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter all_trees.1" expl="1. array creation size" expanded="true">
<proof prover="4" timelimit="10" memlimit="0"><result status="valid" time="0.01"/></proof>
</goal>
......
......@@ -431,7 +431,7 @@
<result status="unknown" time="0.55"/>
</proof>
<transf
name="split_goal"
name="split_goal_wp"
proved="false"
expanded="true">
<goal
......
......@@ -114,7 +114,7 @@
<proof prover="1" memlimit="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter compute_writes" expl="VC for compute_writes">
<transf name="split_goal">
<transf name="split_goal_wp">
<goal name="WP_parameter compute_writes.1" expl="1. postcondition">
<proof prover="1" memlimit="0"><result status="valid" time="0.19"/></proof>
</goal>
......@@ -152,7 +152,7 @@
</transf>
</goal>
<goal name="WP_parameter wp" expl="VC for wp">
<transf name="split_goal">
<transf name="split_goal_wp">
<goal name="WP_parameter wp.1" expl="1. postcondition">
<proof prover="1" memlimit="0"><result status="valid" time="0.02"/></proof>
<proof prover="2" timelimit="3" memlimit="0"><result status="valid" time="0.04"/></proof>
......
......@@ -11,7 +11,7 @@
<file name="../insertion_sort.mlw" expanded="true">
<theory name="InsertionSort" sum="e2df9c9353b35c33f82300852304729c" expanded="true">
<goal name="WP_parameter insertion_sort" expl="VC for insertion_sort">
<transf name="split_goal">
<transf name="split_goal_wp">
<goal name="WP_parameter insertion_sort.1" expl="1. postcondition">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3" memlimit="0"><result status="valid" time="0.03"/></proof>
......
......@@ -21,7 +21,7 @@
</theory>
<theory name="NewtonMethod" sum="ec5077fe3a5ab0d237e75e1e6c2b762c" expanded="true">
<goal name="WP_parameter sqrt" expl="VC for sqrt" expanded="true">
<transf name="split_goal" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter sqrt.1" expl="1. postcondition">
<proof prover="0" timelimit="20"><result status="valid" time="0.02"/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof>
......@@ -35,7 +35,7 @@
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter sqrt.3" expl="3. loop invariant init">
<transf name="split_goal">
<transf name="split_goal_wp">
<goal name="WP_parameter sqrt.3.1" expl="1.">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof>
......@@ -67,7 +67,7 @@
</transf>
</goal>
<goal name="WP_parameter sqrt.4" expl="4. loop invariant preservation" expanded="true">
<transf name="split_goal" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter sqrt.4.1" expl="1.">
<proof prover="0"><result status="valid" time="3.53"/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof>
......
......@@ -41,7 +41,7 @@
<proof prover="2" timelimit="10" memlimit="0"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter initnext" expl="VC for initnext" expanded="true">
<transf name="split_goal" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter initnext.1" expl="1. array creation size">
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
......@@ -176,7 +176,7 @@
</transf>
</goal>
<goal name="WP_parameter kmp" expl="VC for kmp">
<transf name="split_goal">
<transf name="split_goal_wp">
<goal name="WP_parameter kmp.1" expl="1. precondition">
<proof prover="2" timelimit="10" memlimit="0"><result status="valid" time="0.01"/></proof>
</goal>
......
......@@ -17,7 +17,7 @@
<proof prover="1" timelimit="10" memlimit="0" edited="knuth_prime_numbers_WP_PrimeNumbers_exists_prime_1.v"><result status="valid" time="1.41"/></proof>
</goal>
<goal name="WP_parameter prime_numbers" expl="VC for prime_numbers">
<transf name="split_goal">
<transf name="split_goal_wp">
<goal name="WP_parameter prime_numbers.1" expl="1. array creation size">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3" memlimit="0"><result status="valid" time="0.01"/></proof>
......
......@@ -27,7 +27,7 @@
<proof prover="0" edited="linked_list_rev_WP_InPlaceRev_list_seg_no_repet_1.v"><result status="valid" time="1.07"/></proof>
</goal>
<goal name="WP_parameter in_place_reverse" expl="VC for in_place_reverse" expanded="true">
<transf name="split_goal" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter in_place_reverse.1" expl="1. loop invariant init">
<proof prover="2" memlimit="1000"><result status="valid" time="0.02"/></proof>
</goal>
......
......@@ -11,7 +11,7 @@
</goal>
<goal name="G2" expanded="true">
<proof prover="1" timelimit="4"><result status="unknown" time="0.00"/></proof>
<transf name="split_goal" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="G2.1" expl="1." expanded="true">
<proof prover="0" edited="hello_proof_HelloProof_G2_1.v"><result status="unknown" time="0.99"/></proof>
<proof prover="1" memlimit="1000"><result status="unknown" time="0.00"/></proof>
......
......@@ -16,7 +16,7 @@
<proof prover="1" timelimit="47" memlimit="0"><result status="valid" time="0.79"/></proof>
</goal>
<goal name="WP_parameter maximum" expl="VC for maximum" expanded="true">
<transf name="split_goal" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter maximum.1" expl="1. postcondition">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
......@@ -60,9 +60,9 @@
</transf>
</goal>
<goal name="WP_parameter memo" expl="VC for memo">
<transf name="split_goal">
<transf name="split_goal_wp">
<goal name="WP_parameter memo.1" expl="1. postcondition">
<transf name="split_goal">
<transf name="split_goal_wp">
<goal name="WP_parameter memo.1.1" expl="1.">
<proof prover="3" timelimit="5" memlimit="1000"><result status="valid" time="0.02"/></proof>
</goal>
......@@ -85,14 +85,14 @@
</transf>
</goal>
<goal name="WP_parameter maxmat" expl="VC for maxmat">
<transf name="split_goal">
<transf name="split_goal_wp">
<goal name="WP_parameter maxmat.1" expl="1. assertion">
<proof prover="3" timelimit="5" memlimit="1000"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter maxmat.2" expl="2. precondition">
<transf name="inline_goal">
<goal name="WP_parameter maxmat.2.1" expl="1. precondition">
<transf name="split_goal">
<transf name="split_goal_wp">
<goal name="WP_parameter maxmat.2.1.1" expl="1.">
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
......@@ -116,7 +116,7 @@
</transf>
</goal>
<goal name="WP_parameter maxmat.3" expl="3. postcondition">
<transf name="split_goal">
<transf name="split_goal_wp">
<goal name="WP_parameter maxmat.3.1" expl="1. postcondition">
<transf name="inline_goal">
<goal name="WP_parameter maxmat.3.1.1" expl="1. postcondition">
......
......@@ -15,7 +15,7 @@
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter f91_nonrec" expl="VC for f91_nonrec" expanded="true">
<transf name="split_goal" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter f91_nonrec.1" expl="1. loop invariant init" expanded="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
......
......@@ -678,7 +678,7 @@
</theory>
<theory name="Mergesort" sum="677ecc2cc8e9a27b2fc4db5ff998a2b1">
<goal name="WP_parameter split" expl="VC for split">
<transf name="split_goal">
<transf name="split_goal_wp">
<goal name="WP_parameter split.1" expl="1. postcondition">
<proof prover="9"><result status="valid" time="0.03"/></proof>
</goal>
......@@ -689,7 +689,7 @@
<proof prover="9"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter split.4" expl="4. postcondition">
<transf name="split_goal">
<transf name="split_goal_wp">
<goal name="WP_parameter split.4.1" expl="1.">
<proof prover="9"><result status="valid" time="0.02"/></proof>
</goal>
......@@ -707,7 +707,7 @@
</transf>
</goal>
<goal name="WP_parameter mergesort" expl="VC for mergesort">
<transf name="split_goal">
<transf name="split_goal_wp">
<goal name="WP_parameter mergesort.1" expl="1. postcondition">
<proof prover="9"><result status="valid" time="0.00"/></proof>
</goal>
......@@ -724,7 +724,7 @@
<proof prover="9"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter mergesort.6" expl="6. postcondition">
<transf name="split_goal">
<transf name="split_goal_wp">
<goal name="WP_parameter mergesort.6.1" expl="1.">
<proof prover="9"><result status="valid" time="0.00"/></proof>
</goal>
......
......@@ -16,7 +16,7 @@
<file name="../mergesort_queue.mlw" expanded="true">
<theory name="MergesortQueue" sum="b46de19477e299c22fe69d96d0b7166a" expanded="true">
<goal name="WP_parameter merge" expl="VC for merge">
<transf name="split_goal">
<transf name="split_goal_wp">
<goal name="WP_parameter merge.1" expl="1. loop invariant init">
<proof prover="9"><result status="valid" time="0.02"/></proof>
</goal>
......
......@@ -8,7 +8,7 @@
<file name="../mjrty.mlw" expanded="true">
<theory name="Mjrty" sum="17a949696d46c4232e2f3472816482de" expanded="true">
<goal name="WP_parameter mjrty" expl="VC for mjrty" expanded="true">
<transf name="split_goal" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter mjrty.1" expl="1. index in array bounds" expanded="true">
<proof prover="1" timelimit="5" memlimit="1000"><result status="valid" time="0.01"/></proof>
</goal>
......
......@@ -9,7 +9,7 @@
<file name="../muller.mlw">
<theory name="Muller" sum="c15e422322bde3321531e330e3ec4e70">
<goal name="WP_parameter compact" expl="VC for compact">
<transf name="split_goal">
<transf name="split_goal_wp">
<goal name="WP_parameter compact.1" expl="1. array creation size">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="1" timelimit="10" memlimit="0"><result status="valid" time="0.01"/></proof>
......
......@@ -7,7 +7,7 @@
<file name="../my_cosine.mlw" expanded="true">
<theory name="M" sum="d51240628b8088b176f87798a8258835" expanded="true">
<goal name="WP_parameter my_cosine" expl="VC for my_cosine" expanded="true">
<transf name="split_goal" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter my_cosine.1" expl="1. assertion" expanded="true">
<proof prover="0" edited="my_cosine_M_WP_parameter_my_cosine_1.v"><result status="valid" time="3.83"/></proof>
</goal>
......
......@@ -12,7 +12,7 @@
<file name="../optimal_replay.mlw" expanded="true">
<theory name="OptimalReplay" sum="1fdf083e4b86c6fb71d8b4ddbcd7acec" expanded="true">
<goal name="WP_parameter distance" expl="VC for distance" expanded="true">
<transf name="split_goal" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter distance.1" expl="1. array creation size">
<proof prover="3" memlimit="0"><result status="valid" time="0.00"/></proof>
</goal>
......@@ -95,7 +95,7 @@
<goal name="WP_parameter distance.25" expl="25. assertion" expanded="true">
<transf name="inline_goal" expanded="true">
<goal name="WP_parameter distance.25.1" expl="1. assertion" expanded="true">
<transf name="split_goal" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter distance.25.1.1" expl="1. assertion">
<proof prover="3" memlimit="0"><result status="valid" time="0.01"/></proof>
</goal>
......
......@@ -12,14 +12,14 @@
<proof prover="2" timelimit="3" memlimit="0"><result status="valid" time="0.39"/></proof>
</goal>
<goal name="WP_parameter fast_exp_imperative" expl="VC for fast_exp_imperative" expanded="true">
<transf name="split_goal" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter fast_exp_imperative.1" expl="1. loop invariant init" expanded="true">
<proof prover="1" timelimit="10"><result status="valid" time="0.00"/></proof>
<proof prover="2" memlimit="0"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter fast_exp_imperative.2" expl="2. loop invariant preservation" expanded="true">
<transf name="split_goal" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter fast_exp_imperative.2.1" expl="1." expanded="true">
<proof prover="2" timelimit="10"><result status="valid" time="0.01"/></proof>
</goal>
......@@ -34,7 +34,7 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter fast_exp_imperative.4" expl="4. loop invariant preservation" expanded="true">
<transf name="split_goal" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter fast_exp_imperative.4.1" expl="1." expanded="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2" memlimit="0"><result status="valid" time="0.02"/></proof>
......@@ -51,7 +51,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter fast_exp_imperative.6" expl="6. postcondition" expanded="true">
<transf name="split_goal" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter fast_exp_imperative.6.1" expl="1. postcondition" expanded="true">
<proof prover="2" memlimit="0"><result status="valid" time="0.01"/></proof>
</goal>
......
......@@ -15,7 +15,7 @@
</theory>
<theory name="NQueensSetsTermination" sum="643fbc4ed120bd5f297aa232ffa610d8">
<goal name="WP_parameter t" expl="VC for t">
<transf name="split_goal">
<transf name="split_goal_wp">
<goal name="WP_parameter t.1" expl="1. loop invariant init">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
......@@ -50,7 +50,7 @@
</theory>
<theory name="NQueensSets" sum="4454c0ee66b324191db088e01edc03ff" expanded="true">
<goal name="WP_parameter t3" expl="VC for t3">
<transf name="split_goal">
<transf name="split_goal_wp">
<goal name="WP_parameter t3.1" expl="1. loop invariant init">
<proof prover="1"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.04"/></proof>
......@@ -62,7 +62,7 @@
<proof prover="3"><result status="valid" time="0.79"/></proof>
</goal>
<goal name="WP_parameter t3.3" expl="3. precondition">
<transf name="split_goal">
<transf name="split_goal_wp">
<goal name="WP_parameter t3.3.1" expl="1.">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
......@@ -109,7 +109,7 @@
<goal name="WP_parameter t3.3.12" expl="12.">
<transf name="inline_goal">
<goal name="WP_parameter t3.3.12.1" expl="1.">
<transf name="split_goal">
<transf name="split_goal_wp">
<goal name="WP_parameter t3.3.12.1.1" expl="1.">
<proof prover="3"><result status="valid" time="2.69"/></proof>
</goal>
......@@ -818,7 +818,7 @@
</transf>
</goal>
<goal name="WP_parameter t3.4" expl="4. loop invariant preservation">
<transf name="split_goal">
<transf name="split_goal_wp">
<goal name="WP_parameter t3.4.1" expl="1.">
<proof prover="1"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
......@@ -2792,7 +2792,7 @@
<proof prover="3"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="WP_parameter t3.6" expl="6. postcondition">