diff options
| author | Frédéric Besson | 2020-08-10 16:45:35 +0200 |
|---|---|---|
| committer | Frédéric Besson | 2020-08-10 18:55:25 +0200 |
| commit | 74932ad2ff431f49370d8bb0f730a588b192b484 (patch) | |
| tree | bfd25ebb404a583512785a54854dcaa5440c2b5f /test-suite | |
| parent | ef08abec26c2f0017d1136870f8f99144e579538 (diff) | |
[micromega] Fix bug#12790
zify used to generate many syntactic positivity constraints when translating a goal
from nat to Z. For instance, to state that the product of 2 integers
is positive. Instead, lia performs an interval analysis that is more semantic.
The bug was that the interval analysis was performed after the
elimination of equations. The current workaround is to perform
interval analysis before and after eliminating equations.
bla
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/micromega/bug_12790.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/test-suite/micromega/bug_12790.v b/test-suite/micromega/bug_12790.v new file mode 100644 index 0000000000..39d640ebd9 --- /dev/null +++ b/test-suite/micromega/bug_12790.v @@ -0,0 +1,8 @@ +Require Import Lia. + +Goal forall (a b c d x: nat), +S c = a - b -> x <= x + (S c) * d. +Proof. +intros a b c d x H. +lia. +Qed. |