From 4cf8c3c2a02dd29f98ec0e7a2fb31ed71a1a2939 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Thu, 19 Jun 2014 18:24:00 -0700
Subject: Fixed crash in resolver

---
 Test/test0/LineResolve.bpl        | 5 +++++
 Test/test0/LineResolve.bpl.expect | 3 ++-
 2 files changed, 7 insertions(+), 1 deletion(-)

(limited to 'Test/test0')

diff --git a/Test/test0/LineResolve.bpl b/Test/test0/LineResolve.bpl
index da1a5bfa..39bf9983 100644
--- a/Test/test0/LineResolve.bpl
+++ b/Test/test0/LineResolve.bpl
@@ -38,3 +38,8 @@ l+  // error: A B C . txt(12,0)
 
 0;
 }
+
+#line 100 LineResolve.bpl
+procedure ResolutionTest() {
+  x := 0;  // error: undeclared identifier (once upon a time, this used to crash Boogie)
+}
diff --git a/Test/test0/LineResolve.bpl.expect b/Test/test0/LineResolve.bpl.expect
index 6ca45551..1e5b4eb7 100644
--- a/Test/test0/LineResolve.bpl.expect
+++ b/Test/test0/LineResolve.bpl.expect
@@ -10,4 +10,5 @@ Abc.txt(13,0): Error: undeclared identifier: i
 Abc.txt(99,0): Error: undeclared identifier: j
 c:\Users\leino\Documents\Programs\MyClass.ssc(104,0): Error: undeclared identifier: k
 A B C . txt(12,0): Error: undeclared identifier: l
-12 name resolution errors detected in LineResolve.bpl
+LineResolve.bpl(101,2): Error: undeclared identifier: x
+13 name resolution errors detected in LineResolve.bpl
-- 
cgit v1.2.3