diff --git a/Duper/Tests/bugs.lean b/Duper/Tests/bugs.lean
index 5b9944f..6b1ea10 100644
--- a/Duper/Tests/bugs.lean
+++ b/Duper/Tests/bugs.lean
@@ -88,3 +88,18 @@ argument has type
 but function has type
   Type u_2 → Type u_2
 -/
+
+-- Bug 8
+set_option trace.Saturate.debug true in
+example (h1 : ∀ x : Nat, x > 0 → ∃ y : Fin x, y.1 = 0) (h2 : 3 > 0) : ∃ z : Fin 3, z.1 = 0 := by
+  duper [h1, h2]
+
+/-
+The final active set contains both of the following clauses:
+- ∀ (a : Fin 3), a.1 ≠ 0
+- ∀ (a : Fin 3), (skS.0 Type 0 ((x_0 : Nat) → Fin x_0 → Fin x_0) 3 a).1 = 0
+
+If it were possible to unify `a` from the first clause with `(skS.0 Type 0 ((x_0 : Nat) → Fin x_0 → Fin x_0) 3 a)` from
+the second clause, then duper would be able to derive a contradiction. However, the current manner in which skolem symbols
+are constructed prevents this.
+-/