diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml
index ff663736385c38996242a8f7a39857d35bc6ba1e..430d87177b910f79106126668e9c9f668d606f23 100644
--- a/src/plugins/qed/term.ml
+++ b/src/plugins/qed/term.ml
@@ -2242,7 +2242,8 @@ struct
     let res = ref None in
     let found_term t = assert (!res = None);
       assert (not (Vars.mem x t.vars));
-      res := Some t; true
+      if not (lc_closed t) then false else
+        (res := Some t; true)
     in
     let is_term_ok a b =
       match a.repr with
diff --git a/src/plugins/wp/tests/wp_bts/oracle/ex5.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/ex5.res.oracle
index 6a9e199c6af53c02176f226f781d11228a0383ce..b37af5db7fee1f02ca661429b7f9954e48c38d54 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/ex5.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/ex5.res.oracle
@@ -32,7 +32,7 @@ Prove: true.
 ------------------------------------------------------------
 
 Goal Post-condition 'ok12' in 'exists':
-Prove: true.
+Prove: exists i_1,i : Z. L_f(i) = i_1.
 
 ------------------------------------------------------------
 
@@ -42,7 +42,7 @@ Prove: true.
 ------------------------------------------------------------
 
 Goal Post-condition 'ok22' in 'exists':
-Prove: true.
+Prove: exists i_1,i : Z. (1 + i_1) = L_f(i).
 
 ------------------------------------------------------------
 
@@ -52,7 +52,7 @@ Prove: true.
 ------------------------------------------------------------
 
 Goal Post-condition 'ok32' in 'exists':
-Prove: true.
+Prove: exists i_1,i : Z. (a + i_1 + L_f(a)) = (b + L_f(i)).
 
 ------------------------------------------------------------
 
@@ -130,7 +130,7 @@ Prove: false.
 ------------------------------------------------------------
 
 Goal Post-condition 'ok12' in 'forall':
-Prove: false.
+Prove: L_f(i) != i_1.
 
 ------------------------------------------------------------
 
@@ -140,7 +140,7 @@ Prove: false.
 ------------------------------------------------------------
 
 Goal Post-condition 'ok22' in 'forall':
-Prove: false.
+Prove: (1 + i) != L_f(i_1).
 
 ------------------------------------------------------------
 
@@ -150,7 +150,7 @@ Prove: false.
 ------------------------------------------------------------
 
 Goal Post-condition 'ok32' in 'forall':
-Prove: false.
+Prove: (a + i + L_f(a)) != (b + L_f(i_1)).
 
 ------------------------------------------------------------