From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- test-suite/bugs/closed/5359.v | 218 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 218 insertions(+) create mode 100644 test-suite/bugs/closed/5359.v (limited to 'test-suite/bugs/closed/5359.v') 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))). -- cgit v1.2.3