diff --git a/CHANGES b/CHANGES
index a24f09277e98dc22a59d4cf3eea680e258a9883d..8ac29acc86c991471195b7373efa538eaeb14920 100644
--- a/CHANGES
+++ b/CHANGES
@@ -31,12 +31,16 @@ Encodings
Provers
* discarded support for Alt-Ergo versions older than 0.95.2
+ o support for Alt-Ergo 1.01 (released Feb 16, 2016) and
+ non-free versions 1.10 and 1.20
o support for Coq 8.4pl6 (released Apr 9, 2015)
+ o support for Coq 8.5 (released Jan 21, 2016)
o support for Gappa 1.2.0 (released May 19, 2015)
* discarded support for Isabelle 2014
- o support for Isabelle 2015 (released May 25, 2015) and Isabelle
- 2016 (released ?, 2016)
- o support for Z3 4.4.0 (released Apr 29, 2015)
+ o support for Isabelle 2015 (released May 25, 2015) and
+ Isabelle 2016 (released Feb 17, 2016)
+ o support for Z3 4.4.0 (released Apr 29, 2015) and
+ 4.4.1 (released Oct 5, 2015)
o support for Zenon 0.8.0 (released Oct 21, 2014)
o support for Zenon_modulo 0.4.1 (released Jul 2, 2015)
diff --git a/doc/coq.tex b/doc/coq.tex
index 011dad179d82d220c63764a77801552bc836c3f5..79026038d49697d67502e5c240b25a54c68ae0a1 100644
--- a/doc/coq.tex
+++ b/doc/coq.tex
@@ -15,7 +15,7 @@ generated parts or adding empty lines inside them.
will be lost when the file is regenerated by \why. This part ends
at the first empty line.
\item Abstract logic symbols are assumed with the vernacular directive
- \verb+Paramater+. Axioms are assumed with the \verb+Axiom+
+ \verb+Parameter+. Axioms are assumed with the \verb+Axiom+
directive. When regenerating a script, \why assumes that all such
symbols have been generated by a previous run. As a consequence,
the user should not introduce new symbols with these two
diff --git a/examples/logic/genealogy/why3session.xml b/examples/logic/genealogy/why3session.xml
index cf1545365cb8030294dc040499649d25cd2d55f0..56e6f2423af134c3dda33b743b3cb84e748c7ddd 100644
--- a/examples/logic/genealogy/why3session.xml
+++ b/examples/logic/genealogy/why3session.xml
@@ -16,6 +16,7 @@
+
@@ -29,9 +30,10 @@
+
-
+
@@ -43,6 +45,7 @@
+
@@ -55,8 +58,9 @@
+
-
+
@@ -69,6 +73,7 @@
+
@@ -80,8 +85,9 @@
+
-
+
@@ -93,6 +99,7 @@
+
@@ -103,8 +110,9 @@
+
-
+
@@ -116,6 +124,7 @@
+
@@ -127,8 +136,9 @@
+
-
+
@@ -140,6 +150,7 @@
+
@@ -151,8 +162,9 @@
+
-
+
@@ -164,6 +176,7 @@
+
@@ -175,8 +188,9 @@
+
-
+
@@ -188,6 +202,7 @@
+
@@ -199,6 +214,7 @@
+
diff --git a/share/provers-detection-data.conf b/share/provers-detection-data.conf
index 4956882ce3c9b19bf2dedbfaf38a4b4d12f57eda..b2104605c37a10b518fed65a90d44c7e720d38b4 100644
--- a/share/provers-detection-data.conf
+++ b/share/provers-detection-data.conf
@@ -1,11 +1,13 @@
[ATP alt-ergo]
name = "Alt-Ergo"
exec = "alt-ergo"
-exec = "alt-ergo-1.00.prv"
-exec = "alt-ergo-1.01"
+exec = "alt-ergo-1.20.prv"
exec = "alt-ergo-1.10.prv"
+exec = "alt-ergo-1.01"
+exec = "alt-ergo-1.00.prv"
version_switch = "-version"
version_regexp = "^\\([0-9.]+\\(-dev\\|prv\\)?\\)$"
+version_ok = "1.20.prv"
version_ok = "1.10.prv"
version_ok = "1.01"
version_ok = "1.00.prv"
@@ -324,9 +326,11 @@ version_old = "201310"
[ATP z3]
name = "Z3"
exec = "z3"
+exec = "z3-4.4.1"
exec = "z3-4.4.0"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
+version_ok = "4.4.1"
version_ok = "4.4.0"
driver = "drivers/z3_440.drv"
command = "%l/why3-cpulimit %t %m -s %e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f"
@@ -337,9 +341,11 @@ command_steps = "%l/why3-cpulimit %U %m -s %e -smt2 sat.random_seed=42 nlsat.ran
name = "Z3"
alternative = "noBV"
exec = "z3"
+exec = "z3-4.4.1"
exec = "z3-4.4.0"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
+version_ok = "4.4.1"
version_ok = "4.4.0"
driver = "drivers/z3_432.drv"
command = "%l/why3-cpulimit %t %m -s %e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f"