From e978da8c41d8a3c19a29036d9c569fbe2a4616b0 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 16 Jun 2006 14:41:51 +0000
Subject: Imported Upstream version 8.0pl3+8.1beta

---
 test-suite/success/ROmega2.v | 28 ++++++++++++++++++++++++++++
 1 file changed, 28 insertions(+)
 create mode 100644 test-suite/success/ROmega2.v

(limited to 'test-suite/success/ROmega2.v')

diff --git a/test-suite/success/ROmega2.v b/test-suite/success/ROmega2.v
new file mode 100644
index 00000000..9d47c9f6
--- /dev/null
+++ b/test-suite/success/ROmega2.v
@@ -0,0 +1,28 @@
+Require Import ZArith ROmega.
+
+(* Submitted by Yegor Bryukhov (#922) *)
+
+Open Scope Z_scope.
+
+Lemma Test46 : 
+forall v1 v2 v3 v4 v5 : Z,
+((2 * v4) + (5)) + (8 * v2) <= ((4 * v4) + (3 * v4)) + (5 * v4) ->
+9 * v4 > (1 * v4) + ((2 * v1) + (0 * v2)) ->
+((9 * v3) + (2 * v5)) + (5 * v2) = 3 * v4 ->
+0 > 6 * v1 ->
+(0 * v3) + (6 * v2) <> 2 ->
+(0 * v3) + (5 * v5) <> ((4 * v2) + (8 * v2)) + (2 * v5) ->
+7 * v3 > 5 * v5 ->
+0 * v4 >= ((5 * v1) + (4 * v1)) + ((6 * v5) + (3 * v5)) ->
+7 * v2 = ((3 * v2) + (6 * v5)) + (7 * v2) ->
+0 * v3 > 7 * v1 ->
+9 * v2 < 9 * v5 ->
+(2 * v3) + (8 * v1) <= 5 * v4 ->
+5 * v2 = ((5 * v1) + (0 * v5)) + (1 * v2) ->
+0 * v5 <= 9 * v2 ->
+((7 * v1) + (1 * v3)) + ((2 * v3) + (1 * v3)) >= ((6 * v5) + (4)) + ((1) + (9))
+-> False.
+intros.
+(*romega.*)
+Admitted.
+
-- 
cgit v1.2.3