1 files changed, 15 insertions, 0 deletions
diff --git a/Test/test2/BadLineNumber.bpl b/Test/test2/BadLineNumber.bpl
new file mode 100644
index 00000000..b8776a4e
--- /dev/null
+++ b/Test/test2/BadLineNumber.bpl
@@ -0,0 +1,15 @@
+// RUN: %boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+procedure p();
+  ensures false;
+
+implementation p()
+{
+    if (*)
+    {
+    }
+    else
+    {
+    }
+}
+\ No newline at end of file