Commit 5cac408d authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Merge branch 'new_ide'

# Conflicts:
#	Makefile.in
#	examples/WP_revisited/blocking_semantics5/why3session.xml
#	examples/WP_revisited/wp2/why3session.xml
#	examples/algo63/why3session.xml
#	examples/algo64/why3session.xml
#	examples/algo65/why3session.xml
#	examples/all_distinct/why3session.xml
#	examples/arm/why3session.xml
#	examples/avl/association_list/why3session.xml
#	examples/avl/avl/why3session.xml
#	examples/avl/priority_queue/why3session.xml
#	examples/avl/ral/why3session.xml
#	examples/avl/sorted/why3session.xml
#	examples/avl/tables/why3session.xml
#	examples/bag/why3session.xml
#	examples/balance/why3session.xml
#	examples/bellman_ford/why3session.xml
#	examples/bignum/why3session.xml
#	examples/binary_search/why3session.xml
#	examples/binary_sort/why3session.xml
#	examples/binary_sqrt/why3session.xml
#	examples/binomial_heap/why3session.xml
#	examples/bitcount/why3session.xml
#	examples/bitvector_examples/why3session.xml
#	examples/bitwalker/why3session.xml
#	examples/braun_trees/why3session.xml
#	examples/bresenham/why3session.xml
#	examples/bts/16_subst/why3shapes.gz
#	examples/bubble_sort/why3session.xml
#	examples/checking_a_large_routine/why3session.xml
#	examples/coincidence_count/why3session.xml
#	examples/coincidence_count_list/why3session.xml
#	examples/conjugate/why3session.xml
#	examples/counting_sort/why3session.xml
#	examples/cubic_root/why3session.xml
#	examples/cursor/why3session.xml
#	examples/decrease1/why3session.xml
#	examples/defunctionalization/why3session.xml
#	examples/dfa_example/why3session.xml
#	examples/dfs/why3session.xml
#	examples/dijkstra/why3session.xml
#	examples/division/why3session.xml
#	examples/double_wp/compiler/why3session.xml
#	examples/double_wp/logic/why3session.xml
#	examples/double_wp/specs/why3session.xml
#	examples/dyck/why3session.xml
#	examples/edit_distance/why3session.xml
#	examples/esterel/why3session.xml
#	examples/euler002/why3session.xml
#	examples/euler011/why3session.xml
#	examples/fenwick/why3session.xml
#	examples/fib_memo/why3session.xml
#	examples/fibonacci/why3session.xml
#	examples/find/why3session.xml
#	examples/finger_trees/why3session.xml
#	examples/flag/why3session.xml
#	examples/flag2/why3session.xml
#	examples/foveoos11_challenge1/why3session.xml
#	examples/foveoos11_challenge3/why3session.xml
#	examples/gcd/why3session.xml
#	examples/gcd_bezout/why3session.xml
#	examples/generate_all_trees/why3session.xml
#	examples/hackers-delight/why3session.xml
#	examples/hashtbl_impl/why3session.xml
#	examples/in_progress/2wp_gen/base/why3session.xml
#	examples/in_progress/2wp_gen/game/why3session.xml
#	examples/in_progress/2wp_gen/game_fmla/why3session.xml
#	examples/in_progress/2wp_gen/game_wp/why3session.xml
#	examples/in_progress/2wp_gen/order/why3session.xml
#	examples/in_progress/2wp_gen/transfinite/why3session.xml
#	examples/in_progress/2wp_gen/transition/why3session.xml
#	examples/in_progress/2wp_gen/zorn/why3session.xml
#	examples/in_progress/koda_ruskey/why3session.xml
#	examples/in_progress/mp/why3session.xml
#	examples/insertion_sort/why3session.xml
#	examples/insertion_sort_list/why3session.xml
#	examples/insertion_sort_naive/why3session.xml
#	examples/inverse_in_place/why3session.xml
#	examples/isqrt/why3session.xml
#	examples/isqrt_von_neumann/why3session.xml
#	examples/kmp/why3session.xml
#	examples/knuth_prime_numbers/why3session.xml
#	examples/koda_ruskey/why3session.xml
#	examples/largest_prime_factor/why3session.xml
#	examples/lcp/why3session.xml
#	examples/leftist_heap/why3session.xml
#	examples/linear_probing/why3session.xml
#	examples/linked_list_rev/why3session.xml
#	examples/logic/hello_proof/why3session.xml
#	examples/max_matrix/why3session.xml
#	examples/maximum_subarray/why3session.xml
#	examples/mccarthy/why3session.xml
#	examples/mergesort_array/why3session.xml
#	examples/mergesort_list/why3session.xml
#	examples/mergesort_queue/why3session.xml
#	examples/mjrty/why3session.xml
#	examples/muller/why3session.xml
#	examples/my_cosine/why3session.xml
#	examples/optimal_replay/why3session.xml
#	examples/patience/why3session.xml
#	examples/pigeonhole/why3session.xml
#	examples/power/why3session.xml
#	examples/queens/why3session.xml
#	examples/queens_bv/why3session.xml
#	examples/quicksort/why3session.xml
#	examples/random_access_list/why3session.xml
#	examples/register_allocation/why3session.xml
#	examples/relabel/why3session.xml
#	examples/remove_duplicate/why3session.xml
#	examples/remove_duplicate_hash/why3session.xml
#	examples/residual/why3session.xml
#	examples/rightmostbittrick/why3session.xml
#	examples/ropes/why3session.xml
#	examples/same_fringe/why3session.xml
#	examples/schorr_waite/why3session.xml
#	examples/schorr_waite_via_recursion/why3session.xml
#	examples/selection_sort/why3session.xml
#	examples/sf/why3session.xml
#	examples/sieve/why3session.xml
#	examples/skew_heaps/why3session.xml
#	examples/snapshotable_trees/why3session.xml
#	examples/stdlib/array/why3session.xml
#	examples/stdlib/list/why3session.xml
#	examples/sudoku/why3session.xml
#	examples/sum_of_digits/why3session.xml
#	examples/sumrange/why3session.xml
#	examples/tests-provers/ieee_float/why3session.xml
#	examples/there_and_back_again/why3session.xml
#	examples/topological_sorting/why3session.xml
#	examples/tortoise_and_hare/why3session.xml
#	examples/tower_of_hanoi/why3session.xml
#	examples/toy_compiler/why3session.xml
#	examples/tree_height/why3session.xml
#	examples/tree_of_array/why3session.xml
#	examples/tree_of_list/why3session.xml
#	examples/unraveling_a_card_trick/why3session.xml
#	examples/use_api/mlw.ml
#	examples/vacid_0_binary_heaps/proofs/why3session.xml
#	examples/vacid_0_build_maze/why3session.xml
#	examples/vacid_0_red_black_trees/why3session.xml
#	examples/vacid_0_sparse_array/why3session.xml
#	examples/verifythis_2015_dancing_links/why3session.xml
#	examples/verifythis_2015_parallel_gcd/why3session.xml
#	examples/verifythis_2015_relaxed_prefix/why3session.xml
#	examples/verifythis_2016_matrix_multiplication/matrices/why3session.xml
#	examples/verifythis_2016_matrix_multiplication/matrices_ring_simp/why3session.xml
#	examples/verifythis_2016_matrix_multiplication/naive/why3session.xml
#	examples/verifythis_2016_matrix_multiplication/strassen/why3session.xml
#	examples/verifythis_2016_matrix_multiplication/sum_extended/why3session.xml
#	examples/verifythis_2016_tree_traversal/why3session.xml
#	examples/verifythis_PrefixSumRec/why3session.xml
#	examples/verifythis_fm2012_LRS/why3session.xml
#	examples/verifythis_fm2012_treedel/why3session.xml
#	examples/vstte10_aqueue/why3session.xml
#	examples/vstte10_inverting/why3session.xml
#	examples/vstte10_max_sum/why3session.xml
#	examples/vstte10_queens/why3session.xml
#	examples/vstte10_search_list/why3session.xml
#	examples/vstte12_bfs/why3session.xml
#	examples/vstte12_combinators/why3session.xml
#	examples/vstte12_ring_buffer/why3session.xml
#	examples/vstte12_tree_reconstruction/why3session.xml
#	examples/vstte12_two_way_sort/why3session.xml
#	examples/warshall_algorithm/why3session.xml
#	examples/zeros/why3session.xml
#	src/core/pretty.ml
#	src/transform/introduction.ml
#	tests/theory-sessions/bintree/why3session.xml
#	tests/theory-sessions/hashtbl/why3session.xml
parents bb25fb15 8e560e42
......@@ -229,7 +229,7 @@ LIB_TRANSFORM = simplify_formula inlining split_goal \
intro_vc_vars_counterexmp prepare_for_counterexmp \
instantiate_predicate smoke_detector \
prop_curry eliminate_literal \
generic_arg_trans_utils case apply \
generic_arg_trans_utils case apply subst \
ind_itp destruct cut \
induction induction_pr matching reflection
......
......@@ -6,7 +6,7 @@
<file name="../jlamp0.mlw">
<theory name="M">
<goal name="WP_parameter p1" expl="VC for p1">
<transf name="split_intros_goal_wp" >
<transf name="split_vc" >
<goal name="WP_parameter p1.0" expl="assertion">
<proof prover="0"><result status="unknown" time="0.01"/></proof>
</goal>
......@@ -19,7 +19,7 @@
</transf>
</goal>
<goal name="WP_parameter p2" expl="VC for p2">
<transf name="split_intros_goal_wp" >
<transf name="split_vc" >
<goal name="WP_parameter p2.0" expl="loop invariant init">
<proof prover="0"><result status="unknown" time="0.00"/></proof>
</goal>
......
......@@ -89,7 +89,7 @@
<goal name="eval_type_term" proved="true">
<transf name="induction_ty_lex" proved="true" >
<goal name="eval_type_term.0" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="eval_type_term.0.0" proved="true">
<proof prover="0"><result status="valid" time="0.06" steps="281"/></proof>
</goal>
......@@ -145,7 +145,7 @@
<goal name="eval_msubst_term" proved="true">
<transf name="induction_ty_lex" proved="true" >
<goal name="eval_msubst_term.0" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="eval_msubst_term.0.0" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="12"/></proof>
</goal>
......@@ -165,7 +165,7 @@
<goal name="eval_msubst" proved="true">
<transf name="induction_ty_lex" proved="true" >
<goal name="eval_msubst.0" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="eval_msubst.0.0" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="34"/></proof>
</goal>
......@@ -209,7 +209,7 @@
<goal name="eval_swap_term" proved="true">
<transf name="induction_ty_lex" proved="true" >
<goal name="eval_swap_term.0" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="eval_swap_term.0.0" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
......@@ -237,7 +237,7 @@
<goal name="eval_swap_gen" proved="true">
<transf name="induction_ty_lex" proved="true" >
<goal name="eval_swap_gen.0" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="eval_swap_gen.0.0" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="48"/></proof>
</goal>
......@@ -284,7 +284,7 @@
<goal name="eval_term_change_free" proved="true">
<transf name="induction_ty_lex" proved="true" >
<goal name="eval_term_change_free.0" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="eval_term_change_free.0.0" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="6"/></proof>
</goal>
......@@ -304,7 +304,7 @@
<goal name="eval_change_free" proved="true">
<transf name="induction_ty_lex" proved="true" >
<goal name="eval_change_free.0" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="eval_change_free.0.0" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="37"/></proof>
</goal>
......@@ -489,7 +489,7 @@
<goal name="monotonicity" proved="true">
<transf name="induction_ty_lex" proved="true" >
<goal name="monotonicity.0" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="monotonicity.0.0" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="11"/></proof>
</goal>
......@@ -551,7 +551,7 @@
<goal name="distrib_conj" proved="true">
<transf name="induction_ty_lex" proved="true" >
<goal name="distrib_conj.0" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="distrib_conj.0.0" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="28"/></proof>
</goal>
......@@ -620,7 +620,7 @@
<goal name="progress" proved="true">
<transf name="induction_ty_lex" proved="true" >
<goal name="progress.0" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="progress.0.0" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="11"/></proof>
</goal>
......
......@@ -155,7 +155,7 @@
<proof prover="6"><result status="valid" time="0.02" steps="6"/></proof>
</goal>
<goal name="VC compute_writes" expl="VC for compute_writes" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC compute_writes.0" expl="variant decrease" proved="true">
<proof prover="6"><result status="valid" time="0.04" steps="44"/></proof>
</goal>
......@@ -172,7 +172,7 @@
<proof prover="6"><result status="valid" time="0.04" steps="49"/></proof>
</goal>
<goal name="VC compute_writes.5" expl="postcondition" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC compute_writes.5.0" expl="postcondition" proved="true">
<proof prover="10"><result status="valid" time="0.04"/></proof>
</goal>
......@@ -196,7 +196,7 @@
</transf>
</goal>
<goal name="VC wp" expl="VC for wp" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC wp.0" expl="variant decrease" proved="true">
<proof prover="6"><result status="valid" time="0.04" steps="44"/></proof>
</goal>
......@@ -213,7 +213,7 @@
<proof prover="6"><result status="valid" time="0.04" steps="49"/></proof>
</goal>
<goal name="VC wp.5" expl="postcondition" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC wp.5.0" expl="postcondition" proved="true">
<proof prover="6"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
......
......@@ -9,7 +9,7 @@
<proof prover="2"><result status="valid" time="0.03" steps="62"/></proof>
</goal>
<goal name="VC partition_" expl="VC for partition_" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC partition_.0" expl="index in array bounds" proved="true">
<proof prover="2"><result status="valid" time="0.00" steps="6"/></proof>
</goal>
......
......@@ -6,7 +6,7 @@
<file name="../algo63.mlw" proved="true">
<theory name="Algo63" proved="true">
<goal name="VC exchange" expl="VC for exchange" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC exchange.0" expl="index in array bounds" proved="true">
<proof prover="3"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
......@@ -31,7 +31,7 @@
</transf>
</goal>
<goal name="VC partition_" expl="VC for partition_" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC partition_.0" expl="index in array bounds" proved="true">
<proof prover="3"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
......@@ -206,7 +206,7 @@
</transf>
</goal>
<goal name="VC partition" expl="VC for partition" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC partition.0" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
......
......@@ -41,7 +41,7 @@
<proof prover="0"><result status="valid" time="0.01" steps="56"/></proof>
</goal>
<goal name="rotation_preserve_model" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="rotation_preserve_model.0" proved="true">
<proof prover="0"><result status="valid" time="0.04" steps="90"/></proof>
</goal>
......@@ -75,7 +75,7 @@
<proof prover="0"><result status="valid" time="0.15" steps="649"/></proof>
</goal>
<goal name="VC balance" expl="VC for balance" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC balance.0" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="26"/></proof>
</goal>
......@@ -128,7 +128,7 @@
<proof prover="0"><result status="valid" time="0.67" steps="3086"/></proof>
</goal>
<goal name="VC balance.17" expl="postcondition" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC balance.17.0" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.59" steps="2454"/></proof>
</goal>
......@@ -167,7 +167,7 @@
<proof prover="0"><result status="valid" time="0.07" steps="290"/></proof>
</goal>
<goal name="VC fuse" expl="VC for fuse" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC fuse.0" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.06" steps="179"/></proof>
</goal>
......@@ -178,7 +178,7 @@
<proof prover="0"><result status="valid" time="0.14" steps="295"/></proof>
</goal>
<goal name="VC fuse.3" expl="postcondition" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC fuse.3.0" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.65" steps="2230"/></proof>
</goal>
......@@ -196,7 +196,7 @@
<proof prover="0"><result status="valid" time="0.55" steps="1931"/></proof>
</goal>
<goal name="VC join" expl="VC for join" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC join.0" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.20" steps="586"/></proof>
</goal>
......@@ -230,7 +230,7 @@
<proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
<goal name="VC insert" expl="VC for insert" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC insert.0" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="37"/></proof>
</goal>
......@@ -297,7 +297,7 @@
</transf>
</goal>
<goal name="VC remove" expl="VC for remove" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC remove.0" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="22"/></proof>
</goal>
......@@ -367,7 +367,7 @@
<proof prover="0"><result status="valid" time="0.60" steps="3195"/></proof>
</goal>
<goal name="VC extract" expl="VC for extract" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC extract.0" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.07" steps="130"/></proof>
</goal>
......@@ -422,7 +422,7 @@
</transf>
</goal>
<goal name="VC split" expl="VC for split" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC split.0" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.05" steps="130"/></proof>
</goal>
......
......@@ -12,7 +12,7 @@
<proof prover="0"><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_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC assoc_m.0" expl="assertion" proved="true">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
......@@ -35,7 +35,7 @@
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC assoc_m.7" expl="postcondition" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC assoc_m.7.0" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
......@@ -83,7 +83,7 @@
<proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
<goal name="M.VC op" expl="VC for op" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC op.0" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="7"/></proof>
</goal>
......@@ -99,7 +99,7 @@
<proof prover="0"><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_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC monoid_sum_is_min.0" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
......@@ -113,7 +113,7 @@
<proof prover="0"><result status="valid" time="0.02" steps="41"/></proof>
</goal>
<goal name="VC monoid_sum_is_min.4" expl="postcondition" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC monoid_sum_is_min.4.0" expl="VC for monoid_sum_is_min" proved="true">
<proof prover="1"><result status="valid" time="0.09"/></proof>
</goal>
......@@ -128,12 +128,12 @@
</transf>
</goal>
<goal name="VC selected_is_min" expl="VC for selected_is_min" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC selected_is_min.0" expl="unreachable point" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
<goal name="VC selected_is_min.1" expl="assertion" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC selected_is_min.1.0" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.68" steps="1664"/></proof>
</goal>
......@@ -154,9 +154,9 @@
</transf>
</goal>
<goal name="VC selected_part" expl="VC for selected_part" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC selected_part.0" expl="postcondition" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC selected_part.0.0" expl="VC for selected_part" proved="true">
<proof prover="0"><result status="valid" time="0.07" steps="79"/></proof>
</goal>
......@@ -199,7 +199,7 @@
</transf>
</goal>
<goal name="VC selected_part.1" expl="postcondition" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC selected_part.1.0" expl="VC for selected_part" proved="true">
<proof prover="0"><result status="valid" time="0.06" steps="252"/></proof>
</goal>
......@@ -242,7 +242,7 @@
</transf>
</goal>
<goal name="VC selected_part.2" expl="postcondition" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC selected_part.2.0" expl="VC for selected_part" proved="true">
<proof prover="0"><result status="valid" time="0.05" steps="192"/></proof>
</goal>
......@@ -285,7 +285,7 @@
</transf>
</goal>
<goal name="VC selected_part.3" expl="postcondition" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC selected_part.3.0" expl="VC for selected_part" proved="true">
<proof prover="0"><result status="valid" time="0.16" steps="704"/></proof>
</goal>
......@@ -308,7 +308,7 @@
<proof prover="0"><result status="valid" time="0.18" steps="518"/></proof>
</goal>
<goal name="VC selected_part.3.7" expl="VC for selected_part" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC selected_part.3.7.0" expl="VC for selected_part" proved="true">
<proof prover="0"><result status="valid" time="0.37" steps="866"/></proof>
</goal>
......@@ -373,9 +373,9 @@
<proof prover="0"><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_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC to_bag_mem.0" expl="assertion" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC to_bag_mem.0.0" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="15"/></proof>
</goal>
......@@ -396,7 +396,7 @@
</transf>
</goal>
<goal name="VC get_minimum_index" expl="VC for get_minimum_index" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC get_minimum_index.0" expl="loop invariant init" proved="true">
<proof prover="0"><result status="valid" time="0.04" steps="64"/></proof>
</goal>
......@@ -448,7 +448,7 @@
</transf>
</goal>
<goal name="VC split_gives_minimum" expl="VC for split_gives_minimum" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC split_gives_minimum.0" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="46"/></proof>
</goal>
......@@ -470,7 +470,7 @@
</transf>
</goal>
<goal name="VC correction" expl="VC for correction" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC correction.0" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="12"/></proof>
</goal>
......@@ -507,7 +507,7 @@
<proof prover="0"><result status="valid" time="0.26" steps="378"/></proof>
</goal>
<goal name="VC remove_count" expl="VC for remove_count" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC remove_count.0" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="61"/></proof>
</goal>
......@@ -520,7 +520,7 @@
</transf>
</goal>
<goal name="VC extract_min" expl="VC for extract_min" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC extract_min.0" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.04" steps="20"/></proof>
</goal>
......@@ -531,7 +531,7 @@
<proof prover="0"><result status="valid" time="0.03" steps="14"/></proof>
</goal>
<goal name="VC extract_min.3" expl="postcondition" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC extract_min.3.0" expl="VC for extract_min" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="21"/></proof>
</goal>
......@@ -555,7 +555,7 @@
</transf>
</goal>
<goal name="VC min" expl="VC for min" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC min.0" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="12"/></proof>
</goal>
......@@ -568,7 +568,7 @@
</transf>
</goal>
<goal name="VC pop_min" expl="VC for pop_min" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC pop_min.0" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="12"/></proof>
</goal>
......@@ -579,7 +579,7 @@
<proof prover="0"><result status="valid" time="0.03" steps="11"/></proof>
</goal>
<goal name="VC pop_min.3" expl="postcondition" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC pop_min.3.0" expl="VC for pop_min" proved="true">
<proof prover="0"><result status="valid" time="0.12" steps="76"/></proof>
</goal>
......@@ -594,7 +594,7 @@
</transf>
</goal>
<goal name="VC add" expl="VC for add" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC add.0" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="70"/></proof>
</goal>
......
......@@ -120,7 +120,7 @@
<proof prover="0"><result status="valid" time="0.15" steps="353"/></proof>
</goal>
<goal name="VC harness" expl="VC for harness" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC harness.0" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="6"/></proof>
</goal>
......
......@@ -37,7 +37,7 @@
<proof prover="1"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
<goal name="VC selected_part" expl="VC for selected_part" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC selected_part.0" expl="assertion" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="25"/></proof>
</goal>
......@@ -45,7 +45,7 @@
<proof prover="1"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="VC selected_part.2" expl="postcondition" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC selected_part.2.0" expl="VC for selected_part" proved="true">
<proof prover="1"><result status="valid" time="0.12" steps="490"/></proof>
</goal>
......@@ -53,7 +53,7 @@
<proof prover="1"><result status="valid" time="0.02" steps="44"/></proof>
</goal>
<goal name="VC selected_part.2.2" expl="VC for selected_part" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC selected_part.2.2.0" expl="VC for selected_part" proved="true">
<proof prover="1" timelimit="5"><result status="valid" time="1.86" steps="2859"/></proof>
</goal>
......@@ -118,9 +118,9 @@
<proof prover="1"><result status="valid" time="0.03" steps="167"/></proof>
</goal>
<goal name="VC selected_model" expl="VC for selected_model" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC selected_model.0" expl="postcondition" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC selected_model.0.0" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.22" steps="553"/></proof>
</goal>
......@@ -165,9 +165,9 @@
</transf>
</goal>
<goal name="VC selected_sorted" expl="VC for selected_sorted" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC selected_sorted.0" expl="postcondition" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC selected_sorted.0.0" expl="VC for selected_sorted" proved="true">
<proof prover="1"><result status="valid" time="1.06" steps="1512"/></proof>
</goal>
......@@ -215,7 +215,7 @@
<proof prover="1"><result status="valid" time="0.24" steps="518"/></proof>
</goal>
<goal name="VC insert" expl="VC for insert" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC insert.0" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="16"/></proof>
</goal>
......@@ -247,7 +247,7 @@
<proof prover="1"><result status="valid" time="0.05" steps="20"/></proof>
</goal>
<goal name="VC insert.10" expl="postcondition" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC insert.10.0" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.47" steps="1457"/></proof>
</goal>
......@@ -262,7 +262,7 @@
</transf>
</goal>
<goal name="VC remove" expl="VC for remove" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC remove.0" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="16"/></proof>
</goal>
......@@ -287,7 +287,7 @@
</transf>
</goal>
<goal name="VC split" expl="VC for split" proved="true">
<transf name="split_goal_wp" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC split.0" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="16"/></proof>
</goal>
......@@ -298,7 +298,7 @@
<proof prover="1"><result status="valid" time="0.07" steps="157"/></proof>