4 files changed, 56 insertions, 2 deletions
diff --git a/test-suite/bugs/closed/bug_4836.v b/test-suite/bugs/closed/bug_4836.v
index 5838dcd8a7..9aefb10172 100644
--- a/test-suite/bugs/closed/bug_4836.v
+++ b/test-suite/bugs/closed/bug_4836.v
@@ -1 +1 @@
-(* -*- coq-prog-args: ("-compile" "bugs/closed/PLACEHOLDER.v") -*- *)
+(* -*- coq-prog-args: ("bugs/closed/PLACEHOLDER.v") -*- *)
diff --git a/test-suite/bugs/closed/bug_7811.v b/test-suite/bugs/closed/bug_7811.v
index fee330f22d..155f3285b7 100644
--- a/test-suite/bugs/closed/bug_7811.v
+++ b/test-suite/bugs/closed/bug_7811.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-top" "atomic" "-Q" "." "iris" "-R" "." "stdpp") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-top" "atomic" "-Q" "." "iris" "-R" "." "stdpp") -*- *)
 (* File reduced by coq-bug-finder from original input, then from 140 lines to 26 lines, then from 141 lines to 27 lines, then from 142 lines to 27 lines, then from 272 lines to 61 lines, then from 291 lines to 94 lines, then from 678 lines to 142 lines, then from 418 lines to 161 lines, then from 538 lines to 189 lines, then from 840 lines to 493 lines, then from 751 lines to 567 lines, then from 913 lines to 649 lines, then from 875 lines to 666 lines, then from 784 lines to 568 lines, then from 655 lines to 173 lines, then from 317 lines to 94 lines, then from 172 lines to 86 lines, then from 102 lines to 86 lines, then from 130 lines to 86 lines, then from 332 lines to 112 lines, then from 279 lines to 111 lines, then from 3996 lines to 5697 lines, then from 153 lines to 117 lines, then from 146 lines to 108 lines, then from 124 lines to 108 lines *)
 (* coqc version 8.8.0 (May 2018) compiled on May 2 2018 16:49:46 with OCaml 4.02.3
    coqtop version 8.8.0 (May 2018) *)
diff --git a/test-suite/bugs/closed/bug_9268.v b/test-suite/bugs/closed/bug_9268.v
new file mode 100644
index 0000000000..02dd46f6d2
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9268.v
@@ -0,0 +1,46 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Coq.micromega.Lia.
+
+Local Open Scope Z_scope.
+
+Definition Register := Z%type.
+
+Definition Opcode := Z%type.
+
+Inductive InstructionI : Type
+  := Lb : Register -> Register -> Z -> InstructionI
+  |  InvalidI : InstructionI.
+
+Inductive Instruction : Type
+  := IInstruction : InstructionI -> Instruction.
+
+Definition funct3_LB : Z := 0.
+
+Definition opcode_LOAD : Opcode := 3.
+
+Set Universe Polymorphism.
+
+Definition MachineInt := Z.
+
+Definition funct3_JALR := 0.
+
+Axiom InstructionMapper: Type -> Type.
+
+Definition apply_InstructionMapper(mapper: InstructionMapper Z)(inst: Instruction): Z :=
+  match inst with
+  | IInstruction   InvalidI   => 2
+  | IInstruction   (Lb  rd rs1 oimm12) => 3
+   end.
+
+Axiom Encoder: InstructionMapper MachineInt.
+
+Definition encode: Instruction -> MachineInt := apply_InstructionMapper Encoder.
+
+Lemma foo: forall (ins: InstructionI),
+    0 <= encode (IInstruction ins) ->
+    0 <= encode (IInstruction ins) .
+Proof.
+  Set Printing Universes.
+  intros.
+  lia.
+Qed.
diff --git a/test-suite/bugs/closed/bug_9451.v b/test-suite/bugs/closed/bug_9451.v
new file mode 100644
index 0000000000..03bb0433f1
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9451.v
@@ -0,0 +1,8 @@
+Goal False.
+cut True.
+assert False.
+evar (x : True).
+let v := open_constr:(_) in idtac. all: exfalso; clear.
+Optimize Proof.
+(* Error: Anomaly "grounding a non evar-free term" *)
+Abort All.