Some unresolved existential variables remain

Some unresolved existential variables remain

Using opam switch '4.14.1+flambda'

which ocamlfind: '/root/.opamcache/4.14.1+flambda/bin/ocamlfind'

ocamlfind ocamlopt -v: The OCaml native-code compiler, version 4.14.1 Standard library directory: /root/.opamcache/4.14.1+flambda/lib/ocaml

download failing artifacts @ cecd17315cceead371ebd704ec97df139dad33e8 https://gitlab.com/coq/coq/-/jobs/4437684128/artifacts/download https://gitlab.com/coq/coq/-/jobs/4437684172/artifacts/download

download passing artifacts @ 6e739ce1f8ec685f7e409f0799a894c45c4325ea https://gitlab.com/coq/coq/-/jobs/4436252752/artifacts/download https://gitlab.com/coq/coq/-/jobs/4436253439/artifacts/download

/github/workspace/builds/coq/coq-failing/_install_ci/bin/coqc -config: COQLIB=/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/ COQCORELIB=/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/../coq-core/ DOCDIR=/builds/coq/coq/_install_ci/share/doc/ OCAMLFIND=/root/.opamcache/4.14.1+flambda/bin/ocamlfind CAMLFLAGS=-thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 WARN=-warn-error +a-3 HASNATDYNLINK=true COQ_SRC_SUBDIRS=boot config lib clib kernel library engine pretyping interp gramlib parsing proofs tactics toplevel printing ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/funind plugins/ltac plugins/ltac2 plugins/micromega plugins/nsatz plugins/ring plugins/rtauto plugins/ssr plugins/ssrmatching plugins/syntax COQ_NATIVE_COMPILER_DEFAULT=yes

/github/workspace/builds/coq/coq-passing/_install_ci/bin/coqc -config: COQLIB=/github/workspace/builds/coq/coq-passing/_install_ci/lib/coq/ COQCORELIB=/github/workspace/builds/coq/coq-passing/_install_ci/lib/coq/../coq-core/ DOCDIR=/builds/coq/coq/_install_ci/share/doc/ OCAMLFIND=/root/.opamcache/4.14.1+flambda/bin/ocamlfind CAMLFLAGS=-thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 WARN=-warn-error +a-3 HASNATDYNLINK=true COQ_SRC_SUBDIRS=boot config lib clib kernel library engine pretyping interp gramlib parsing proofs tactics toplevel printing ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/funind plugins/ltac plugins/ltac2 plugins/micromega plugins/nsatz plugins/ring plugins/rtauto plugins/ssr plugins/ssrmatching plugins/syntax COQ_NATIVE_COMPILER_DEFAULT=yes

Running command /usr/bin/python3 /github/workspace/coq-tools/find-bug.py -y /github/workspace/cwd/bug_01.v /github/workspace/cwd/bug_01.v /github/workspace/cwd/tmp.v --no-deps --ignore-coq-prog-args --inline-user-contrib --coqc=/github/workspace/builds/coq/coq-failing/_install_ci/bin/coqc.orig --coqtop=/github/workspace/builds/coq/coq-failing/_install_ci/bin/coqtop.orig --coq_makefile=/github/workspace/builds/coq/coq-passing/_install_ci/bin/coq_makefile --coqdep /github/workspace/builds/coq/coq-passing/_install_ci/bin/coqdep --base-dir=/github/workspace/builds/coq/coq-failing/_build_ci/ -Q /github/workspace/cwd Top --verbose-include-failure-warning --verbose-include-failure-warning-prefix ::warning:: --verbose-include-failure-warning-newline --nonpassing-arg=-q --nonpassing-arg=-w --nonpassing-arg=+implicit-core-hint-db\,+implicits-in-term\,+non-reversible-notation\,+deprecated-intros-until-0\,+deprecated-focus\,+unused-intro-pattern\,+variable-collision\,+unexpected-implicit-declaration\,+omega-is-deprecated\,+deprecated-instantiate-syntax\,+non-recursive\,+undeclared-scope\,+deprecated-hint-rewrite-without-locality\,+deprecated-hint-without-locality\,+deprecated-instance-without-locality\,+deprecated-typeclasses-transparency-without-locality\,unsupported-attributes --nonpassing-arg=-w --nonpassing-arg=-notation-overridden\,-deprecated-hint-constr\,-fragile-hint-constr\,-native-compiler-disabled\,-ambiguous-paths\,-masking-absolute-name --nonpassing-arg=-w --nonpassing-arg=-deprecated-native-compiler-option --nonpassing-arg=-native-compiler --nonpassing-arg=ondemand --nonpassing-Q /github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/deps/coqutil/src/coqutil coqutil --nonpassing-Q /github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/src/Rupicola Rupicola --nonpassing-Q /github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/bedrock2/src/bedrock2 bedrock2 --nonpassing-Q /github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/bedrock2/src/bedrock2Examples bedrock2Examples --nonpassing-Q /github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/compiler/src/compiler compiler --nonpassing-Q /github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv riscv --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/src Crypto --passing-coqc=/github/workspace/builds/coq/coq-passing/_install_ci/bin/coqc.orig --passing-coqtop=/github/workspace/builds/coq/coq-passing/_install_ci/bin/coqtop.orig --passing-base-dir=/github/workspace/builds/coq/coq-passing/_build_ci/ --passing-arg=-q --passing-arg=-w --passing-arg=+implicit-core-hint-db\,+implicits-in-term\,+non-reversible-notation\,+deprecated-intros-until-0\,+deprecated-focus\,+unused-intro-pattern\,+variable-collision\,+unexpected-implicit-declaration\,+omega-is-deprecated\,+deprecated-instantiate-syntax\,+non-recursive\,+undeclared-scope\,+deprecated-hint-rewrite-without-locality\,+deprecated-hint-without-locality\,+deprecated-instance-without-locality\,+deprecated-typeclasses-transparency-without-locality\,unsupported-attributes --passing-arg=-w --passing-arg=-notation-overridden\,-deprecated-hint-constr\,-fragile-hint-constr\,-native-compiler-disabled\,-ambiguous-paths\,-masking-absolute-name --passing-arg=-w --passing-arg=-deprecated-native-compiler-option --passing-arg=-native-compiler --passing-arg=ondemand --passing-Q /github/workspace/builds/coq/coq-passing/_build_ci/fiat_crypto/rupicola/bedrock2/deps/coqutil/src/coqutil coqutil --passing-Q /github/workspace/builds/coq/coq-passing/_build_ci/fiat_crypto/rupicola/src/Rupicola Rupicola --passing-Q /github/workspace/builds/coq/coq-passing/_build_ci/fiat_crypto/rupicola/bedrock2/bedrock2/src/bedrock2 bedrock2 --passing-Q /github/workspace/builds/coq/coq-passing/_build_ci/fiat_crypto/rupicola/bedrock2/bedrock2/src/bedrock2Examples bedrock2Examples --passing-Q /github/workspace/builds/coq/coq-passing/_build_ci/fiat_crypto/rupicola/bedrock2/compil

::warning::Failed to inline Rewriter.Util.plugins.RewriterBuildRegistry via Include, stripping Requires and preserve the error. The new error was: File "/tmp/tmpvmi23n4_/Top/bug_01.v", line 340, characters 0-9: Warning: Let definition cast_outside_of_range declared as an axiom. [let-as-axiom,vernacular,default] File "/tmp/tmpvmi23n4_/Top/bug_01.v", line 550, characters 2-230: Error: Anomaly "Uncaught exception Not_found." Please report at http://coq.inria.fr/bugs/. The file generating the error was: (* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-w" "+implicit-core-hint-db,+implicits-in-term,+non-reversible-notation,+deprecated-intros-until-0,+deprecated-focus,+unused-intro-pattern,+variable-collision,+unexpected-implicit-declaration,+omega-is-deprecated,+deprecated-instantiate-syntax,+non-recursive,+undeclared-scope,+deprecated-hint-rewrite-without-locality,+deprecated-hint-without-locality,+deprecated-instance-without-locality,+deprecated-typeclasses-transparency-without-locality,unsupported-attributes" "-w" "-notation-overridden,-deprecated-hint-constr,-fragile-hint-constr,-native-compiler-disabled,-ambiguous-paths,-masking-absolute-name" "-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/src" "Crypto" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/deps/coqutil/src/coqutil" "coqutil" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/src/Rupicola" "Rupicola" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/bedrock2/src/bedrock2" "bedrock2" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/bedrock2/src/bedrock2Examples" "bedrock2Examples" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/compiler/src/compiler" "compiler" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv" "riscv" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Bignums" "Bignums" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Coqprime" "Coqprime" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Ltac2" "Ltac2" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Rewriter" "Rewriter" "-top" "Top.bug_01") -*- *) (* File reduced by coq-bug-minimizer from original input, then from 1498 lines to 11 lines, then from 24 lines to 324 lines, then from 329 lines to 52 lines, then from 65 lines to 384 lines, then from 389 lines to 57 lines, then from 70 lines to 840 lines, then from 845 lines to 118 lines, then from 131 lines to 380 lines, then from 385 lines to 130 lines, then from 143 lines to 339 lines, then from 344 lines to 132 lines, then from 150 lines to 132 lines, then from 145 lines to 478 lines, then from 484 lines to 255 lines, then from 269 lines to 501 lines, then from 506 lines to 351 lines, then from 365 lines to 694 lines, then from 699 lines to 825 lines, then from 833 lines to 357 lines, then from 370 lines to 564 lines, then from 570 lines to 377 lines, then from 391 lines to 987 lines, then from 992 lines to 377 lines, then from 391 lines to 3948 lines, then from 3948 lines to 4401 lines, then from 4405 lines to 389 lines, then from 402 lines to 615 lines, then from 621 lines to 464 lines, then from 478 lines to 431 lines, then from 444 lines to 700 lines, then from 706 lines to 435 lines, then from 449 lines to 476 lines, then from 482 lines to 549 lines, then from 567 lines to 439 lines, then from 452 lines to 668 lines, then from 674 lines to 440 lines, then from 454 lines to 524 lines, then from 530 lines to 442 lines, then from 456 lines to 475 lines, then from 481 lines to 475 lines, then from 493 lines to 444 lines *) (* coqc version 8.18+alpha compiled with OCaml 4.14.1 coqtop version runner-vxtc-u6t-project-6138686-concurrent-0:/builds/coq/coq/_bu