Add repro for #3236

tests/bug-reports/Bug3236.fst

@@ -0,0 +1,33 @@
+module Bug3236
+
+#set-options "--defensive error"
+
+open FStar.Tactics.V2
+
+val fa_cong : unit -> unit
+let fa_cong (u1:unit) =
+  let do1 (u2:unit) : Tac unit =
+    let t = (`()) in
+    let l = Cons #term t Nil in
+    ()
+  in
+  ()
+
+val ex_cong : unit -> unit
+let ex_cong () =
+  let t () : Tac unit =
+    admit();
+    let [ex] = l_intros () in
+    ()
+  in
+  ()
+
+val is_true : term -> Tac bool
+let is_true t =
+    begin match term_as_formula' t with
+    | True_ -> true
+    | x1 -> begin match inspect t with
+           | Tv_App l r -> true
+           | x2 -> false
+           end
+    end

tests/bug-reports/Makefile

@@ -55,7 +55,7 @@ SHOULD_VERIFY_CLOSED=Bug022.fst Bug024.fst Bug025.fst Bug026.fst Bug026b.fst Bug
   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 \
-  Bug3213.fst Bug3213b.fst Bug3207.fst Bug3207b.fst Bug3207c.fst Bug2155.fst Bug3224a.fst Bug3224b.fst
+  Bug3213.fst Bug3213b.fst Bug3207.fst Bug3207b.fst Bug3207c.fst Bug2155.fst Bug3224a.fst Bug3224b.fst Bug3236.fst
 
 SHOULD_VERIFY_INTERFACE_CLOSED=Bug771.fsti Bug771b.fsti
 SHOULD_VERIFY_AND_WARN_CLOSED=Bug016.fst