Add repro for FStarLang#3238

mtzguido · Apr 10, 2024 · 95b0330 · 95b0330
1 parent 9aa1de2
commit 95b0330
Show file tree

Hide file tree

Showing 2 changed files with 15 additions and 1 deletion.
diff --git a/tests/bug-reports/Bug3238.fst b/tests/bug-reports/Bug3238.fst
@@ -0,0 +1,13 @@
+module Bug3238
+
+open FStar.Range
+
+assume val p : range -> prop
+
+assume val lem : r:range -> Lemma (p r)
+
+let test () : range =
+  let r = normalize_term (mk_range "asd" 1 2 3 4) in
+  Classical.forall_intro lem;
+  assert (p r);
+  r
diff --git a/tests/bug-reports/Makefile b/tests/bug-reports/Makefile
@@ -55,7 +55,8 @@ 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 Bug3236.fst
+  Bug3213.fst Bug3213b.fst Bug3207.fst Bug3207b.fst Bug3207c.fst Bug2155.fst Bug3224a.fst Bug3224b.fst Bug3236.fst \
+  Bug3238.fst
 
 SHOULD_VERIFY_INTERFACE_CLOSED=Bug771.fsti Bug771b.fsti
 SHOULD_VERIFY_AND_WARN_CLOSED=Bug016.fst