summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/5359.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/bugs/closed/5359.v')
-rw-r--r--test-suite/bugs/closed/5359.v218
1 files changed, 218 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/5359.v b/test-suite/bugs/closed/5359.v
new file mode 100644
index 00000000..87e69565
--- /dev/null
+++ b/test-suite/bugs/closed/5359.v
@@ -0,0 +1,218 @@
+Require Import Coq.nsatz.Nsatz.
+Goal False.
+
+ (* the first (succeeding) goal was reached by clearing one hypothesis in the second goal which overflows 6GB of stack space *)
+ let sugar := constr:( 0%Z ) in
+ let nparams := constr:( (-1)%Z ) in
+ let reified_goal := constr:(
+ (Ring_polynom.PEsub (Ring_polynom.PEc 1%Z)
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 4) (Ring_polynom.PEX Z 2))
+ (Ring_polynom.PEX Z 5)) (Ring_polynom.PEX Z 3))
+ (Ring_polynom.PEX Z 6))) ) in
+ let power := constr:( N.one ) in
+ let reified_givens := constr:(
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEadd (Ring_polynom.PEc 1%Z)
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 4) (Ring_polynom.PEX Z 2))
+ (Ring_polynom.PEX Z 5)) (Ring_polynom.PEX Z 3))
+ (Ring_polynom.PEX Z 6)))
+ (Ring_polynom.PEsub (Ring_polynom.PEc 1%Z)
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 4) (Ring_polynom.PEX Z 2))
+ (Ring_polynom.PEX Z 5)) (Ring_polynom.PEX Z 3))
+ (Ring_polynom.PEX Z 6)))
+ :: Ring_polynom.PEsub
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEadd (Ring_polynom.PEc 1%Z)
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 4)
+ (Ring_polynom.PEX Z 2)) (Ring_polynom.PEX Z 5))
+ (Ring_polynom.PEX Z 3)) (Ring_polynom.PEX Z 6)))
+ (Ring_polynom.PEX Z 10)) (Ring_polynom.PEc 1%Z)
+ :: Ring_polynom.PEsub
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEsub (Ring_polynom.PEc 1%Z)
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 4)
+ (Ring_polynom.PEX Z 2)) (Ring_polynom.PEX Z 5))
+ (Ring_polynom.PEX Z 3)) (Ring_polynom.PEX Z 6)))
+ (Ring_polynom.PEX Z 9)) (Ring_polynom.PEc 1%Z)
+ :: Ring_polynom.PEsub
+ (Ring_polynom.PEadd
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 1)
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 7)
+ (Ring_polynom.PEX Z 7)))
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 8) (Ring_polynom.PEX Z 8)))
+ (Ring_polynom.PEadd (Ring_polynom.PEc 1%Z)
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 4)
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 7)
+ (Ring_polynom.PEX Z 7)))
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 8)
+ (Ring_polynom.PEX Z 8))))
+ :: Ring_polynom.PEsub
+ (Ring_polynom.PEadd
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 1)
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 5)
+ (Ring_polynom.PEX Z 5)))
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 6)
+ (Ring_polynom.PEX Z 6)))
+ (Ring_polynom.PEadd (Ring_polynom.PEc 1%Z)
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 4)
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 5)
+ (Ring_polynom.PEX Z 5)))
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 6)
+ (Ring_polynom.PEX Z 6))))
+ :: Ring_polynom.PEsub
+ (Ring_polynom.PEadd
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 1)
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 2)
+ (Ring_polynom.PEX Z 2)))
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 3)
+ (Ring_polynom.PEX Z 3)))
+ (Ring_polynom.PEadd (Ring_polynom.PEc 1%Z)
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 4)
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 2)
+ (Ring_polynom.PEX Z 2)))
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 3)
+ (Ring_polynom.PEX Z 3)))) :: nil)%list ) in
+ Nsatz.nsatz_compute
+ (@cons _ (@Ring_polynom.PEc _ sugar) (@cons _ (@Ring_polynom.PEc _ nparams) (@cons _ (@Ring_polynom.PEpow _ reified_goal power) reified_givens))).
+
+ let sugar := constr:( 0%Z ) in
+ let nparams := constr:( (-1)%Z ) in
+ let reified_goal := constr:(
+ (Ring_polynom.PEsub (Ring_polynom.PEc 1%Z)
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 4) (Ring_polynom.PEX Z 2))
+ (Ring_polynom.PEX Z 5)) (Ring_polynom.PEX Z 3))
+ (Ring_polynom.PEX Z 6))) ) in
+ let power := constr:( N.one ) in
+ let reified_givens := constr:(
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEadd (Ring_polynom.PEc 1%Z)
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 4) (Ring_polynom.PEX Z 2))
+ (Ring_polynom.PEX Z 5)) (Ring_polynom.PEX Z 3))
+ (Ring_polynom.PEX Z 6)))
+ (Ring_polynom.PEsub (Ring_polynom.PEc 1%Z)
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 4) (Ring_polynom.PEX Z 2))
+ (Ring_polynom.PEX Z 5)) (Ring_polynom.PEX Z 3))
+ (Ring_polynom.PEX Z 6)))
+ :: Ring_polynom.PEadd
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEadd (Ring_polynom.PEc 1%Z)
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 4)
+ (Ring_polynom.PEX Z 2)) (Ring_polynom.PEX Z 5))
+ (Ring_polynom.PEX Z 3)) (Ring_polynom.PEX Z 6)))
+ (Ring_polynom.PEsub (Ring_polynom.PEc 1%Z)
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 4)
+ (Ring_polynom.PEX Z 2)) (Ring_polynom.PEX Z 5))
+ (Ring_polynom.PEX Z 3)) (Ring_polynom.PEX Z 6))))
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 4)
+ (Ring_polynom.PEadd
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 2)
+ (Ring_polynom.PEX Z 6))
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 3)
+ (Ring_polynom.PEX Z 5)))) (Ring_polynom.PEX Z 7))
+ (Ring_polynom.PEsub
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 3) (Ring_polynom.PEX Z 6))
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 1)
+ (Ring_polynom.PEX Z 2)) (Ring_polynom.PEX Z 5))))
+ (Ring_polynom.PEX Z 8))
+ :: Ring_polynom.PEsub
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEadd (Ring_polynom.PEc 1%Z)
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 4)
+ (Ring_polynom.PEX Z 2)) (Ring_polynom.PEX Z 5))
+ (Ring_polynom.PEX Z 3)) (Ring_polynom.PEX Z 6)))
+ (Ring_polynom.PEX Z 10)) (Ring_polynom.PEc 1%Z)
+ :: Ring_polynom.PEsub
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEsub (Ring_polynom.PEc 1%Z)
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 4)
+ (Ring_polynom.PEX Z 2))
+ (Ring_polynom.PEX Z 5)) (Ring_polynom.PEX Z 3))
+ (Ring_polynom.PEX Z 6))) (Ring_polynom.PEX Z 9))
+ (Ring_polynom.PEc 1%Z)
+ :: Ring_polynom.PEsub
+ (Ring_polynom.PEadd
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 1)
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 7)
+ (Ring_polynom.PEX Z 7)))
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 8)
+ (Ring_polynom.PEX Z 8)))
+ (Ring_polynom.PEadd (Ring_polynom.PEc 1%Z)
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 4)
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 7)
+ (Ring_polynom.PEX Z 7)))
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 8)
+ (Ring_polynom.PEX Z 8))))
+ :: Ring_polynom.PEsub
+ (Ring_polynom.PEadd
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 1)
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 5)
+ (Ring_polynom.PEX Z 5)))
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 6)
+ (Ring_polynom.PEX Z 6)))
+ (Ring_polynom.PEadd (Ring_polynom.PEc 1%Z)
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 4)
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 5)
+ (Ring_polynom.PEX Z 5)))
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 6)
+ (Ring_polynom.PEX Z 6))))
+ :: Ring_polynom.PEsub
+ (Ring_polynom.PEadd
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 1)
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 2)
+ (Ring_polynom.PEX Z 2)))
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 3)
+ (Ring_polynom.PEX Z 3)))
+ (Ring_polynom.PEadd (Ring_polynom.PEc 1%Z)
+ (Ring_polynom.PEmul
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 4)
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 2)
+ (Ring_polynom.PEX Z 2)))
+ (Ring_polynom.PEmul (Ring_polynom.PEX Z 3)
+ (Ring_polynom.PEX Z 3)))) :: nil)%list ) in
+ Nsatz.nsatz_compute
+ (@cons _ (@Ring_polynom.PEc _ sugar) (@cons _ (@Ring_polynom.PEc _ nparams) (@cons _ (@Ring_polynom.PEpow _ reified_goal power) reified_givens))).
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-07 14:53:24 +0000