diff options
| author | Maxime Dénès | 2017-06-20 09:30:59 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-20 09:30:59 +0200 |
| commit | b39d8ddff03db8f6e1ab739a13ab1bdb7ea849be (patch) | |
| tree | 110681dc1ddefd5fbf48f7ee46a17820d55cd2ba /test-suite | |
| parent | 25cd7acea0df79fcc07274e429c9839de1246611 (diff) | |
| parent | d7e85f575fe6a41a700da9cd50236bef8ab03cf8 (diff) | |
Merge PR#807: romega: fix a slowdown
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/ROmega3.v | 31 |
1 files changed, 31 insertions, 0 deletions
diff --git a/test-suite/success/ROmega3.v b/test-suite/success/ROmega3.v new file mode 100644 index 0000000000..fd4ff260b5 --- /dev/null +++ b/test-suite/success/ROmega3.v @@ -0,0 +1,31 @@ + +Require Import ZArith ROmega. +Local Open Scope Z_scope. + +(** Benchmark provided by Chantal Keller, that romega used to + solve far too slowly (compared to omega or lia). *) + +Parameter v4 : Z. +Parameter v3 : Z. +Parameter o4 : Z. +Parameter s5 : Z. +Parameter v2 : Z. +Parameter o5 : Z. +Parameter s6 : Z. +Parameter v1 : Z. +Parameter o6 : Z. +Parameter s7 : Z. +Parameter v0 : Z. +Parameter o7 : Z. + +Lemma lemma_5833 : + ~ 16 * v4 + (8 * v3 + (-8192 * o4 + (-4096 * s5 + (4 * v2 + + (-4096 * o5 + (-2048 * s6 + (2 * v1 + (-2048 * o6 + + (-1024 * s7 + (v0 + -1024 * o7)))))))))) >= 8192 +\/ + 16 * v4 + (8 * v3 + (-8192 * o4 + (-4096 * s5 + (4 * v2 + + (-4096 * o5 + (-2048 * s6 + (2 * v1 + (-2048 * o6 + + (-1024 * s7 + (v0 + -1024 * o7)))))))))) >= 1024. +Proof. +Timeout 1 romega. (* should take a few milliseconds, not seconds *) +Timeout 1 Qed. (* ditto *) |