test for #1404

FStarLang · Mar 17, 2018 · e8e8519 · e8e8519
1 parent 124a5db
commit e8e8519
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 1 deletion.
diff --git a/examples/bug-reports/Makefile b/examples/bug-reports/Makefile
@@ -64,7 +64,8 @@ SHOULD_NOT_VERIFY_CLOSED=bug035.fst bug043.fst bug044.fst bug063.fst bug120.fst
   bug156.fst bug163.fst bug176.fst bug177.fst bug183.fst bug250.fst bug253.fst bug253b.fst bug262.fst bug284.fst\
   bug319.fst bug320.fst bug362.fst bug379.fst bug406.fst bug446.fst bug612.fst bug623.fst bug655.fst\
   bug769.fst bug769b.fst bug769d.fst bug1017.fst bug1043.fst bug1043b.fst bug1106.fst bug1106b.fst bug174.fst\
-  bug193.fst bug208.fst bug208.fst bug378.fst bug696.fst bug1090.fst bug1187.fst bug380_1.fst bug380_2.fst
+  bug193.fst bug208.fst bug208.fst bug378.fst bug696.fst bug1090.fst bug1187.fst bug380_1.fst bug380_2.fst \
+  bug1404.fst
 
 # These will not be checked, but the SHOULD_NOT_VERIFY_BROKEN examples are expected to work since their
 # corresponding GitHub issue is closed. Consider re-opening.

diff --git a/examples/bug-reports/bug1404.fst b/examples/bug-reports/bug1404.fst
@@ -0,0 +1,10 @@
+module Bug1404
+
+(* This should fail with :
+ * bug1404.fst(9,6-10,17): (Error 297) Patterns in this match are incoherent, variable y is bound in some but not all patterns.
+ *)
+let f o =
+    match o with
+    | (Some x, _)
+    | (x, Some y) -> y
+    | _ -> false