From 1ef6104cf043ec839059cddfe530a81418a3d474 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 7 Jul 2016 13:45:32 +0200
Subject: Add test file for #4880.

---
 test-suite/bugs/closed/4880.v | 11 +++++++++++
 1 file changed, 11 insertions(+)
 create mode 100644 test-suite/bugs/closed/4880.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/4880.v b/test-suite/bugs/closed/4880.v
new file mode 100644
index 0000000000..5569798d54
--- /dev/null
+++ b/test-suite/bugs/closed/4880.v
@@ -0,0 +1,11 @@
+Require Import Coq.Reals.Reals Coq.nsatz.Nsatz.
+Local Open Scope R.
+
+Goal forall x y : R,
+  x*x =  y *  y ->
+  x*x = -y * -y ->
+  x*(x*x) = 0 -> (* The associativity does not actually matter, *)
+  (x*x)*x = 0.   (* just otherwise [assumption] would solve the goal. *)
+Proof.
+  nsatz.
+Qed.
-- 
cgit v1.2.3


From 88f4ca3d1798fc28f230f749665bcf48597accc3 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 7 Jul 2016 13:48:20 +0200
Subject: Test file for #4858.

---
 test-suite/bugs/closed/4858.v | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 test-suite/bugs/closed/4858.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/4858.v b/test-suite/bugs/closed/4858.v
new file mode 100644
index 0000000000..c04895a1bb
--- /dev/null
+++ b/test-suite/bugs/closed/4858.v
@@ -0,0 +1,7 @@
+Require Import Nsatz.
+Goal True.
+nsatz_compute
+ (PEc 0%Z :: PEc (-1)%Z
+    :: PEpow (PEsub (PEX Z 2) (PEX Z 3)) 1
+       :: PEsub (PEX Z 1) (PEX Z 1) :: nil).
+Abort.
-- 
cgit v1.2.3


From e1661dc9a43b34526437e9bc3029e6320e09f899 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 8 Jul 2016 13:03:16 +0200
Subject: Fix test file for #4858.

---
 test-suite/bugs/closed/4858.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/4858.v b/test-suite/bugs/closed/4858.v
index c04895a1bb..a2fa93832a 100644
--- a/test-suite/bugs/closed/4858.v
+++ b/test-suite/bugs/closed/4858.v
@@ -1,6 +1,6 @@
 Require Import Nsatz.
 Goal True.
-nsatz_compute
+try nsatz_compute
  (PEc 0%Z :: PEc (-1)%Z
     :: PEpow (PEsub (PEX Z 2) (PEX Z 3)) 1
        :: PEsub (PEX Z 1) (PEX Z 1) :: nil).
-- 
cgit v1.2.3