tests: add test for FStarLang#3145

tests/error-messages/Bug3145.fst

@@ -0,0 +1,6 @@
+module Bug3145
+
+let t1 = int * int * int
+let t2 = int * int & int
+let t3 = int & int * int
+let t4 = int & int & int

tests/error-messages/Bug3145.fst.expected

@@ -0,0 +1,47 @@
+Module after desugaring:
+module Bug3145
+Declarations: [
+let t1 = Prims.int & Prims.int & Prims.int
+let t2 = (Prims.int & Prims.int) & Prims.int
+let t3 = Prims.int & (Prims.int & Prims.int)
+let t4 = Prims.int & Prims.int & Prims.int
+]
+Exports: [
+let t1 = Prims.int & Prims.int & Prims.int
+let t2 = (Prims.int & Prims.int) & Prims.int
+let t3 = Prims.int & (Prims.int & Prims.int)
+let t4 = Prims.int & Prims.int & Prims.int
+]
+
+Module before type checking:
+module Bug3145
+Declarations: [
+let t1 = Prims.int & Prims.int & Prims.int
+let t2 = (Prims.int & Prims.int) & Prims.int
+let t3 = Prims.int & (Prims.int & Prims.int)
+let t4 = Prims.int & Prims.int & Prims.int
+]
+Exports: [
+let t1 = Prims.int & Prims.int & Prims.int
+let t2 = (Prims.int & Prims.int) & Prims.int
+let t3 = Prims.int & (Prims.int & Prims.int)
+let t4 = Prims.int & Prims.int & Prims.int
+]
+
+Module after type checking:
+module Bug3145
+Declarations: [
+let t1 = Prims.int & Prims.int & Prims.int
+let t2 = (Prims.int & Prims.int) & Prims.int
+let t3 = Prims.int & (Prims.int & Prims.int)
+let t4 = Prims.int & Prims.int & Prims.int
+]
+Exports: [
+let t1 = Prims.int & Prims.int & Prims.int
+let t2 = (Prims.int & Prims.int) & Prims.int
+let t3 = Prims.int & (Prims.int & Prims.int)
+let t4 = Prims.int & Prims.int & Prims.int
+]
+
+Verified module: Bug3145
+All verification conditions discharged successfully

tests/error-messages/Makefile

@@ -25,6 +25,7 @@ all: check-all
 # matches the expected file.
 Bug1997.fst.output: OTHERFLAGS+=--dump_module Bug1997
 Bug2820.fst.output: OTHERFLAGS+=--dump_module Bug2820
+Bug3145.fst.output: OTHERFLAGS+=--dump_module Bug3145
 Bug3227.fst.output: OTHERFLAGS+=--dump_module Bug3227
 Bug3292.fst.output: OTHERFLAGS+=--dump_module Bug3292
 CalcImpl.fst.output: OTHERFLAGS+=--dump_module CalcImpl