diff options
author | Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-05-29 18:03:19 +0200 |
---|---|---|
committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-05-29 18:20:05 +0200 |
commit | 2125c92aa9d17b27c9a19a59774e7e319e48262b (patch) | |
tree | 57b6734b6ed307795e0397cd596cecf05a70c66a /test-suite/bugs/closed/4132.v | |
parent | eefda76f6f42674fb342e1aa5f1dcf29569a4806 (diff) |
Omega: use "simpl" only on coefficents, not on atoms (fix #4132)
Two issues in one:
- some focused_simpl were called on the wrong locations
- some focused_simpl were done on whole equations
In the two cases, this could be bad if "simpl" goes too far
with respect to what omega expects: later calls to "occurrence"
might fail. This may happen for instance if an atom isn't a variable,
but a let-in (b:=5:Z in the example).
Diffstat (limited to 'test-suite/bugs/closed/4132.v')
-rw-r--r-- | test-suite/bugs/closed/4132.v | 31 |
1 files changed, 31 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4132.v b/test-suite/bugs/closed/4132.v new file mode 100644 index 000000000..806ffb771 --- /dev/null +++ b/test-suite/bugs/closed/4132.v @@ -0,0 +1,31 @@ + +Require Import ZArith Omega. +Open Scope Z_scope. + +(** bug 4132: omega was using "simpl" either on whole equations, or on + delimited but wrong spots. This was leading to unexpected reductions + when one atom (here [b]) is an evaluable reference instead of a variable. *) + +Lemma foo + (x y x' zxy zxy' z : Z) + (b := 5) + (Ry : - b <= y < b) + (Bx : x' <= b) + (H : - zxy' <= zxy) + (H' : zxy' <= x') : - b <= zxy. +Proof. +omega. (* was: Uncaught exception Invalid_argument("index out of bounds"). *) +Qed. + +Lemma foo2 x y (b := 5) (H1 : x <= y) (H2 : y <= b) : x <= b. +omega. (* Pierre L: according to a comment of bug report #4132, + this might have triggered "index out of bounds" in the past, + but I never managed to reproduce that in any version, + even before my fix. *) +Qed. + +Lemma foo3 x y (b := 0) (H1 : x <= y) (H2 : y <= b) : x <= b. +omega. (* Pierre L: according to a comment of bug report #4132, + this might have triggered "Failure(occurence 2)" in the past, + but I never managed to reproduce that. *) +Qed. |