diff --git a/src/plugins/wp/share/why3/frama_c_wp/qed.mlw b/src/plugins/wp/share/why3/frama_c_wp/qed.mlw
index 845fbeab4072375761a8f57907c9b2b42f740db7..8992dc01542d09ab6a4a566f9651a729202e5512 100644
--- a/src/plugins/wp/share/why3/frama_c_wp/qed.mlw
+++ b/src/plugins/wp/share/why3/frama_c_wp/qed.mlw
@@ -28,18 +28,8 @@ theory Qed
   use real.FromInt
   use int.ComputerDivision as CD
 
-  (** to be used only for the ACSL ite generation.
-      Something is wrong with "wp/share/ergo/bool.Bool.mlw" (coming from why3),
-      the function match_bool is undefined.  
-      An hack is to give a definition here. *)
-  function match_bool (x : bool) (y z:'a ) : 'a
-  axiom match_bool: forall p:bool, x:'a, y:'a [match_bool p x y].
-   ( p=True /\ match_bool p x y=x ) ||
-   ( p=False /\ match_bool p x y=y )
-  meta "remove_for_why3" axiom match_bool
-
   (** The definitions are in comment because its not useful for coq
-  (no if-then-else on formula) and not tested on automatic provers *)
+      (no if-then-else on formula) and not tested on automatic provers *)
 
   function eqb (x y : 'a) : bool (*= if x = y then True else False*)
   axiom eqb : forall x:'a, y:'a. eqb x y = True <-> x = y
diff --git a/src/plugins/wp/tests/wp_bts/issue_81.i b/src/plugins/wp/tests/wp_bts/issue_81.i
new file mode 100644
index 0000000000000000000000000000000000000000..50f0a51b00516f4dd0b4c140abd6430349723e6b
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/issue_81.i
@@ -0,0 +1,4 @@
+/*@ predicate isMax( integer x, integer y, integer z ) = x < y ? x == z : y == z ; */
+
+/*@ ensures isMax(a,b,\result); */
+int getMax(int a,int b) { return a <= b ? a : b; }
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_81.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_81.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..3c3d2d46a68d9024af31e4d184d6a5d81b5478d4
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle/issue_81.res.oracle
@@ -0,0 +1,19 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_bts/issue_81.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Function getMax
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_bts/issue_81.i, line 3) in 'getMax':
+Assume {
+  Type: is_sint32(a) /\ is_sint32(b) /\ is_sint32(getMax_0).
+  If a <= b
+  Then { Have: getMax_0 = a. }
+  Else { Have: getMax_0 = b. }
+}
+Prove: P_isMax(a, b, getMax_0).
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_81.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_81.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..9486ece4eccbf935e4da4957d98eb7d28619cef9
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_81.res.oracle
@@ -0,0 +1,14 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_bts/issue_81.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] 1 goal scheduled
+[wp] [Alt-Ergo] Goal typed_getMax_ensures : Valid
+[wp] Proved goals:    1 / 1
+  Qed:             0 
+  Alt-Ergo:        1
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  getMax                    -        1        1       100%
+------------------------------------------------------------