Add a test

FStarLang · Oct 13, 2024 · 6c0788d · 6c0788d
1 parent b12031f
commit 6c0788d
Show file tree

Hide file tree

Showing 4 changed files with 13 additions and 1 deletion.
diff --git a/tests/bug-reports/Bug3559a.fst b/tests/bug-reports/Bug3559a.fst
@@ -0,0 +1,4 @@
+module Bug3559a
+
+let a = "A.a"
+let b = "A.b"
diff --git a/tests/bug-reports/Bug3559b.fst b/tests/bug-reports/Bug3559b.fst
@@ -0,0 +1,4 @@
+module Bug3559b
+let a = "B.a"
+let b = "B.b"
+include Bug3559a {a}
diff --git a/tests/bug-reports/Bug3559c.fst b/tests/bug-reports/Bug3559c.fst
@@ -0,0 +1,4 @@
+module Bug3559c
+include Bug3559b
+let _ = assert (a == "A.a")
+let _ = assert (b == "B.b")
diff --git a/tests/bug-reports/Makefile b/tests/bug-reports/Makefile
@@ -80,7 +80,7 @@ SHOULD_VERIFY_CLOSED=\
 	Bug2155.fst Bug3224a.fst Bug3224b.fst Bug3236.fst Bug3252.fst \
 	BugBoxInjectivity.fst BugTypeParamProjector.fst Bug2172.fst Bug3266.fst		\
 	Bug3264a.fst Bug3264b.fst Bug3286a.fst Bug3286b.fst Bug3320.fst Bug2583.fst \
-	Bug2419.fst Bug3353.fst Bug3426.fst Bug3530.fst
+	Bug2419.fst Bug3353.fst Bug3426.fst Bug3530.fst Bug3559c.fst
 
 
 SHOULD_VERIFY_INTERFACE_CLOSED=Bug771.fsti Bug771b.fsti