From 035ba52ec4a8c8cd24a2eb8867ac4e3f5ca9155e Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 4 Apr 2018 11:49:01 +0200 Subject: [PATCH] Clean some session files. --- .../blocking_semantics5/why3session.xml | 2 - examples/WP_revisited/formula/why3session.xml | 8 +- examples/WP_revisited/imp_n/why3session.xml | 2 +- examples/add_list/why3session.xml | 16 +- examples/add_list_vc_sp/why3session.xml | 6 +- examples/all_distinct/why3session.xml | 2 +- examples/arm/why3session.xml | 6 +- .../why3session.xml | 4 +- examples/avl/avl/why3session.xml | 4 +- examples/avl/key_type/why3session.xml | 4 +- examples/avl/monoid/why3session.xml | 8 +- examples/avl/preorder/why3session.xml | 22 +- examples/avl/priority_queue/why3session.xml | 2 +- examples/avl/ral/why3session.xml | 106 ++--- examples/balance/why3session.xml | 6 +- .../binary_multiplication/why3session.xml | 6 +- examples/bitvector_examples/why3session.xml | 10 +- examples/bitvectors/bitvector/why3session.xml | 8 +- examples/braun_trees/why3session.xml | 2 +- examples/bresenham/why3session.xml | 2 +- examples/bts/12934/why3session.xml | 6 +- examples/bts/13849/why3session.xml | 6 +- examples/bts/13853/why3session.xml | 8 +- examples/bts/13854/why3session.xml | 8 +- examples/bts/16972/why3session.xml | 6 +- examples/bts/19_apply_with/why3session.xml | 6 +- .../bts/71_disambiguation/why3session.xml | 8 +- .../bts/79_compute_unsound/why3session.xml | 2 +- examples/bts/fsetint/why3session.xml | 18 +- examples/check-builtin/ac/why3session.xml | 8 +- examples/check-builtin/array/why3session.xml | 12 +- examples/check-builtin/bool/why3session.xml | 10 +- .../euclideandivision/why3session.xml | 8 +- examples/check-builtin/int/why3session.xml | 42 +- examples/check-builtin/minmax/why3session.xml | 8 +- .../propositional/why3session.xml | 6 +- .../checking_a_large_routine/why3session.xml | 8 +- examples/coincidence_count/why3session.xml | 2 +- examples/conjugate/why3session.xml | 4 +- examples/counting_sort/why3session.xml | 8 +- examples/cubic_root/why3session.xml | 24 +- examples/decrease1/why3session.xml | 2 +- examples/dfa_example/why3session.xml | 2 +- examples/division/why3session.xml | 6 +- examples/double_wp/compiler/why3session.xml | 6 +- examples/double_wp/logic/why3session.xml | 2 +- examples/double_wp/state/why3session.xml | 4 +- examples/dyck/why3session.xml | 4 +- examples/edit_distance/why3session.xml | 4 +- examples/esterel/why3session.xml | 2 +- examples/euler001/why3session.xml | 8 +- examples/euler011/why3session.xml | 2 +- examples/ewd673/why3session.xml | 6 +- examples/fact/why3session.xml | 26 +- examples/fact_vc_sp/why3session.xml | 4 +- examples/fenwick/why3session.xml | 2 +- examples/fib_memo/why3session.xml | 8 +- examples/fibonacci/why3session.xml | 150 +++---- examples/fill/why3session.xml | 2 +- examples/finger_trees/why3session.xml | 10 +- examples/flag2/why3session.xml | 2 +- .../foveoos11-cm/array_max/why3session.xml | 2 +- examples/foveoos11-cm/duplets/why3session.xml | 2 +- .../foveoos11-cm/tree_max/why3session.xml | 12 +- examples/foveoos11_challenge1/why3session.xml | 2 +- examples/foveoos11_challenge2/why3session.xml | 2 +- examples/gcd_bezout_vc_sp/why3session.xml | 2 +- examples/hashtbl_impl/why3session.xml | 2 +- examples/insertion_sort_list/why3session.xml | 4 +- examples/inverse_in_place/why3session.xml | 4 +- examples/knuth_prime_numbers/why3session.xml | 2 +- examples/lcp/why3session.xml | 2 +- examples/logic/First/why3session.xml | 8 +- examples/logic/agatha/why3session.xml | 12 +- examples/logic/bitvectors/why3session.xml | 16 +- examples/logic/distr/why3session.xml | 8 +- examples/logic/einstein/why3session.xml | 28 +- examples/logic/ffx/why3session.xml | 10 +- examples/logic/hello_proof/why3session.xml | 16 +- .../logic/lagrange_inequality/why3session.xml | 26 +- examples/logic/los_problem/why3session.xml | 6 +- examples/logic/real/why3session.xml | 2 +- .../scottish-private-club/why3session.xml | 6 +- examples/logic/simple/why3session.xml | 6 +- examples/logic/sorted_list/why3session.xml | 4 +- .../logic/triangle_inequality/why3session.xml | 4 +- examples/mjrty/why3session.xml | 2 +- examples/muller/why3session.xml | 2 +- examples/optimal_replay/why3session.xml | 2 +- examples/power_vc_sp/why3session.xml | 2 +- examples/remove_duplicate/why3session.xml | 2 +- .../remove_duplicate_hash/why3session.xml | 2 +- examples/residual/why3session.xml | 4 +- examples/resizable_array/why3session.xml | 4 +- examples/rightmostbittrick/why3session.xml | 2 +- examples/ropes/why3session.xml | 6 +- examples/same_fringe/why3session.xml | 42 +- examples/sorted_list/why3session.xml | 8 +- examples/swap/why3session.xml | 4 +- examples/tests-provers/bv/why3session.xml | 408 +++++++++--------- .../coq-interval/why3session.xml | 2 +- examples/tests-provers/coq/why3session.xml | 6 +- examples/tests-provers/cvc3/why3session.xml | 10 +- examples/tests-provers/div/why3session.xml | 186 ++++---- .../tests-provers/div_real/why3session.xml | 50 +-- .../tests-provers/ieee_float/why3session.xml | 42 +- .../tests-provers/metitarski/why3session.xml | 2 +- examples/there_and_back_again/why3session.xml | 4 +- examples/tortoise_and_hare/why3session.xml | 2 +- examples/tree_height/why3session.xml | 8 +- examples/tree_of_array/why3session.xml | 2 +- examples/tree_of_list/why3session.xml | 8 +- .../why3session.xml | 2 +- .../why3session.xml | 2 +- .../why3session.xml | 2 +- .../verifythis_PrefixSumRec/why3session.xml | 2 +- examples/vstte10_aqueue/why3session.xml | 16 +- examples/vstte10_search_list/why3session.xml | 2 +- examples/vstte12_combinators/why3session.xml | 2 +- examples/vstte12_ring_buffer/why3session.xml | 8 +- .../why3session.xml | 10 +- examples/warshall_algorithm/why3session.xml | 2 +- .../white_and_black_balls/why3session.xml | 6 +- examples/zeros/why3session.xml | 4 +- 124 files changed, 858 insertions(+), 886 deletions(-) diff --git a/examples/WP_revisited/blocking_semantics5/why3session.xml b/examples/WP_revisited/blocking_semantics5/why3session.xml index b83370fb1..93f91897f 100644 --- a/examples/WP_revisited/blocking_semantics5/why3session.xml +++ b/examples/WP_revisited/blocking_semantics5/why3session.xml @@ -77,8 +77,6 @@ - - diff --git a/examples/WP_revisited/formula/why3session.xml b/examples/WP_revisited/formula/why3session.xml index a6e2f94c5..351ac44b7 100644 --- a/examples/WP_revisited/formula/why3session.xml +++ b/examples/WP_revisited/formula/why3session.xml @@ -5,11 +5,9 @@ - - - - - + + + diff --git a/examples/WP_revisited/imp_n/why3session.xml b/examples/WP_revisited/imp_n/why3session.xml index d01a652d2..78cef7779 100644 --- a/examples/WP_revisited/imp_n/why3session.xml +++ b/examples/WP_revisited/imp_n/why3session.xml @@ -6,7 +6,7 @@ - + diff --git a/examples/add_list/why3session.xml b/examples/add_list/why3session.xml index 1490f7a0e..9bb19a96d 100644 --- a/examples/add_list/why3session.xml +++ b/examples/add_list/why3session.xml @@ -4,22 +4,20 @@ - - - - - + + + - + - - + + - + diff --git a/examples/add_list_vc_sp/why3session.xml b/examples/add_list_vc_sp/why3session.xml index dc9294e2f..4eec2fef4 100644 --- a/examples/add_list_vc_sp/why3session.xml +++ b/examples/add_list_vc_sp/why3session.xml @@ -4,9 +4,7 @@ - - - + @@ -14,7 +12,7 @@ - + diff --git a/examples/all_distinct/why3session.xml b/examples/all_distinct/why3session.xml index 7270b9c4f..a17fbae00 100644 --- a/examples/all_distinct/why3session.xml +++ b/examples/all_distinct/why3session.xml @@ -4,7 +4,7 @@ - + diff --git a/examples/arm/why3session.xml b/examples/arm/why3session.xml index 40304b3e1..f0564f3e2 100644 --- a/examples/arm/why3session.xml +++ b/examples/arm/why3session.xml @@ -4,14 +4,12 @@ - + - - - + diff --git a/examples/assigning_meanings_to_programs/why3session.xml b/examples/assigning_meanings_to_programs/why3session.xml index 92f1e091e..65085708e 100644 --- a/examples/assigning_meanings_to_programs/why3session.xml +++ b/examples/assigning_meanings_to_programs/why3session.xml @@ -4,12 +4,12 @@ - + - + diff --git a/examples/avl/avl/why3session.xml b/examples/avl/avl/why3session.xml index fbf73169c..a951eef05 100644 --- a/examples/avl/avl/why3session.xml +++ b/examples/avl/avl/why3session.xml @@ -4,7 +4,7 @@ - + @@ -18,7 +18,7 @@ - + diff --git a/examples/avl/key_type/why3session.xml b/examples/avl/key_type/why3session.xml index 3db4ff18e..5eee48095 100644 --- a/examples/avl/key_type/why3session.xml +++ b/examples/avl/key_type/why3session.xml @@ -2,8 +2,6 @@ - - - + diff --git a/examples/avl/monoid/why3session.xml b/examples/avl/monoid/why3session.xml index 47b2bfd9a..052f6739e 100644 --- a/examples/avl/monoid/why3session.xml +++ b/examples/avl/monoid/why3session.xml @@ -5,11 +5,7 @@ - - - - - + @@ -35,7 +31,5 @@ - - diff --git a/examples/avl/preorder/why3session.xml b/examples/avl/preorder/why3session.xml index 2bc22a66b..94b7541ba 100644 --- a/examples/avl/preorder/why3session.xml +++ b/examples/avl/preorder/why3session.xml @@ -3,33 +3,31 @@ "http://why3.lri.fr/why3session.dtd"> - - - + + + - + - + - + - + - - + + - + - - diff --git a/examples/avl/priority_queue/why3session.xml b/examples/avl/priority_queue/why3session.xml index 886deae7e..f6dd1625a 100644 --- a/examples/avl/priority_queue/why3session.xml +++ b/examples/avl/priority_queue/why3session.xml @@ -7,7 +7,7 @@ - + diff --git a/examples/avl/ral/why3session.xml b/examples/avl/ral/why3session.xml index b9abfaa08..a3b197533 100644 --- a/examples/avl/ral/why3session.xml +++ b/examples/avl/ral/why3session.xml @@ -3,157 +3,157 @@ "http://why3.lri.fr/why3session.dtd"> - - - + + + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - - - + + + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/balance/why3session.xml b/examples/balance/why3session.xml index ff29da7ea..79c54fead 100644 --- a/examples/balance/why3session.xml +++ b/examples/balance/why3session.xml @@ -4,9 +4,7 @@ - - - + @@ -14,7 +12,7 @@ - + diff --git a/examples/binary_multiplication/why3session.xml b/examples/binary_multiplication/why3session.xml index 819d0285e..2ed982403 100644 --- a/examples/binary_multiplication/why3session.xml +++ b/examples/binary_multiplication/why3session.xml @@ -3,9 +3,9 @@ "http://why3.lri.fr/why3session.dtd"> - - - + + + diff --git a/examples/bitvector_examples/why3session.xml b/examples/bitvector_examples/why3session.xml index 7177e0676..0781203e3 100644 --- a/examples/bitvector_examples/why3session.xml +++ b/examples/bitvector_examples/why3session.xml @@ -5,7 +5,7 @@ - + @@ -19,7 +19,7 @@ - + @@ -78,7 +78,7 @@ - + @@ -140,7 +140,7 @@ - + @@ -191,7 +191,7 @@ - + diff --git a/examples/bitvectors/bitvector/why3session.xml b/examples/bitvectors/bitvector/why3session.xml index cef9c0ff7..92fa0abe6 100644 --- a/examples/bitvectors/bitvector/why3session.xml +++ b/examples/bitvectors/bitvector/why3session.xml @@ -10,7 +10,7 @@ - + @@ -77,19 +77,19 @@ - + - + - + diff --git a/examples/braun_trees/why3session.xml b/examples/braun_trees/why3session.xml index f54b03fc0..925610dc3 100644 --- a/examples/braun_trees/why3session.xml +++ b/examples/braun_trees/why3session.xml @@ -5,7 +5,7 @@ - + diff --git a/examples/bresenham/why3session.xml b/examples/bresenham/why3session.xml index 827fabc22..6a247198e 100644 --- a/examples/bresenham/why3session.xml +++ b/examples/bresenham/why3session.xml @@ -5,7 +5,7 @@ - + diff --git a/examples/bts/12934/why3session.xml b/examples/bts/12934/why3session.xml index dff7f0f05..e7a4b3030 100644 --- a/examples/bts/12934/why3session.xml +++ b/examples/bts/12934/why3session.xml @@ -3,9 +3,9 @@ "http://why3.lri.fr/why3session.dtd"> - - - + + + diff --git a/examples/bts/13849/why3session.xml b/examples/bts/13849/why3session.xml index e3825d05e..96a10ea79 100644 --- a/examples/bts/13849/why3session.xml +++ b/examples/bts/13849/why3session.xml @@ -3,9 +3,9 @@ "http://why3.lri.fr/why3session.dtd"> - - - + + + diff --git a/examples/bts/13853/why3session.xml b/examples/bts/13853/why3session.xml index 292e475b7..d9c7f2281 100644 --- a/examples/bts/13853/why3session.xml +++ b/examples/bts/13853/why3session.xml @@ -3,12 +3,12 @@ "http://why3.lri.fr/why3session.dtd"> - - - + + + - + diff --git a/examples/bts/13854/why3session.xml b/examples/bts/13854/why3session.xml index 4295bd12f..ae1bc8b77 100644 --- a/examples/bts/13854/why3session.xml +++ b/examples/bts/13854/why3session.xml @@ -3,12 +3,12 @@ "http://why3.lri.fr/why3session.dtd"> - - - + + + - + diff --git a/examples/bts/16972/why3session.xml b/examples/bts/16972/why3session.xml index b5ac657ba..f7e03484b 100644 --- a/examples/bts/16972/why3session.xml +++ b/examples/bts/16972/why3session.xml @@ -3,9 +3,9 @@ "http://why3.lri.fr/why3session.dtd"> - - - + + + diff --git a/examples/bts/19_apply_with/why3session.xml b/examples/bts/19_apply_with/why3session.xml index 70dd60b0b..9ad03aa21 100644 --- a/examples/bts/19_apply_with/why3session.xml +++ b/examples/bts/19_apply_with/why3session.xml @@ -3,7 +3,7 @@ "http://why3.lri.fr/why3session.dtd"> - + @@ -13,7 +13,7 @@ - + @@ -23,7 +23,7 @@ - + diff --git a/examples/bts/71_disambiguation/why3session.xml b/examples/bts/71_disambiguation/why3session.xml index a4a28b9ec..4ffe91908 100644 --- a/examples/bts/71_disambiguation/why3session.xml +++ b/examples/bts/71_disambiguation/why3session.xml @@ -4,14 +4,14 @@ - + - + @@ -28,11 +28,11 @@ - + - + diff --git a/examples/bts/79_compute_unsound/why3session.xml b/examples/bts/79_compute_unsound/why3session.xml index 22bafe750..18b3621ca 100644 --- a/examples/bts/79_compute_unsound/why3session.xml +++ b/examples/bts/79_compute_unsound/why3session.xml @@ -4,7 +4,7 @@ - + diff --git a/examples/bts/fsetint/why3session.xml b/examples/bts/fsetint/why3session.xml index 2d592856c..b8194cf9c 100644 --- a/examples/bts/fsetint/why3session.xml +++ b/examples/bts/fsetint/why3session.xml @@ -8,9 +8,9 @@ - - - + + + @@ -19,16 +19,16 @@ - - + + - + - + @@ -37,8 +37,8 @@ - - + + diff --git a/examples/check-builtin/ac/why3session.xml b/examples/check-builtin/ac/why3session.xml index 0b42de63e..e5b227516 100644 --- a/examples/check-builtin/ac/why3session.xml +++ b/examples/check-builtin/ac/why3session.xml @@ -6,15 +6,15 @@ - - - + + + - + diff --git a/examples/check-builtin/array/why3session.xml b/examples/check-builtin/array/why3session.xml index f81bf1f39..c3b3489e6 100644 --- a/examples/check-builtin/array/why3session.xml +++ b/examples/check-builtin/array/why3session.xml @@ -7,30 +7,30 @@ - - - + + + - + - + - + diff --git a/examples/check-builtin/bool/why3session.xml b/examples/check-builtin/bool/why3session.xml index 0b070b99a..e8d4de7af 100644 --- a/examples/check-builtin/bool/why3session.xml +++ b/examples/check-builtin/bool/why3session.xml @@ -6,21 +6,21 @@ - - - + + + - + - + diff --git a/examples/check-builtin/euclideandivision/why3session.xml b/examples/check-builtin/euclideandivision/why3session.xml index d4e45976d..23b5e3848 100644 --- a/examples/check-builtin/euclideandivision/why3session.xml +++ b/examples/check-builtin/euclideandivision/why3session.xml @@ -8,9 +8,9 @@ - - - + + + @@ -18,7 +18,7 @@ - + diff --git a/examples/check-builtin/int/why3session.xml b/examples/check-builtin/int/why3session.xml index 9577bd2c0..2f43d0c13 100644 --- a/examples/check-builtin/int/why3session.xml +++ b/examples/check-builtin/int/why3session.xml @@ -9,27 +9,27 @@ - - - + + + - + - + - + - + - + @@ -38,7 +38,7 @@ - + @@ -47,7 +47,7 @@ - + @@ -56,7 +56,7 @@ - + @@ -65,7 +65,7 @@ - + @@ -74,25 +74,25 @@ - + - + - + - + - + - + @@ -102,12 +102,12 @@ - - + + - + diff --git a/examples/check-builtin/minmax/why3session.xml b/examples/check-builtin/minmax/why3session.xml index 2e163a2b0..fc700d2ff 100644 --- a/examples/check-builtin/minmax/why3session.xml +++ b/examples/check-builtin/minmax/why3session.xml @@ -6,15 +6,15 @@ - - - + + + - + diff --git a/examples/check-builtin/propositional/why3session.xml b/examples/check-builtin/propositional/why3session.xml index d5b13598d..61493eff9 100644 --- a/examples/check-builtin/propositional/why3session.xml +++ b/examples/check-builtin/propositional/why3session.xml @@ -6,9 +6,9 @@ - - - + + + diff --git a/examples/checking_a_large_routine/why3session.xml b/examples/checking_a_large_routine/why3session.xml index b3edb4937..cccb170a2 100644 --- a/examples/checking_a_large_routine/why3session.xml +++ b/examples/checking_a_large_routine/why3session.xml @@ -3,12 +3,12 @@ "http://why3.lri.fr/why3session.dtd"> - - - + + + - + diff --git a/examples/coincidence_count/why3session.xml b/examples/coincidence_count/why3session.xml index 1f99cacb6..fa5c53826 100644 --- a/examples/coincidence_count/why3session.xml +++ b/examples/coincidence_count/why3session.xml @@ -6,7 +6,7 @@ - + diff --git a/examples/conjugate/why3session.xml b/examples/conjugate/why3session.xml index aecf2b750..9908d8978 100644 --- a/examples/conjugate/why3session.xml +++ b/examples/conjugate/why3session.xml @@ -4,12 +4,12 @@ - + - + diff --git a/examples/counting_sort/why3session.xml b/examples/counting_sort/why3session.xml index 45e8a667f..b2108206b 100644 --- a/examples/counting_sort/why3session.xml +++ b/examples/counting_sort/why3session.xml @@ -6,7 +6,7 @@ - + @@ -14,7 +14,7 @@ - + @@ -113,7 +113,7 @@ - + @@ -215,7 +215,7 @@ - + diff --git a/examples/cubic_root/why3session.xml b/examples/cubic_root/why3session.xml index 011dcc6a8..7780a3806 100644 --- a/examples/cubic_root/why3session.xml +++ b/examples/cubic_root/why3session.xml @@ -3,32 +3,32 @@ "http://why3.lri.fr/why3session.dtd"> - - - - - + + + + + - + - + - + - + - + - + - + diff --git a/examples/decrease1/why3session.xml b/examples/decrease1/why3session.xml index 046ba1806..f9f76abe1 100644 --- a/examples/decrease1/why3session.xml +++ b/examples/decrease1/why3session.xml @@ -5,7 +5,7 @@ - + diff --git a/examples/dfa_example/why3session.xml b/examples/dfa_example/why3session.xml index 738139ba6..9d9723db4 100644 --- a/examples/dfa_example/why3session.xml +++ b/examples/dfa_example/why3session.xml @@ -10,7 +10,7 @@ - + diff --git a/examples/division/why3session.xml b/examples/division/why3session.xml index 934491aa0..82d968174 100644 --- a/examples/division/why3session.xml +++ b/examples/division/why3session.xml @@ -3,9 +3,9 @@ "http://why3.lri.fr/why3session.dtd"> - - - + + + diff --git a/examples/double_wp/compiler/why3session.xml b/examples/double_wp/compiler/why3session.xml index 84a0d2d33..7eb777046 100644 --- a/examples/double_wp/compiler/why3session.xml +++ b/examples/double_wp/compiler/why3session.xml @@ -5,7 +5,7 @@ - + @@ -117,7 +117,7 @@ - + @@ -330,7 +330,7 @@ - + diff --git a/examples/double_wp/logic/why3session.xml b/examples/double_wp/logic/why3session.xml index c36051edf..dfbd24bfd 100644 --- a/examples/double_wp/logic/why3session.xml +++ b/examples/double_wp/logic/why3session.xml @@ -6,7 +6,7 @@ - + diff --git a/examples/double_wp/state/why3session.xml b/examples/double_wp/state/why3session.xml index 1a85ba367..5511aedf2 100644 --- a/examples/double_wp/state/why3session.xml +++ b/examples/double_wp/state/why3session.xml @@ -2,8 +2,6 @@ - - - + diff --git a/examples/dyck/why3session.xml b/examples/dyck/why3session.xml index 88ba08062..dd6c85dde 100644 --- a/examples/dyck/why3session.xml +++ b/examples/dyck/why3session.xml @@ -7,12 +7,12 @@ - + - + diff --git a/examples/edit_distance/why3session.xml b/examples/edit_distance/why3session.xml index a2b7bf79f..27ac0c77e 100644 --- a/examples/edit_distance/why3session.xml +++ b/examples/edit_distance/why3session.xml @@ -8,7 +8,7 @@ - + @@ -123,7 +123,7 @@ - + diff --git a/examples/esterel/why3session.xml b/examples/esterel/why3session.xml index 9681ec145..e17ce5cd6 100644 --- a/examples/esterel/why3session.xml +++ b/examples/esterel/why3session.xml @@ -7,7 +7,7 @@ - + diff --git a/examples/euler001/why3session.xml b/examples/euler001/why3session.xml index fa542cb8d..254245abb 100644 --- a/examples/euler001/why3session.xml +++ b/examples/euler001/why3session.xml @@ -7,7 +7,7 @@ - + @@ -58,7 +58,7 @@ - + @@ -70,7 +70,7 @@ - + @@ -114,7 +114,7 @@ - + diff --git a/examples/euler011/why3session.xml b/examples/euler011/why3session.xml index 985a74701..7118ba034 100644 --- a/examples/euler011/why3session.xml +++ b/examples/euler011/why3session.xml @@ -6,7 +6,7 @@ - + diff --git a/examples/ewd673/why3session.xml b/examples/ewd673/why3session.xml index e7d5f927a..5535a9e85 100644 --- a/examples/ewd673/why3session.xml +++ b/examples/ewd673/why3session.xml @@ -3,9 +3,9 @@ "http://why3.lri.fr/why3session.dtd"> - - - + + + diff --git a/examples/fact/why3session.xml b/examples/fact/why3session.xml index 6be6e5b58..2df02a1fe 100644 --- a/examples/fact/why3session.xml +++ b/examples/fact/why3session.xml @@ -3,38 +3,38 @@ "http://why3.lri.fr/why3session.dtd"> - - - + + + - + - + - + - + - - + + - + - + - + - + diff --git a/examples/fact_vc_sp/why3session.xml b/examples/fact_vc_sp/why3session.xml index bdaa88376..ae0a282f0 100644 --- a/examples/fact_vc_sp/why3session.xml +++ b/examples/fact_vc_sp/why3session.xml @@ -4,7 +4,7 @@ - + @@ -21,7 +21,7 @@ - + diff --git a/examples/fenwick/why3session.xml b/examples/fenwick/why3session.xml index 4d07a953f..5db984969 100644 --- a/examples/fenwick/why3session.xml +++ b/examples/fenwick/why3session.xml @@ -4,7 +4,7 @@ - + diff --git a/examples/fib_memo/why3session.xml b/examples/fib_memo/why3session.xml index 2f25781a1..fc164dcce 100644 --- a/examples/fib_memo/why3session.xml +++ b/examples/fib_memo/why3session.xml @@ -3,12 +3,12 @@ "http://why3.lri.fr/why3session.dtd"> - - - + + + - + diff --git a/examples/fibonacci/why3session.xml b/examples/fibonacci/why3session.xml index aa852838e..1ffa3103c 100644 --- a/examples/fibonacci/why3session.xml +++ b/examples/fibonacci/why3session.xml @@ -6,218 +6,218 @@ - - - + + + - + - + - - + + - - + + - + - + - + - - + + - + - - + + - - + + - + - + - + - + - - - + + + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - - + + - + - + - - + + - - - + + + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/fill/why3session.xml b/examples/fill/why3session.xml index aa248fb14..8c940f963 100644 --- a/examples/fill/why3session.xml +++ b/examples/fill/why3session.xml @@ -4,7 +4,7 @@ - + diff --git a/examples/finger_trees/why3session.xml b/examples/finger_trees/why3session.xml index dd4b45fe7..2692fdb7c 100644 --- a/examples/finger_trees/why3session.xml +++ b/examples/finger_trees/why3session.xml @@ -3,15 +3,15 @@ "http://why3.lri.fr/why3session.dtd"> - - - + + + - + - + diff --git a/examples/flag2/why3session.xml b/examples/flag2/why3session.xml index bb53b77fd..7bc45998e 100644 --- a/examples/flag2/why3session.xml +++ b/examples/flag2/why3session.xml @@ -4,7 +4,7 @@ - + diff --git a/examples/foveoos11-cm/array_max/why3session.xml b/examples/foveoos11-cm/array_max/why3session.xml index 4567eca0e..90b35c6fb 100644 --- a/examples/foveoos11-cm/array_max/why3session.xml +++ b/examples/foveoos11-cm/array_max/why3session.xml @@ -6,7 +6,7 @@ - + diff --git a/examples/foveoos11-cm/duplets/why3session.xml b/examples/foveoos11-cm/duplets/why3session.xml index 6569c55ce..87f805ad2 100644 --- a/examples/foveoos11-cm/duplets/why3session.xml +++ b/examples/foveoos11-cm/duplets/why3session.xml @@ -4,7 +4,7 @@ - + diff --git a/examples/foveoos11-cm/tree_max/why3session.xml b/examples/foveoos11-cm/tree_max/why3session.xml index 976c30593..1065b4e79 100644 --- a/examples/foveoos11-cm/tree_max/why3session.xml +++ b/examples/foveoos11-cm/tree_max/why3session.xml @@ -4,17 +4,17 @@ - - - + + + - - + + - + diff --git a/examples/foveoos11_challenge1/why3session.xml b/examples/foveoos11_challenge1/why3session.xml index 0eb5fa412..50018adb9 100644 --- a/examples/foveoos11_challenge1/why3session.xml +++ b/examples/foveoos11_challenge1/why3session.xml @@ -4,7 +4,7 @@ - + diff --git a/examples/foveoos11_challenge2/why3session.xml b/examples/foveoos11_challenge2/why3session.xml index d1953976c..cef9ba128 100644 --- a/examples/foveoos11_challenge2/why3session.xml +++ b/examples/foveoos11_challenge2/why3session.xml @@ -5,7 +5,7 @@ - + diff --git a/examples/gcd_bezout_vc_sp/why3session.xml b/examples/gcd_bezout_vc_sp/why3session.xml index 59e7d777d..d9b6c8859 100644 --- a/examples/gcd_bezout_vc_sp/why3session.xml +++ b/examples/gcd_bezout_vc_sp/why3session.xml @@ -5,7 +5,7 @@ - + diff --git a/examples/hashtbl_impl/why3session.xml b/examples/hashtbl_impl/why3session.xml index d555cc4b2..4b7c3cddd 100644 --- a/examples/hashtbl_impl/why3session.xml +++ b/examples/hashtbl_impl/why3session.xml @@ -8,7 +8,7 @@ - + diff --git a/examples/insertion_sort_list/why3session.xml b/examples/insertion_sort_list/why3session.xml index 4abf8250f..fa795f235 100644 --- a/examples/insertion_sort_list/why3session.xml +++ b/examples/insertion_sort_list/why3session.xml @@ -6,8 +6,8 @@ - - + + diff --git a/examples/inverse_in_place/why3session.xml b/examples/inverse_in_place/why3session.xml index 5eb326565..58f2f4283 100644 --- a/examples/inverse_in_place/why3session.xml +++ b/examples/inverse_in_place/why3session.xml @@ -6,7 +6,7 @@ - + @@ -87,7 +87,7 @@ - + diff --git a/examples/knuth_prime_numbers/why3session.xml b/examples/knuth_prime_numbers/why3session.xml index 883b43cc0..619046600 100644 --- a/examples/knuth_prime_numbers/why3session.xml +++ b/examples/knuth_prime_numbers/why3session.xml @@ -6,7 +6,7 @@ - + diff --git a/examples/lcp/why3session.xml b/examples/lcp/why3session.xml index 5eb0352b7..816b351c7 100644 --- a/examples/lcp/why3session.xml +++ b/examples/lcp/why3session.xml @@ -4,7 +4,7 @@ - + diff --git a/examples/logic/First/why3session.xml b/examples/logic/First/why3session.xml index 584720ce6..91c86bcfd 100644 --- a/examples/logic/First/why3session.xml +++ b/examples/logic/First/why3session.xml @@ -13,9 +13,9 @@ - - - + + + @@ -26,7 +26,7 @@ - + diff --git a/examples/logic/agatha/why3session.xml b/examples/logic/agatha/why3session.xml index 8edaef35a..e623681e8 100644 --- a/examples/logic/agatha/why3session.xml +++ b/examples/logic/agatha/why3session.xml @@ -9,9 +9,9 @@ - - - + + + @@ -20,7 +20,7 @@ - + @@ -29,7 +29,7 @@ - + @@ -38,7 +38,7 @@ - + diff --git a/examples/logic/bitvectors/why3session.xml b/examples/logic/bitvectors/why3session.xml index 6c1922aed..db5a0987c 100644 --- a/examples/logic/bitvectors/why3session.xml +++ b/examples/logic/bitvectors/why3session.xml @@ -6,7 +6,7 @@ - + @@ -42,7 +42,7 @@ - + @@ -57,7 +57,7 @@ - + @@ -72,12 +72,12 @@ - + - + @@ -110,7 +110,7 @@ - + @@ -129,7 +129,7 @@ - + @@ -141,7 +141,7 @@ - + diff --git a/examples/logic/distr/why3session.xml b/examples/logic/distr/why3session.xml index 4cfef3cab..9e3a9ee3c 100644 --- a/examples/logic/distr/why3session.xml +++ b/examples/logic/distr/why3session.xml @@ -5,14 +5,14 @@ - - - + + + - + diff --git a/examples/logic/einstein/why3session.xml b/examples/logic/einstein/why3session.xml index 1e7a89a24..92472b143 100644 --- a/examples/logic/einstein/why3session.xml +++ b/examples/logic/einstein/why3session.xml @@ -25,10 +25,6 @@ - - - - @@ -36,11 +32,11 @@ - + - - + + @@ -60,22 +56,22 @@ - + - + - - + + - + - - + + @@ -84,10 +80,10 @@ - + - + diff --git a/examples/logic/ffx/why3session.xml b/examples/logic/ffx/why3session.xml index 03923b0cf..dff267f30 100644 --- a/examples/logic/ffx/why3session.xml +++ b/examples/logic/ffx/why3session.xml @@ -21,7 +21,7 @@ - + @@ -83,7 +83,7 @@ - + @@ -100,7 +100,7 @@ - + @@ -117,7 +117,7 @@ - + @@ -137,7 +137,7 @@ - + diff --git a/examples/logic/hello_proof/why3session.xml b/examples/logic/hello_proof/why3session.xml index 7c71e5ea1..3dc6b5032 100644 --- a/examples/logic/hello_proof/why3session.xml +++ b/examples/logic/hello_proof/why3session.xml @@ -4,24 +4,24 @@ - - - + + + - + - - + + - + - + diff --git a/examples/logic/lagrange_inequality/why3session.xml b/examples/logic/lagrange_inequality/why3session.xml index 6c8e6d13c..19417a508 100644 --- a/examples/logic/lagrange_inequality/why3session.xml +++ b/examples/logic/lagrange_inequality/why3session.xml @@ -8,46 +8,46 @@ - - - + + + - + - - + + - + - + - + - - + + - + - + diff --git a/examples/logic/los_problem/why3session.xml b/examples/logic/los_problem/why3session.xml index 09a93fc27..13b53dcff 100644 --- a/examples/logic/los_problem/why3session.xml +++ b/examples/logic/los_problem/why3session.xml @@ -7,9 +7,9 @@ - - - + + + diff --git a/examples/logic/real/why3session.xml b/examples/logic/real/why3session.xml index 09c2aa3f4..19ea2096e 100644 --- a/examples/logic/real/why3session.xml +++ b/examples/logic/real/why3session.xml @@ -5,7 +5,7 @@ - + diff --git a/examples/logic/scottish-private-club/why3session.xml b/examples/logic/scottish-private-club/why3session.xml index c1f7b0270..a25a67e4f 100644 --- a/examples/logic/scottish-private-club/why3session.xml +++ b/examples/logic/scottish-private-club/why3session.xml @@ -8,9 +8,9 @@ - - - + + + diff --git a/examples/logic/simple/why3session.xml b/examples/logic/simple/why3session.xml index 538dfd233..e2dca217a 100644 --- a/examples/logic/simple/why3session.xml +++ b/examples/logic/simple/why3session.xml @@ -7,9 +7,9 @@ - - - + + + diff --git a/examples/logic/sorted_list/why3session.xml b/examples/logic/sorted_list/why3session.xml index 35134f7b1..7b402b7cd 100644 --- a/examples/logic/sorted_list/why3session.xml +++ b/examples/logic/sorted_list/why3session.xml @@ -13,7 +13,7 @@ - + @@ -21,7 +21,7 @@ - + diff --git a/examples/logic/triangle_inequality/why3session.xml b/examples/logic/triangle_inequality/why3session.xml index 97cad4425..3a9477117 100644 --- a/examples/logic/triangle_inequality/why3session.xml +++ b/examples/logic/triangle_inequality/why3session.xml @@ -11,7 +11,7 @@ - + @@ -97,7 +97,7 @@ - + diff --git a/examples/mjrty/why3session.xml b/examples/mjrty/why3session.xml index 385611402..9c9e9af4d 100644 --- a/examples/mjrty/why3session.xml +++ b/examples/mjrty/why3session.xml @@ -4,7 +4,7 @@ - + diff --git a/examples/muller/why3session.xml b/examples/muller/why3session.xml index 8f217261d..bbf6ea6ff 100644 --- a/examples/muller/why3session.xml +++ b/examples/muller/why3session.xml @@ -4,7 +4,7 @@ - + diff --git a/examples/optimal_replay/why3session.xml b/examples/optimal_replay/why3session.xml index b64cf61e1..ba060995f 100644 --- a/examples/optimal_replay/why3session.xml +++ b/examples/optimal_replay/why3session.xml @@ -9,7 +9,7 @@ - + diff --git a/examples/power_vc_sp/why3session.xml b/examples/power_vc_sp/why3session.xml index e1451ca59..59421e302 100644 --- a/examples/power_vc_sp/why3session.xml +++ b/examples/power_vc_sp/why3session.xml @@ -5,7 +5,7 @@ - + diff --git a/examples/remove_duplicate/why3session.xml b/examples/remove_duplicate/why3session.xml index d3fd3738e..da025cad4 100644 --- a/examples/remove_duplicate/why3session.xml +++ b/examples/remove_duplicate/why3session.xml @@ -7,7 +7,7 @@ - + diff --git a/examples/remove_duplicate_hash/why3session.xml b/examples/remove_duplicate_hash/why3session.xml index 8cb2665f3..0c5fcf98e 100644 --- a/examples/remove_duplicate_hash/why3session.xml +++ b/examples/remove_duplicate_hash/why3session.xml @@ -8,7 +8,7 @@ - + diff --git a/examples/residual/why3session.xml b/examples/residual/why3session.xml index 89ab2b3a0..281b3c152 100644 --- a/examples/residual/why3session.xml +++ b/examples/residual/why3session.xml @@ -8,7 +8,7 @@ - + @@ -150,7 +150,7 @@ - + diff --git a/examples/resizable_array/why3session.xml b/examples/resizable_array/why3session.xml index e69113b42..396d3869d 100644 --- a/examples/resizable_array/why3session.xml +++ b/examples/resizable_array/why3session.xml @@ -6,7 +6,7 @@ - + @@ -121,7 +121,7 @@ - + diff --git a/examples/rightmostbittrick/why3session.xml b/examples/rightmostbittrick/why3session.xml index 02778b00e..687b70f6a 100644 --- a/examples/rightmostbittrick/why3session.xml +++ b/examples/rightmostbittrick/why3session.xml @@ -6,7 +6,7 @@ - + diff --git a/examples/ropes/why3session.xml b/examples/ropes/why3session.xml index dec68c350..74bcfb39e 100644 --- a/examples/ropes/why3session.xml +++ b/examples/ropes/why3session.xml @@ -7,7 +7,7 @@ - + @@ -17,7 +17,7 @@ - + @@ -47,7 +47,7 @@ - + diff --git a/examples/same_fringe/why3session.xml b/examples/same_fringe/why3session.xml index d722dfffe..9c407980f 100644 --- a/examples/same_fringe/why3session.xml +++ b/examples/same_fringe/why3session.xml @@ -3,62 +3,62 @@ "http://why3.lri.fr/why3session.dtd"> - - - + + + - + - + - + - + - + - + - + - + - + - + - + - - + + - + - + - + - + - + diff --git a/examples/sorted_list/why3session.xml b/examples/sorted_list/why3session.xml index 438d6c243..a8d1c5d51 100644 --- a/examples/sorted_list/why3session.xml +++ b/examples/sorted_list/why3session.xml @@ -3,12 +3,12 @@ "http://why3.lri.fr/why3session.dtd"> - - - + + + - + diff --git a/examples/swap/why3session.xml b/examples/swap/why3session.xml index ec217caca..3fdef303f 100644 --- a/examples/swap/why3session.xml +++ b/examples/swap/why3session.xml @@ -4,12 +4,12 @@ - + - + diff --git a/examples/tests-provers/bv/why3session.xml b/examples/tests-provers/bv/why3session.xml index b73e7a739..d4973d959 100644 --- a/examples/tests-provers/bv/why3session.xml +++ b/examples/tests-provers/bv/why3session.xml @@ -98,22 +98,22 @@ - + - + - + - + @@ -139,12 +139,12 @@ - + - + @@ -211,7 +211,7 @@ - + @@ -221,52 +221,52 @@ - + - + - + - + - + - + - + - + - + - + @@ -276,7 +276,7 @@ - + @@ -286,17 +286,17 @@ - + - + - + @@ -306,7 +306,7 @@ - + @@ -331,122 +331,122 @@ - + - + - + - + - + - + - + - + - - + + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -454,7 +454,7 @@ - + @@ -464,18 +464,18 @@ - + - + - + - + @@ -485,38 +485,38 @@ - + - + - + - + - + - + - + - + @@ -552,7 +552,7 @@ - + @@ -579,22 +579,22 @@ - + - + - + - + @@ -612,7 +612,7 @@ - + @@ -627,17 +627,17 @@ - + - + - + @@ -686,22 +686,22 @@ - + - + - + - + @@ -749,12 +749,12 @@ - + - + @@ -851,22 +851,22 @@ - + - + - + - + @@ -892,12 +892,12 @@ - + - + @@ -964,7 +964,7 @@ - + @@ -979,7 +979,7 @@ - + @@ -989,17 +989,17 @@ - + - + - + @@ -1009,32 +1009,32 @@ - + - + - + - + - + - + @@ -1044,7 +1044,7 @@ - + @@ -1059,7 +1059,7 @@ - + @@ -1089,65 +1089,65 @@ - + - + - + - + - + - + - + - + - - + + - + - + - + - + @@ -1156,42 +1156,42 @@ - + - + - + - + - + - + - + - + - + @@ -1202,12 +1202,12 @@ - + - + @@ -1294,17 +1294,17 @@ - + - + - + @@ -1335,7 +1335,7 @@ - + @@ -1412,27 +1412,27 @@ - + - + - + - + - + @@ -1442,22 +1442,22 @@ - + - + - + - + @@ -1467,7 +1467,7 @@ - + @@ -1477,17 +1477,17 @@ - + - + - + @@ -1497,12 +1497,12 @@ - + - + @@ -1527,37 +1527,37 @@ - + - + - + - + - + - + - + @@ -1565,7 +1565,7 @@ - + @@ -1579,12 +1579,12 @@ - + - + @@ -1595,62 +1595,62 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -1737,17 +1737,17 @@ - + - + - + @@ -1778,12 +1778,12 @@ - + - + @@ -1850,7 +1850,7 @@ - + @@ -1860,7 +1860,7 @@ - + @@ -1875,7 +1875,7 @@ - + @@ -1890,32 +1890,32 @@ - + - + - + - + - + - + @@ -1935,7 +1935,7 @@ - + @@ -1945,7 +1945,7 @@ - + @@ -1970,12 +1970,12 @@ - + - + @@ -1985,12 +1985,12 @@ - + - + @@ -2000,26 +2000,26 @@ - + - + - + - + - + @@ -2027,10 +2027,10 @@ - + - + @@ -2044,8 +2044,8 @@ - - + + @@ -2060,49 +2060,49 @@ - + - - + + - + - + - + - + - - + + - + - + - + diff --git a/examples/tests-provers/coq-interval/why3session.xml b/examples/tests-provers/coq-interval/why3session.xml index 49bb763f0..f9b152483 100644 --- a/examples/tests-provers/coq-interval/why3session.xml +++ b/examples/tests-provers/coq-interval/why3session.xml @@ -4,7 +4,7 @@ - + diff --git a/examples/tests-provers/coq/why3session.xml b/examples/tests-provers/coq/why3session.xml index 8d104370e..5247f90a9 100644 --- a/examples/tests-provers/coq/why3session.xml +++ b/examples/tests-provers/coq/why3session.xml @@ -3,9 +3,9 @@ "http://why3.lri.fr/why3session.dtd"> - - - + + + diff --git a/examples/tests-provers/cvc3/why3session.xml b/examples/tests-provers/cvc3/why3session.xml index 0ec5d1a43..1941c0b9d 100644 --- a/examples/tests-provers/cvc3/why3session.xml +++ b/examples/tests-provers/cvc3/why3session.xml @@ -8,21 +8,21 @@ - - + + - + - + - + diff --git a/examples/tests-provers/div/why3session.xml b/examples/tests-provers/div/why3session.xml index 5009bca68..4df9616fc 100644 --- a/examples/tests-provers/div/why3session.xml +++ b/examples/tests-provers/div/why3session.xml @@ -36,7 +36,7 @@ - + @@ -44,11 +44,11 @@ - + - + @@ -60,19 +60,19 @@ - + - + - + - + @@ -84,7 +84,7 @@ - + @@ -92,11 +92,11 @@ - + - + @@ -108,7 +108,7 @@ - + @@ -120,7 +120,7 @@ - + @@ -132,19 +132,19 @@ - + - + - + - + @@ -155,19 +155,19 @@ - + - + - + - + @@ -179,7 +179,7 @@ - + @@ -188,12 +188,12 @@ - + - + @@ -204,23 +204,23 @@ - + - + - + - + - + @@ -233,22 +233,22 @@ - + - - - + + + - + - + - + @@ -261,21 +261,21 @@ - + - - + + - + - + @@ -288,21 +288,21 @@ - + - + - + - + - + @@ -313,23 +313,23 @@ - + - + - + - + - + @@ -344,19 +344,19 @@ - + - + - + - + @@ -368,7 +368,7 @@ - + @@ -376,11 +376,11 @@ - + - + @@ -392,19 +392,19 @@ - + - + - + - + @@ -416,19 +416,19 @@ - + - + - + - + @@ -440,7 +440,7 @@ - + @@ -448,11 +448,11 @@ - + - + @@ -464,7 +464,7 @@ - + @@ -472,11 +472,11 @@ - + - + @@ -488,7 +488,7 @@ - + @@ -497,12 +497,12 @@ - + - + @@ -515,21 +515,21 @@ - + - + - + - + @@ -542,7 +542,7 @@ - + @@ -551,13 +551,13 @@ - + - + - + @@ -570,7 +570,7 @@ - + @@ -579,12 +579,12 @@ - + - + @@ -597,21 +597,21 @@ - + - + - + - + @@ -624,21 +624,21 @@ - + - + - + - + diff --git a/examples/tests-provers/div_real/why3session.xml b/examples/tests-provers/div_real/why3session.xml index a131891bf..863fc4a63 100644 --- a/examples/tests-provers/div_real/why3session.xml +++ b/examples/tests-provers/div_real/why3session.xml @@ -10,86 +10,86 @@ - - - + + + - + - + - + - + - + - + - + - + - + - + - + - + - - + + - - + + - - + + - - + + - + - + diff --git a/examples/tests-provers/ieee_float/why3session.xml b/examples/tests-provers/ieee_float/why3session.xml index 6d9747c13..236f6f239 100644 --- a/examples/tests-provers/ieee_float/why3session.xml +++ b/examples/tests-provers/ieee_float/why3session.xml @@ -54,9 +54,9 @@ - + - + @@ -65,7 +65,7 @@ - + @@ -76,11 +76,11 @@ - - - + + + - + @@ -92,7 +92,7 @@ - + @@ -151,9 +151,9 @@ - + - + @@ -190,17 +190,17 @@ - + - + - + - + @@ -224,20 +224,20 @@ - - + + - + - + - + - + - + diff --git a/examples/tests-provers/metitarski/why3session.xml b/examples/tests-provers/metitarski/why3session.xml index ae475dfce..96e7225a1 100644 --- a/examples/tests-provers/metitarski/why3session.xml +++ b/examples/tests-provers/metitarski/why3session.xml @@ -28,7 +28,7 @@ - + diff --git a/examples/there_and_back_again/why3session.xml b/examples/there_and_back_again/why3session.xml index 25d232e79..d2209d122 100644 --- a/examples/there_and_back_again/why3session.xml +++ b/examples/there_and_back_again/why3session.xml @@ -6,7 +6,7 @@ - + @@ -27,7 +27,7 @@ - + diff --git a/examples/tortoise_and_hare/why3session.xml b/examples/tortoise_and_hare/why3session.xml index 8fee9eb27..745036282 100644 --- a/examples/tortoise_and_hare/why3session.xml +++ b/examples/tortoise_and_hare/why3session.xml @@ -6,7 +6,7 @@ - + diff --git a/examples/tree_height/why3session.xml b/examples/tree_height/why3session.xml index 754113f7b..faee90d0d 100644 --- a/examples/tree_height/why3session.xml +++ b/examples/tree_height/why3session.xml @@ -9,7 +9,7 @@ - + @@ -17,7 +17,7 @@ - + @@ -106,7 +106,7 @@ - + @@ -144,7 +144,7 @@ - + diff --git a/examples/tree_of_array/why3session.xml b/examples/tree_of_array/why3session.xml index 14c03e476..889179e2f 100644 --- a/examples/tree_of_array/why3session.xml +++ b/examples/tree_of_array/why3session.xml @@ -4,7 +4,7 @@ - + diff --git a/examples/tree_of_list/why3session.xml b/examples/tree_of_list/why3session.xml index dd4168d4b..69c301695 100644 --- a/examples/tree_of_list/why3session.xml +++ b/examples/tree_of_list/why3session.xml @@ -3,12 +3,12 @@ "http://why3.lri.fr/why3session.dtd"> - - - + + + - + diff --git a/examples/verifythis_2015_dancing_links/why3session.xml b/examples/verifythis_2015_dancing_links/why3session.xml index a0889b5f5..421bdfe49 100644 --- a/examples/verifythis_2015_dancing_links/why3session.xml +++ b/examples/verifythis_2015_dancing_links/why3session.xml @@ -4,7 +4,7 @@ - + diff --git a/examples/verifythis_2015_relaxed_prefix/why3session.xml b/examples/verifythis_2015_relaxed_prefix/why3session.xml index 25b81823e..6c2553bd2 100644 --- a/examples/verifythis_2015_relaxed_prefix/why3session.xml +++ b/examples/verifythis_2015_relaxed_prefix/why3session.xml @@ -4,7 +4,7 @@ - + diff --git a/examples/verifythis_2017_maximum_sum_submatrix/why3session.xml b/examples/verifythis_2017_maximum_sum_submatrix/why3session.xml index 127d6077f..e61e51281 100644 --- a/examples/verifythis_2017_maximum_sum_submatrix/why3session.xml +++ b/examples/verifythis_2017_maximum_sum_submatrix/why3session.xml @@ -6,7 +6,7 @@ - + diff --git a/examples/verifythis_PrefixSumRec/why3session.xml b/examples/verifythis_PrefixSumRec/why3session.xml index 5373d934e..4225242ba 100644 --- a/examples/verifythis_PrefixSumRec/why3session.xml +++ b/examples/verifythis_PrefixSumRec/why3session.xml @@ -10,7 +10,7 @@ - + diff --git a/examples/vstte10_aqueue/why3session.xml b/examples/vstte10_aqueue/why3session.xml index 8c5dbb4b0..9a4cffa61 100644 --- a/examples/vstte10_aqueue/why3session.xml +++ b/examples/vstte10_aqueue/why3session.xml @@ -3,24 +3,24 @@ "http://why3.lri.fr/why3session.dtd"> - - - + + + - + - + - + - + - + diff --git a/examples/vstte10_search_list/why3session.xml b/examples/vstte10_search_list/why3session.xml index 646450bdd..58f40c5eb 100644 --- a/examples/vstte10_search_list/why3session.xml +++ b/examples/vstte10_search_list/why3session.xml @@ -7,7 +7,7 @@ - + diff --git a/examples/vstte12_combinators/why3session.xml b/examples/vstte12_combinators/why3session.xml index c794dd5ca..34fe2fb82 100644 --- a/examples/vstte12_combinators/why3session.xml +++ b/examples/vstte12_combinators/why3session.xml @@ -8,7 +8,7 @@ - + diff --git a/examples/vstte12_ring_buffer/why3session.xml b/examples/vstte12_ring_buffer/why3session.xml index c0b98d40a..2ff66388a 100644 --- a/examples/vstte12_ring_buffer/why3session.xml +++ b/examples/vstte12_ring_buffer/why3session.xml @@ -8,7 +8,7 @@ - + @@ -107,7 +107,7 @@ - + @@ -118,7 +118,7 @@ - + @@ -141,7 +141,7 @@ - + diff --git a/examples/vstte12_tree_reconstruction/why3session.xml b/examples/vstte12_tree_reconstruction/why3session.xml index 25b8eed07..0fb3d9963 100644 --- a/examples/vstte12_tree_reconstruction/why3session.xml +++ b/examples/vstte12_tree_reconstruction/why3session.xml @@ -9,7 +9,7 @@ - + @@ -41,7 +41,7 @@ - + @@ -74,7 +74,7 @@ - + @@ -89,12 +89,12 @@ - + - + diff --git a/examples/warshall_algorithm/why3session.xml b/examples/warshall_algorithm/why3session.xml index 5728c627e..764a75c62 100644 --- a/examples/warshall_algorithm/why3session.xml +++ b/examples/warshall_algorithm/why3session.xml @@ -7,7 +7,7 @@ - + diff --git a/examples/white_and_black_balls/why3session.xml b/examples/white_and_black_balls/why3session.xml index 0bca366a8..d5dc289a7 100644 --- a/examples/white_and_black_balls/why3session.xml +++ b/examples/white_and_black_balls/why3session.xml @@ -3,9 +3,9 @@ "http://why3.lri.fr/why3session.dtd"> - - - + + + diff --git a/examples/zeros/why3session.xml b/examples/zeros/why3session.xml index de60134f8..3e03feeac 100644 --- a/examples/zeros/why3session.xml +++ b/examples/zeros/why3session.xml @@ -4,7 +4,7 @@ - + @@ -12,7 +12,7 @@ - + -- GitLab