diff options
| author | Maxime Dénès | 2017-05-30 14:50:43 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-05-30 14:50:43 +0200 |
| commit | 45338c57d07b24f9daac2fe347a4bf0e62cdf8c0 (patch) | |
| tree | 57b6734b6ed307795e0397cd596cecf05a70c66a /test-suite/bugs | |
| parent | eefda76f6f42674fb342e1aa5f1dcf29569a4806 (diff) | |
| parent | 2125c92aa9d17b27c9a19a59774e7e319e48262b (diff) | |
Merge PR#695: Omega: fix bug #4132
Diffstat (limited to 'test-suite/bugs')
| -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 0000000000..806ffb771f --- /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. |