diff --git a/examples/prover/Unification.mlw b/examples/prover/Unification.mlw
index fdab3c0893b97f2cc9a341846a28e81f4d8386b0..13980a88df7fe27879f039fffab1153e25e28559 100644
--- a/examples/prover/Unification.mlw
+++ b/examples/prover/Unification.mlw
@@ -445,6 +445,7 @@ module Impl
let rhoi = rho.unifier in
let ghost stm = st tm rhoi in
(*let n0 = rho.iteration in*)
+ bottomvar rhob rho z;
assert { rho0 z = Var_fo_term z } ;
assert { rhoi z = Var_fo_term z } ;
(*assert { forall s:int -> (fo_term int int).
diff --git a/examples/prover/Unification/why3session.xml b/examples/prover/Unification/why3session.xml
index 7a43117d7a3ef8145b13f20e850e056b23504cf4..921d0bf0b1321d73a056c053d31081aa5b85ce2f 100644
--- a/examples/prover/Unification/why3session.xml
+++ b/examples/prover/Unification/why3session.xml
@@ -13,7 +13,7 @@
-
+
@@ -33,10 +33,54 @@
-
-
-
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
@@ -182,8 +226,8 @@
-
-
+
+
@@ -194,467 +238,474 @@
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
+
-
+
-
+
-
+
+
+
+
-
+
+
+
+
-
-
+
+
-
+
-
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
+
-
+
-
-
+
+
-
-
+
+
-
-
+
+
-
+
-
-
+
+
-
-
+
+
-
-
+
+
-
+
-
-
+
+
-
+
-
-
+
+
-
-
+
+
-
-
+
+
-
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
+
-
-
+
+
-
-
+
+
-
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
+
-
-
+
+
-
-
+
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
-
+
+
-
+
-
-
+
+
-
-
+
+
-
+
-
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
+
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
+
-
+
-
+
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
+
-
-
+
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
+
-
+
-
+
-
+
-
+
-
+
-
+
+
+
+
-
+
+
-
+
-
+
-
+
-
+
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
-
-
+
+
-
-
+
+
-
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
+
-
+
-
-
+
+
-
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
+
-
+
-
-
+
+
-
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
diff --git a/examples/prover/Unification/why3shapes.gz b/examples/prover/Unification/why3shapes.gz
index 0f2d7e297fa68004fe31065b6a20482e4e1b1bbc..91f2ec8c4aa0b048288136ba61142ba88ec3a39a 100644
Binary files a/examples/prover/Unification/why3shapes.gz and b/examples/prover/Unification/why3shapes.gz differ