From 74932ad2ff431f49370d8bb0f730a588b192b484 Mon Sep 17 00:00:00 2001
From: Frédéric Besson
Date: Mon, 10 Aug 2020 16:45:35 +0200
Subject: [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
---
 test-suite/micromega/bug_12790.v | 8 ++++++++
 1 file changed, 8 insertions(+)
 create mode 100644 test-suite/micromega/bug_12790.v

(limited to 'test-suite')

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.
-- 
cgit v1.2.3