From 97bec684eb514700879778c0da9b05e4264a99f6 Mon Sep 17 00:00:00 2001
From: Frédéric Besson
Date: Mon, 6 Jan 2020 11:57:11 +0100
Subject: [micromega] fix of bug #11191

- Add an instance to ZifyInst to instruct zify that
 0 < x -> 0 < y -> 0 < Z.pow x y

- More aggressive interval analysis to bound non-linear monomials.
---
 test-suite/micromega/bug_11191a.v | 6 ++++++
 test-suite/micromega/bug_11191b.v | 6 ++++++
 2 files changed, 12 insertions(+)
 create mode 100644 test-suite/micromega/bug_11191a.v
 create mode 100644 test-suite/micromega/bug_11191b.v

(limited to 'test-suite')

diff --git a/test-suite/micromega/bug_11191a.v b/test-suite/micromega/bug_11191a.v
new file mode 100644
index 0000000000..57c1d7d52f
--- /dev/null
+++ b/test-suite/micromega/bug_11191a.v
@@ -0,0 +1,6 @@
+Require Import ZArith Lia.
+
+Goal forall p n, (0 < Z.pos (p ^ n))%Z.
+  intros.
+  lia.
+Qed.
diff --git a/test-suite/micromega/bug_11191b.v b/test-suite/micromega/bug_11191b.v
new file mode 100644
index 0000000000..007470c5b3
--- /dev/null
+++ b/test-suite/micromega/bug_11191b.v
@@ -0,0 +1,6 @@
+Require Import ZArith Lia.
+
+Goal forall p, (0 < Z.pos (p ^ 2))%Z.
+  intros.
+  lia.
+Qed.
-- 
cgit v1.2.3