From eb3dd1650afc9a7166e8135f84a269b6e413dd37 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Fri, 28 Jun 2019 08:06:11 +0200
Subject: [PATCH] [qed] restaures term invariants on let-introductions
---
src/plugins/qed/term.ml | 3 ++-
src/plugins/wp/tests/wp_bts/oracle/ex5.res.oracle | 12 ++++++------
2 files changed, 8 insertions(+), 7 deletions(-)
diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml
index ff663736385..430d87177b9 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 6a9e199c6af..b37af5db7fe 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)).
------------------------------------------------------------
--
GitLab