From e68ffb4d0ffa949562b0a6a15e832ebae2875cab Mon Sep 17 00:00:00 2001
From: Andres Erbsen
Date: Mon, 3 Feb 2020 17:07:11 -0500
Subject: add regression test for lia

---
 test-suite/micromega/evars_loops_in_8_10_fixed_8_11.v | 4 ++++
 1 file changed, 4 insertions(+)
 create mode 100644 test-suite/micromega/evars_loops_in_8_10_fixed_8_11.v

diff --git a/test-suite/micromega/evars_loops_in_8_10_fixed_8_11.v b/test-suite/micromega/evars_loops_in_8_10_fixed_8_11.v
new file mode 100644
index 0000000000..a53c160e45
--- /dev/null
+++ b/test-suite/micromega/evars_loops_in_8_10_fixed_8_11.v
@@ -0,0 +1,4 @@
+Require Import Lia.
+Goal forall n (B: n >= 0), exists Goal1 Goal2 Goal3,
+  (0 * (Goal1 * Goal2 + Goal1) <> Goal3 * 0 * (Goal1 * S Goal2)).
+Proof. eexists _, _, _. Fail lia. Abort.
-- 
cgit v1.2.3