correct the version for alt-ergo and coq

ab31cb93 · François Bobot · c709b941 · ab31cb93 · ab31cb93 · ab31cb93
Commit ab31cb93 authored Jan 27, 2012 by François Bobot
69 changed files
--- a/examples/bts/12475/why3session.xml
+++ b/examples/bts/12475/why3session.xml
@@ -9,7 +9,7 @@
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/bts/12934/why3session.xml
+++ b/examples/bts/12934/why3session.xml
@@ -5,11 +5,11 @@
 <prover
  id="alt-ergo"
  name="Alt-Ergo"
-  version="0.93"/>
+  version="0.94"/>
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/check-builtin/ac/why3session.xml
+++ b/examples/check-builtin/ac/why3session.xml
@@ -5,11 +5,11 @@
 <prover
  id="alt-ergo"
  name="Alt-Ergo"
-  version="0.93"/>
+  version="0.94"/>
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/check-builtin/array/why3session.xml
+++ b/examples/check-builtin/array/why3session.xml
@@ -9,7 +9,7 @@
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/check-builtin/bool/why3session.xml
+++ b/examples/check-builtin/bool/why3session.xml
@@ -5,11 +5,11 @@
 <prover
  id="alt-ergo"
  name="Alt-Ergo"
-  version="0.93"/>
+  version="0.94"/>
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/check-builtin/euclideandivision/why3session.xml
+++ b/examples/check-builtin/euclideandivision/why3session.xml
@@ -9,7 +9,7 @@
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/check-builtin/floats/why3session.xml
+++ b/examples/check-builtin/floats/why3session.xml
@@ -9,7 +9,7 @@
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/check-builtin/int/why3session.xml
+++ b/examples/check-builtin/int/why3session.xml
@@ -9,7 +9,7 @@
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/check-builtin/intreal/why3session.xml
+++ b/examples/check-builtin/intreal/why3session.xml
@@ -9,7 +9,7 @@
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/check-builtin/minmax/why3session.xml
+++ b/examples/check-builtin/minmax/why3session.xml
@@ -5,11 +5,11 @@
 <prover
  id="alt-ergo"
  name="Alt-Ergo"
-  version="0.93"/>
+  version="0.94"/>
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/check-builtin/propositional/why3session.xml
+++ b/examples/check-builtin/propositional/why3session.xml
@@ -5,11 +5,11 @@
 <prover
  id="alt-ergo"
  name="Alt-Ergo"
-  version="0.93"/>
+  version="0.94"/>
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/check-builtin/real/why3session.xml
+++ b/examples/check-builtin/real/why3session.xml
@@ -9,7 +9,7 @@
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/einstein/why3session.xml
+++ b/examples/einstein/why3session.xml
@@ -5,11 +5,11 @@
 <prover
  id="alt-ergo"
  name="Alt-Ergo"
-  version="0.93"/>
+  version="0.94"/>
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/explicit_subst/why3session.xml
+++ b/examples/explicit_subst/why3session.xml
@@ -9,7 +9,7 @@
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/genealogy/why3session.xml
+++ b/examples/genealogy/why3session.xml
@@ -5,11 +5,11 @@
 <prover
  id="alt-ergo"
  name="Alt-Ergo"
-  version="0.93"/>
+  version="0.94"/>
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/hello_proof/why3session.xml
+++ b/examples/hello_proof/why3session.xml
@@ -9,7 +9,7 @@
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/my_cosine/why3session.xml
+++ b/examples/my_cosine/why3session.xml
@@ -9,7 +9,7 @@
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/ns_clone/why3session.xml
+++ b/examples/ns_clone/why3session.xml
@@ -5,11 +5,11 @@
 <prover
  id="alt-ergo"
  name="Alt-Ergo"
-  version="0.93"/>
+  version="0.94"/>
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/programs/assigning_meanings_to_programs/why3session.xml
+++ b/examples/programs/assigning_meanings_to_programs/why3session.xml
@@ -9,7 +9,7 @@
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/programs/binary_search/why3session.xml
+++ b/examples/programs/binary_search/why3session.xml
@@ -9,7 +9,7 @@
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/programs/bresenham/why3session.xml
+++ b/examples/programs/bresenham/why3session.xml
@@ -9,7 +9,7 @@
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/programs/checking_a_large_routine/why3session.xml
+++ b/examples/programs/checking_a_large_routine/why3session.xml
@@ -9,7 +9,7 @@
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/programs/decrease1/why3session.xml
+++ b/examples/programs/decrease1/why3session.xml
@@ -9,7 +9,7 @@
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/programs/edit_distance/why3session.xml
+++ b/examples/programs/edit_distance/why3session.xml
@@ -9,7 +9,7 @@
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/programs/euler001/why3session.xml
+++ b/examples/programs/euler001/why3session.xml
@@ -9,7 +9,7 @@
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/programs/ewd673/why3session.xml
+++ b/examples/programs/ewd673/why3session.xml
@@ -9,7 +9,7 @@
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/programs/fact/why3session.xml
+++ b/examples/programs/fact/why3session.xml
@@ -9,7 +9,7 @@
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/programs/fib_memo/why3session.xml
+++ b/examples/programs/fib_memo/why3session.xml
@@ -9,7 +9,7 @@
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/programs/fibonacci/why3session.xml
+++ b/examples/programs/fibonacci/why3session.xml
@@ -9,7 +9,7 @@
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/programs/find/why3session.xml
+++ b/examples/programs/find/why3session.xml
@@ -9,7 +9,7 @@
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/programs/flag/why3session.xml
+++ b/examples/programs/flag/why3session.xml
@@ -9,7 +9,7 @@
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/programs/foveoos11_challenge1/why3session.xml
+++ b/examples/programs/foveoos11_challenge1/why3session.xml
@@ -9,7 +9,7 @@
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/programs/foveoos11_challenge2/why3session.xml
+++ b/examples/programs/foveoos11_challenge2/why3session.xml
@@ -9,7 +9,7 @@
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/programs/foveoos11_challenge3/why3session.xml
+++ b/examples/programs/foveoos11_challenge3/why3session.xml
@@ -9,7 +9,7 @@
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/programs/gcd/why3session.xml
+++ b/examples/programs/gcd/why3session.xml
@@ -9,7 +9,7 @@
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/programs/gcd_bezout/why3session.xml
+++ b/examples/programs/gcd_bezout/why3session.xml
@@ -9,7 +9,7 @@
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/programs/generate_all_trees/why3session.xml
+++ b/examples/programs/generate_all_trees/why3session.xml
@@ -9,7 +9,7 @@
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/programs/insertion_sort/why3session.xml
+++ b/examples/programs/insertion_sort/why3session.xml
@@ -9,7 +9,7 @@
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/programs/insertion_sort_list/why3session.xml
+++ b/examples/programs/insertion_sort_list/why3session.xml
@@ -9,7 +9,7 @@
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/programs/isqrt/why3session.xml
+++ b/examples/programs/isqrt/why3session.xml
@@ -9,7 +9,7 @@
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/programs/kmp/why3session.xml
+++ b/examples/programs/kmp/why3session.xml
@@ -9,7 +9,7 @@
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/programs/knuth_prime_numbers/why3session.xml
+++ b/examples/programs/knuth_prime_numbers/why3session.xml
@@ -9,7 +9,7 @@
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/programs/list_rev/why3session.xml
+++ b/examples/programs/list_rev/why3session.xml
@@ -9,7 +9,7 @@
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/programs/mccarthy/why3session.xml
+++ b/examples/programs/mccarthy/why3session.xml
@@ -9,7 +9,7 @@
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/programs/mergesort_list/why3session.xml
+++ b/examples/programs/mergesort_list/why3session.xml
@@ -9,7 +9,7 @@
 <prover
  id="1"
  prover_id="coq" name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="2"
  prover_id="cvc3-2.2" name="CVC3"

--- a/examples/programs/mergesort_queue/why3session.xml
+++ b/examples/programs/mergesort_queue/why3session.xml
@@ -9,7 +9,7 @@
 <prover
  id="1"
  prover_id="coq" name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="2"
  prover_id="cvc3-2.2" name="CVC3"

--- a/examples/programs/mjrty/why3session.xml
+++ b/examples/programs/mjrty/why3session.xml
@@ -5,11 +5,11 @@
 <prover
  id="alt-ergo"
  name="Alt-Ergo"
-  version="0.93.1"/>
+  version="0.94"/>
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/programs/muller/why3session.xml
+++ b/examples/programs/muller/why3session.xml
@@ -9,7 +9,7 @@
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/programs/my_cosine/why3session.xml
+++ b/examples/programs/my_cosine/why3session.xml
@@ -9,7 +9,7 @@
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/programs/power/why3session.xml
+++ b/examples/programs/power/why3session.xml
@@ -9,7 +9,7 @@
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/programs/queens/why3session.xml
+++ b/examples/programs/queens/why3session.xml
@@ -9,7 +9,7 @@
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/programs/quicksort/why3session.xml
+++ b/examples/programs/quicksort/why3session.xml
@@ -9,7 +9,7 @@
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/programs/same_fringe/why3session.xml
+++ b/examples/programs/same_fringe/why3session.xml
@@ -9,7 +9,7 @@
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/programs/selection_sort/why3session.xml
+++ b/examples/programs/selection_sort/why3session.xml
@@ -9,7 +9,7 @@
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/programs/sf/why3session.xml
+++ b/examples/programs/sf/why3session.xml
@@ -9,7 +9,7 @@
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/programs/snapshotable_trees/why3session.xml
+++ b/examples/programs/snapshotable_trees/why3session.xml
@@ -5,7 +5,7 @@
 <prover
  id="0"
  name="Alt-Ergo"
-  version="0.93.1"/>
+  version="0.94"/>
 <file
  name="../snapshotable_trees.mlw"
  verified="false"

--- a/examples/programs/sorted_list/why3session.xml
+++ b/examples/programs/sorted_list/why3session.xml
@@ -9,7 +9,7 @@
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/programs/tortoise_and_hare/why3session.xml
+++ b/examples/programs/tortoise_and_hare/why3session.xml
@@ -9,7 +9,7 @@
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/programs/unraveling_a_card_trick/why3session.xml
+++ b/examples/programs/unraveling_a_card_trick/why3session.xml
@@ -5,7 +5,7 @@
 <prover
  id="alt-ergo"
  name="Alt-Ergo"
-  version="0.93.1"/>
+  version="0.94"/>
 <prover
  id="coq"
  name="Coq"

--- a/examples/programs/vacid_0_red_black_trees/why3session.xml
+++ b/examples/programs/vacid_0_red_black_trees/why3session.xml
@@ -9,7 +9,7 @@
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl3"/>
 <prover
  id="cvc3-2.2"
  name="CVC3"

--- a/examples/programs/vacid_0_sparse_array/why3session.xml
+++ b/examples/programs/vacid_0_sparse_array/why3session.xml
@@ -9,7 +9,7 @@
 <prover
  id="coq"
  name="Coq"
-  version="8.3pl2"/>