tests: Add repro for FStarLang#3213

tests/bug-reports/Bug3213.fst

@@ -0,0 +1,25 @@
+module Bug3213
+
+#set-options "--debug Test --debug_level SMTQuery"
+
+let ff = nat -> Type0
+
+let bad2 ()
+  : Lemma (forall (f : ff). (forall (x : nat). f x) ==> (fun (_:nat) -> True) == f) = ()
+
+[@@expect_failure [19]]
+let bad ()
+  : Lemma (forall (f : int -> Type0). (forall (x : nat). f x) ==> f (-1)) = ()
+
+(* Replaying unsoundness from an axiom *)
+let bad_assumed ()
+  : Lemma (forall (f : int -> Type0). (forall (x : nat). f x) ==> f (-1)) = admit()
+
+let forall_elim (#a: Type) (p: (a -> GTot Type)) (x:a)
+  : Lemma (requires forall (x: a). p x) (ensures p x) = ()
+
+let falso () : Lemma False =
+  bad_assumed();
+  let f (x:int) : Type0 = x >= 0 in
+  forall_elim #(int -> Type0) (fun f -> (forall (x : nat). f x) ==> f (-1)) f;
+  ()

tests/bug-reports/Makefile

@@ -54,7 +54,8 @@ SHOULD_VERIFY_CLOSED=Bug022.fst Bug024.fst Bug025.fst Bug026.fst Bug026b.fst Bug
   Bug2756.fst MutualRecPositivity.fst Bug2806a.fst Bug2806b.fst Bug2806c.fst Bug2806d.fst Bug2809.fst\
   Bug2849a.fst Bug2849b.fst Bug2045.fst Bug2876.fst Bug2882.fst Bug2895.fst Bug2894.fst \
   Bug2415.fst Bug3028.fst Bug2954.fst Bug3089.fst Bug3102.fst Bug2981.fst Bug2980.fst Bug3115.fst \
-  Bug2083.fst Bug2002.fst Bug1482.fst Bug1066.fst Bug3120a.fst Bug3120b.fst Bug3186.fst Bug3185.fst Bug3210.fst
+  Bug2083.fst Bug2002.fst Bug1482.fst Bug1066.fst Bug3120a.fst Bug3120b.fst Bug3186.fst Bug3185.fst Bug3210.fst \
+  Bug3213.fst
 
 SHOULD_VERIFY_INTERFACE_CLOSED=Bug771.fsti Bug771b.fsti
 SHOULD_VERIFY_AND_WARN_CLOSED=Bug016.fst