1 files changed, 38 insertions, 0 deletions
diff --git a/Test/test0/LineResolve.bpl b/Test/test0/LineResolve.bpl
new file mode 100644
index 00000000..b0c578c7
--- /dev/null
+++ b/Test/test0/LineResolve.bpl
@@ -0,0 +1,38 @@
+procedure P() {
+var x: int;
+x :=
+
+ a+  // error: LineResolve.bpl(5,1)
+
+  b+  // error: LineResolve.bpl(7,2)
+#line 12
+c+ // error: LineResolve.bpl(12,0)
+          d+ // error: LineResolve.bpl(13,10)
+#line 12
+e+ // error: LineResolve.bpl(12,0)
+#line 2
+f+ // error: LineResolve.bpl(2,0)
+#line    1000          
+#line 900
+g+ // error: LineResolve.bpl(900,0)
+
+#line 10    Abc.txt
+
+   h+   // error: Abc.txt(11,3)
+
+i+ // error: Abc.txt(13,0)
+#line 98
+
+j+  // error: Abc.txt(99,0)
+
+#line                103       c:\Users\leino\Documents\Programs\MyClass.ssc  
+
+k+ // error: c:\Users\leino\Documents\Programs\MyClass.ssc(104,0)
+
+#line -58
+
+#line 12 A B C . txt     
+l+  // error: A B C . txt(12,0)
+
+0;
+}