fixed some tests in og

added another test in linear (based on bug reported by Chris)
removed the QED build configuration

12 files changed, 76 insertions, 197 deletions

diff --git a/Source/Boogie.sln b/Source/Boogie.sln
index 755dc189..0d349f23 100644
--- a/Source/Boogie.sln
+++ b/Source/Boogie.sln
@@ -1,6 +1,8 @@
 

 Microsoft Visual Studio Solution File, Format Version 12.00

-# Visual Studio 2012

+# Visual Studio 2013

+VisualStudioVersion = 12.0.21005.1

+MinimumVisualStudioVersion = 10.0.40219.1

 Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = "Provers", "Provers", "{B758C1E3-824A-439F-AA2F-0BA1143E8C8D}"

 EndProject

 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "BoogieDriver", "BoogieDriver\BoogieDriver.csproj", "{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}"

@@ -49,10 +51,6 @@ Global
 		Debug|Any CPU = Debug|Any CPU

 		Debug|Mixed Platforms = Debug|Mixed Platforms

 		Debug|x86 = Debug|x86

-		QED|.NET = QED|.NET

-		QED|Any CPU = QED|Any CPU

-		QED|Mixed Platforms = QED|Mixed Platforms

-		QED|x86 = QED|x86

 		Release|.NET = Release|.NET

 		Release|Any CPU = Release|Any CPU

 		Release|Mixed Platforms = Release|Mixed Platforms

@@ -76,13 +74,6 @@ Global
 		{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU

 		{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU

 		{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Debug|x86.ActiveCfg = Debug|Any CPU

-		{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.QED|.NET.ActiveCfg = QED|Any CPU

-		{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.QED|Any CPU.ActiveCfg = QED|Any CPU

-		{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.QED|Any CPU.Build.0 = QED|Any CPU

-		{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.QED|Mixed Platforms.ActiveCfg = QED|x86

-		{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.QED|Mixed Platforms.Build.0 = QED|x86

-		{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.QED|x86.ActiveCfg = QED|x86

-		{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.QED|x86.Build.0 = QED|x86

 		{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Release|.NET.ActiveCfg = Release|Any CPU

 		{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Release|Any CPU.ActiveCfg = Release|Any CPU

 		{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Release|Any CPU.Build.0 = Release|Any CPU

@@ -109,13 +100,6 @@ Global
 		{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU

 		{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU

 		{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}.Debug|x86.ActiveCfg = Debug|Any CPU

-		{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}.QED|.NET.ActiveCfg = QED|Any CPU

-		{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}.QED|Any CPU.ActiveCfg = QED|Any CPU

-		{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}.QED|Any CPU.Build.0 = QED|Any CPU

-		{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}.QED|Mixed Platforms.ActiveCfg = QED|x86

-		{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}.QED|Mixed Platforms.Build.0 = QED|x86

-		{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}.QED|x86.ActiveCfg = QED|x86

-		{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}.QED|x86.Build.0 = QED|x86

 		{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}.Release|.NET.ActiveCfg = Release|Any CPU

 		{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}.Release|Any CPU.ActiveCfg = Release|Any CPU

 		{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}.Release|Any CPU.Build.0 = Release|Any CPU

@@ -142,12 +126,6 @@ Global
 		{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU

 		{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU

 		{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Debug|x86.ActiveCfg = Debug|Any CPU

-		{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.QED|.NET.ActiveCfg = QED|Any CPU

-		{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.QED|Any CPU.ActiveCfg = QED|Any CPU

-		{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.QED|Any CPU.Build.0 = QED|Any CPU

-		{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.QED|Mixed Platforms.ActiveCfg = QED|Any CPU

-		{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.QED|Mixed Platforms.Build.0 = QED|Any CPU

-		{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.QED|x86.ActiveCfg = QED|Any CPU

 		{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Release|.NET.ActiveCfg = Release|Any CPU

 		{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Release|Any CPU.ActiveCfg = Release|Any CPU

 		{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Release|Any CPU.Build.0 = Release|Any CPU

@@ -174,12 +152,6 @@ Global
 		{E1F10180-C7B9-4147-B51F-FA1B701966DC}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU

 		{E1F10180-C7B9-4147-B51F-FA1B701966DC}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU

 		{E1F10180-C7B9-4147-B51F-FA1B701966DC}.Debug|x86.ActiveCfg = Debug|Any CPU

-		{E1F10180-C7B9-4147-B51F-FA1B701966DC}.QED|.NET.ActiveCfg = QED|Any CPU

-		{E1F10180-C7B9-4147-B51F-FA1B701966DC}.QED|Any CPU.ActiveCfg = QED|Any CPU

-		{E1F10180-C7B9-4147-B51F-FA1B701966DC}.QED|Any CPU.Build.0 = QED|Any CPU

-		{E1F10180-C7B9-4147-B51F-FA1B701966DC}.QED|Mixed Platforms.ActiveCfg = QED|Any CPU

-		{E1F10180-C7B9-4147-B51F-FA1B701966DC}.QED|Mixed Platforms.Build.0 = QED|Any CPU

-		{E1F10180-C7B9-4147-B51F-FA1B701966DC}.QED|x86.ActiveCfg = QED|Any CPU

 		{E1F10180-C7B9-4147-B51F-FA1B701966DC}.Release|.NET.ActiveCfg = Release|Any CPU

 		{E1F10180-C7B9-4147-B51F-FA1B701966DC}.Release|Any CPU.ActiveCfg = Release|Any CPU

 		{E1F10180-C7B9-4147-B51F-FA1B701966DC}.Release|Any CPU.Build.0 = Release|Any CPU

@@ -205,12 +177,6 @@ Global
 		{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU

 		{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU

 		{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}.Debug|x86.ActiveCfg = Debug|Any CPU

-		{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}.QED|.NET.ActiveCfg = QED|Any CPU

-		{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}.QED|Any CPU.ActiveCfg = QED|Any CPU

-		{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}.QED|Any CPU.Build.0 = QED|Any CPU

-		{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}.QED|Mixed Platforms.ActiveCfg = QED|Any CPU

-		{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}.QED|Mixed Platforms.Build.0 = QED|Any CPU

-		{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}.QED|x86.ActiveCfg = QED|Any CPU

 		{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}.Release|.NET.ActiveCfg = Release|Any CPU

 		{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}.Release|Any CPU.ActiveCfg = Release|Any CPU

 		{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}.Release|Any CPU.Build.0 = Release|Any CPU

@@ -236,12 +202,6 @@ Global
 		{B230A69C-C466-4065-B9C1-84D80E76D802}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU

 		{B230A69C-C466-4065-B9C1-84D80E76D802}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU

 		{B230A69C-C466-4065-B9C1-84D80E76D802}.Debug|x86.ActiveCfg = Debug|Any CPU

-		{B230A69C-C466-4065-B9C1-84D80E76D802}.QED|.NET.ActiveCfg = QED|Any CPU

-		{B230A69C-C466-4065-B9C1-84D80E76D802}.QED|Any CPU.ActiveCfg = QED|Any CPU

-		{B230A69C-C466-4065-B9C1-84D80E76D802}.QED|Any CPU.Build.0 = QED|Any CPU

-		{B230A69C-C466-4065-B9C1-84D80E76D802}.QED|Mixed Platforms.ActiveCfg = QED|Any CPU

-		{B230A69C-C466-4065-B9C1-84D80E76D802}.QED|Mixed Platforms.Build.0 = QED|Any CPU

-		{B230A69C-C466-4065-B9C1-84D80E76D802}.QED|x86.ActiveCfg = QED|Any CPU

 		{B230A69C-C466-4065-B9C1-84D80E76D802}.Release|.NET.ActiveCfg = Release|Any CPU

 		{B230A69C-C466-4065-B9C1-84D80E76D802}.Release|Any CPU.ActiveCfg = Release|Any CPU

 		{B230A69C-C466-4065-B9C1-84D80E76D802}.Release|Any CPU.Build.0 = Release|Any CPU

@@ -267,12 +227,6 @@ Global
 		{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU

 		{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU

 		{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.Debug|x86.ActiveCfg = Debug|Any CPU

-		{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.QED|.NET.ActiveCfg = QED|Any CPU

-		{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.QED|Any CPU.ActiveCfg = QED|Any CPU

-		{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.QED|Any CPU.Build.0 = QED|Any CPU

-		{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.QED|Mixed Platforms.ActiveCfg = QED|Any CPU

-		{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.QED|Mixed Platforms.Build.0 = QED|Any CPU

-		{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.QED|x86.ActiveCfg = QED|Any CPU

 		{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.Release|.NET.ActiveCfg = Release|Any CPU

 		{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.Release|Any CPU.ActiveCfg = Release|Any CPU

 		{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.Release|Any CPU.Build.0 = Release|Any CPU

@@ -298,12 +252,6 @@ Global
 		{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU

 		{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU

 		{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Debug|x86.ActiveCfg = Debug|Any CPU

-		{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.QED|.NET.ActiveCfg = QED|Any CPU

-		{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.QED|Any CPU.ActiveCfg = QED|Any CPU

-		{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.QED|Any CPU.Build.0 = QED|Any CPU

-		{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.QED|Mixed Platforms.ActiveCfg = QED|Any CPU

-		{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.QED|Mixed Platforms.Build.0 = QED|Any CPU

-		{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.QED|x86.ActiveCfg = QED|Any CPU

 		{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Release|.NET.ActiveCfg = Release|Any CPU

 		{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Release|Any CPU.ActiveCfg = Release|Any CPU

 		{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Release|Any CPU.Build.0 = Release|Any CPU

@@ -329,12 +277,6 @@ Global
 		{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU

 		{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU

 		{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}.Debug|x86.ActiveCfg = Debug|Any CPU

-		{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}.QED|.NET.ActiveCfg = QED|Any CPU

-		{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}.QED|Any CPU.ActiveCfg = QED|Any CPU

-		{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}.QED|Any CPU.Build.0 = QED|Any CPU

-		{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}.QED|Mixed Platforms.ActiveCfg = QED|Any CPU

-		{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}.QED|Mixed Platforms.Build.0 = QED|Any CPU

-		{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}.QED|x86.ActiveCfg = QED|Any CPU

 		{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}.Release|.NET.ActiveCfg = Release|Any CPU

 		{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}.Release|Any CPU.ActiveCfg = Release|Any CPU

 		{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}.Release|Any CPU.Build.0 = Release|Any CPU

@@ -360,12 +302,6 @@ Global
 		{A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Debug|Mixed Platforms.Build.0 = Debug|x86

 		{A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Debug|x86.ActiveCfg = Debug|x86

 		{A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Debug|x86.Build.0 = Debug|x86

-		{A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.QED|.NET.ActiveCfg = QED|x86

-		{A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.QED|Any CPU.ActiveCfg = QED|x86

-		{A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.QED|Mixed Platforms.ActiveCfg = QED|x86

-		{A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.QED|Mixed Platforms.Build.0 = QED|x86

-		{A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.QED|x86.ActiveCfg = QED|x86

-		{A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.QED|x86.Build.0 = QED|x86

 		{A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Release|.NET.ActiveCfg = Release|x86

 		{A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Release|Any CPU.ActiveCfg = Release|x86

 		{A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Release|Mixed Platforms.ActiveCfg = Release|x86

@@ -390,12 +326,6 @@ Global
 		{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU

 		{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU

 		{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.Debug|x86.ActiveCfg = Debug|Any CPU

-		{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.QED|.NET.ActiveCfg = QED|Any CPU

-		{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.QED|Any CPU.ActiveCfg = QED|Any CPU

-		{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.QED|Any CPU.Build.0 = QED|Any CPU

-		{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.QED|Mixed Platforms.ActiveCfg = QED|Any CPU

-		{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.QED|Mixed Platforms.Build.0 = QED|Any CPU

-		{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.QED|x86.ActiveCfg = QED|Any CPU

 		{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.Release|.NET.ActiveCfg = Release|Any CPU

 		{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.Release|Any CPU.ActiveCfg = Release|Any CPU

 		{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.Release|Any CPU.Build.0 = Release|Any CPU

@@ -421,12 +351,6 @@ Global
 		{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU

 		{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU

 		{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Debug|x86.ActiveCfg = Debug|Any CPU

-		{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.QED|.NET.ActiveCfg = QED|Any CPU

-		{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.QED|Any CPU.ActiveCfg = QED|Any CPU

-		{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.QED|Any CPU.Build.0 = QED|Any CPU

-		{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.QED|Mixed Platforms.ActiveCfg = QED|Any CPU

-		{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.QED|Mixed Platforms.Build.0 = QED|Any CPU

-		{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.QED|x86.ActiveCfg = QED|Any CPU

 		{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Release|.NET.ActiveCfg = Release|Any CPU

 		{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Release|Any CPU.ActiveCfg = Release|Any CPU

 		{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Release|Any CPU.Build.0 = Release|Any CPU

@@ -452,12 +376,6 @@ Global
 		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU

 		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU

 		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Debug|x86.ActiveCfg = Debug|Any CPU

-		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.QED|.NET.ActiveCfg = QED|Any CPU

-		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.QED|Any CPU.ActiveCfg = QED|Any CPU

-		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.QED|Any CPU.Build.0 = QED|Any CPU

-		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.QED|Mixed Platforms.ActiveCfg = QED|Any CPU

-		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.QED|Mixed Platforms.Build.0 = QED|Any CPU

-		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.QED|x86.ActiveCfg = QED|Any CPU

 		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Release|.NET.ActiveCfg = Release|Any CPU

 		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Release|Any CPU.ActiveCfg = Release|Any CPU

 		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Release|Any CPU.Build.0 = Release|Any CPU

@@ -483,12 +401,6 @@ Global
 		{AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU

 		{AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU

 		{AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Debug|x86.ActiveCfg = Debug|Any CPU

-		{AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.QED|.NET.ActiveCfg = QED|Any CPU

-		{AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.QED|Any CPU.ActiveCfg = QED|Any CPU

-		{AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.QED|Any CPU.Build.0 = QED|Any CPU

-		{AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.QED|Mixed Platforms.ActiveCfg = QED|Any CPU

-		{AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.QED|Mixed Platforms.Build.0 = QED|Any CPU

-		{AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.QED|x86.ActiveCfg = QED|Any CPU

 		{AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Release|.NET.ActiveCfg = Release|Any CPU

 		{AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Release|Any CPU.ActiveCfg = Release|Any CPU

 		{AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Release|Any CPU.Build.0 = Release|Any CPU

@@ -513,12 +425,6 @@ Global
 		{884386A3-58E9-40BB-A273-B24976775553}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU

 		{884386A3-58E9-40BB-A273-B24976775553}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU

 		{884386A3-58E9-40BB-A273-B24976775553}.Debug|x86.ActiveCfg = Debug|Any CPU

-		{884386A3-58E9-40BB-A273-B24976775553}.QED|.NET.ActiveCfg = QED|Any CPU

-		{884386A3-58E9-40BB-A273-B24976775553}.QED|Any CPU.ActiveCfg = QED|Any CPU

-		{884386A3-58E9-40BB-A273-B24976775553}.QED|Any CPU.Build.0 = QED|Any CPU

-		{884386A3-58E9-40BB-A273-B24976775553}.QED|Mixed Platforms.ActiveCfg = QED|Any CPU

-		{884386A3-58E9-40BB-A273-B24976775553}.QED|Mixed Platforms.Build.0 = QED|Any CPU

-		{884386A3-58E9-40BB-A273-B24976775553}.QED|x86.ActiveCfg = QED|Any CPU

 		{884386A3-58E9-40BB-A273-B24976775553}.Release|.NET.ActiveCfg = Release|Any CPU

 		{884386A3-58E9-40BB-A273-B24976775553}.Release|Any CPU.ActiveCfg = Release|Any CPU

 		{884386A3-58E9-40BB-A273-B24976775553}.Release|Any CPU.Build.0 = Release|Any CPU

@@ -543,12 +449,6 @@ Global
 		{EAA5EB79-D475-4601-A59B-825C191CD25F}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU

 		{EAA5EB79-D475-4601-A59B-825C191CD25F}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU

 		{EAA5EB79-D475-4601-A59B-825C191CD25F}.Debug|x86.ActiveCfg = Debug|Any CPU

-		{EAA5EB79-D475-4601-A59B-825C191CD25F}.QED|.NET.ActiveCfg = QED|Any CPU

-		{EAA5EB79-D475-4601-A59B-825C191CD25F}.QED|Any CPU.ActiveCfg = QED|Any CPU

-		{EAA5EB79-D475-4601-A59B-825C191CD25F}.QED|Any CPU.Build.0 = QED|Any CPU

-		{EAA5EB79-D475-4601-A59B-825C191CD25F}.QED|Mixed Platforms.ActiveCfg = QED|Any CPU

-		{EAA5EB79-D475-4601-A59B-825C191CD25F}.QED|Mixed Platforms.Build.0 = QED|Any CPU

-		{EAA5EB79-D475-4601-A59B-825C191CD25F}.QED|x86.ActiveCfg = QED|Any CPU

 		{EAA5EB79-D475-4601-A59B-825C191CD25F}.Release|.NET.ActiveCfg = Release|Any CPU

 		{EAA5EB79-D475-4601-A59B-825C191CD25F}.Release|Any CPU.ActiveCfg = Release|Any CPU

 		{EAA5EB79-D475-4601-A59B-825C191CD25F}.Release|Any CPU.Build.0 = Release|Any CPU

@@ -573,12 +473,6 @@ Global
 		{8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU

 		{8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU

 		{8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Debug|x86.ActiveCfg = Debug|Any CPU

-		{8A05D14E-F2BF-4890-BBE0-D76B18A50797}.QED|.NET.ActiveCfg = QED|Any CPU

-		{8A05D14E-F2BF-4890-BBE0-D76B18A50797}.QED|Any CPU.ActiveCfg = QED|Any CPU

-		{8A05D14E-F2BF-4890-BBE0-D76B18A50797}.QED|Any CPU.Build.0 = QED|Any CPU

-		{8A05D14E-F2BF-4890-BBE0-D76B18A50797}.QED|Mixed Platforms.ActiveCfg = QED|Any CPU

-		{8A05D14E-F2BF-4890-BBE0-D76B18A50797}.QED|Mixed Platforms.Build.0 = QED|Any CPU

-		{8A05D14E-F2BF-4890-BBE0-D76B18A50797}.QED|x86.ActiveCfg = QED|Any CPU

 		{8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Release|.NET.ActiveCfg = Release|Any CPU

 		{8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Release|Any CPU.ActiveCfg = Release|Any CPU

 		{8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Release|Any CPU.Build.0 = Release|Any CPU

@@ -603,12 +497,6 @@ Global
 		{D07B8E38-E172-47F4-AD02-0373014A46D3}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU

 		{D07B8E38-E172-47F4-AD02-0373014A46D3}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU

 		{D07B8E38-E172-47F4-AD02-0373014A46D3}.Debug|x86.ActiveCfg = Debug|Any CPU

-		{D07B8E38-E172-47F4-AD02-0373014A46D3}.QED|.NET.ActiveCfg = QED|Any CPU

-		{D07B8E38-E172-47F4-AD02-0373014A46D3}.QED|Any CPU.ActiveCfg = QED|Any CPU

-		{D07B8E38-E172-47F4-AD02-0373014A46D3}.QED|Any CPU.Build.0 = QED|Any CPU

-		{D07B8E38-E172-47F4-AD02-0373014A46D3}.QED|Mixed Platforms.ActiveCfg = QED|Any CPU

-		{D07B8E38-E172-47F4-AD02-0373014A46D3}.QED|Mixed Platforms.Build.0 = QED|Any CPU

-		{D07B8E38-E172-47F4-AD02-0373014A46D3}.QED|x86.ActiveCfg = QED|Any CPU

 		{D07B8E38-E172-47F4-AD02-0373014A46D3}.Release|.NET.ActiveCfg = Release|Any CPU

 		{D07B8E38-E172-47F4-AD02-0373014A46D3}.Release|Any CPU.ActiveCfg = Release|Any CPU

 		{D07B8E38-E172-47F4-AD02-0373014A46D3}.Release|Any CPU.Build.0 = Release|Any CPU

diff --git a/Source/Concurrency/LinearSets.cs b/Source/Concurrency/LinearSets.cs
index 08354ae6..fc44468c 100644
--- a/Source/Concurrency/LinearSets.cs
+++ b/Source/Concurrency/LinearSets.cs
@@ -466,9 +466,14 @@ namespace Microsoft.Boogie
                     Error(node, "Only local linear variable can be an actual input parameter of a procedure call");

                     continue;

                 }

-                if (FindLinearKind(formal) == LinearKind.LINEAR && FindLinearKind(actual.Decl) == LinearKind.CONST)

+                if (FindLinearKind(actual.Decl) == LinearKind.CONST && FindLinearKind(formal) == LinearKind.LINEAR)

                 {

-                    Error(node, "Only non-const linear variable can be an actual parameter to a non-const input parameter of a procedure call");

+                    Error(node, "Const linear variable cannot be an argument for a linear input parameter of a procedure call");

+                    continue;

+                }

+                if (FindLinearKind(actual.Decl) == LinearKind.CONST && FindLinearKind(formal) == LinearKind.CONST && node.IsAsync)

+                {

+                    Error(node, "Const linear variable cannot be an argument for a const parameter of an async procedure call");

                     continue;

                 }

                 if (inVars.Contains(actual.Decl))

diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs
index 669a502e..5fd67978 100644
--- a/Source/Concurrency/TypeCheck.cs
+++ b/Source/Concurrency/TypeCheck.cs
@@ -333,9 +333,7 @@ namespace Microsoft.Boogie
             if (errorCount > 0) return;

             this.VisitProgram(program);

             if (errorCount > 0) return;

-#if QED

             YieldTypeChecker.PerformYieldSafeCheck(this);

-#endif

         }

 

         public MoverTypeChecker(Program program)

diff --git a/Source/Concurrency/YieldTypeChecker.cs b/Source/Concurrency/YieldTypeChecker.cs
index c6979fc7..d278ad69 100644
--- a/Source/Concurrency/YieldTypeChecker.cs
+++ b/Source/Concurrency/YieldTypeChecker.cs
@@ -1,12 +1,9 @@
-#if QED

-

-using System;

+using System;

 using System.Collections;

 using System.Collections.Generic;

 using System.Linq;

 using System.Text;

 using Microsoft.Boogie;

-using Microsoft.Automata;

 using System.Diagnostics.Contracts;

 using Microsoft.Boogie.AbstractInterpretation;

 using Microsoft.Boogie.GraphUtil;

@@ -16,42 +13,9 @@ namespace Microsoft.Boogie
 {

     class YieldTypeChecker

     {

-        static CharSetSolver yieldTypeCheckerAutomatonSolver;

-        static Automaton<BvSet> yieldTypeCheckerAutomaton;

         static List<Tuple<int, int, int>> yieldTypeCheckerAutomatonEdges;

         static YieldTypeChecker()

         {

-            yieldTypeCheckerAutomatonSolver = new CharSetSolver(BitWidth.BV7);

-            yieldTypeCheckerAutomaton = yieldTypeCheckerAutomatonSolver.ReadFromRanges(3, new int[] { 0 },

-                new int[][] {

-                    new int[] {3, 'P', 'P', 3 },

-                    new int[] {3, 'Y', 'Y', 0 },

-                    new int[] {3, 'Y', 'Y', 1 },

-                    new int[] {3, 'Y', 'Y', 2 },

-                    new int[] {0, 'P', 'P', 0 },

-                    new int[] {0, 'Y', 'Y', 0 },

-                    new int[] {0, 'Y', 'Y', 1 },

-                    new int[] {0, 'Y', 'Y', 2 },

-                    new int[] {1, 'P', 'P', 1 },

-                    new int[] {1, 'R', 'R', 1 },

-                    new int[] {1, 'B', 'B', 1 },

-                    new int[] {1, 'Y', 'Y', 1 },

-                    new int[] {1, 'Y', 'Y', 0 },

-                    new int[] {1, 'A', 'A', 2 },

-                    new int[] {1, 'P', 'P', 2 },

-                    new int[] {1, 'R', 'R', 2 },

-                    new int[] {1, 'B', 'B', 2 },

-                    new int[] {1, 'Y', 'Y', 2 },

-                    new int[] {2, 'L', 'L', 2 },

-                    new int[] {2, 'B', 'B', 2 },

-                    new int[] {2, 'P', 'P', 2 },

-                    new int[] {2, 'Y', 'Y', 2 },

-                    new int[] {2, 'Y', 'Y', 1 },

-                    new int[] {2, 'Y', 'Y', 0 },

-                });

-            // uncomment the following line to visualize the spec automaton

-            // yieldTypeCheckerAutomatonSolver.ShowGraph(yieldTypeCheckerAutomaton, "yieldTypeCheckerAutomaton.dgml");

-

             yieldTypeCheckerAutomatonEdges = new List<Tuple<int, int, int>>();

             AddEdge(0, 'P', 0);

             AddEdge(0, 'Y', 0);

@@ -125,22 +89,6 @@ namespace Microsoft.Boogie
                     initialConstraints[absyToNode[block]] = new HashSet<int>(new int[] { 0, 1 });

                 }

             }

-

-            Automaton<BvSet> implAutomaton = yieldTypeCheckerAutomatonSolver.ReadFromRanges(dummyInitial, finalStates.ToArray(), transitions);

-            // yieldTypeCheckerAutomatonSolver.SaveAsDgml(implAutomaton, string.Format("{0}.dgml", impl.Name));

-            List<BvSet> witnessSet;

-            var isNonEmpty = Automaton<BvSet>.CheckDifference(

-                                                           implAutomaton,

-                                                           yieldTypeCheckerAutomaton,

-                                                           0,

-                                                           yieldTypeCheckerAutomatonSolver,

-                                                           out witnessSet);

-            var diffAutomaton = implAutomaton.Minus(yieldTypeCheckerAutomaton, yieldTypeCheckerAutomatonSolver);

-            if (isNonEmpty)

-            {

-                moverTypeChecker.Error(impl, PrintErrorTrace(diffAutomaton));

-            }

-

             SimulationRelation<int, int, int> x = new SimulationRelation<int, int, int>(implEdges, yieldTypeCheckerAutomatonEdges, initialConstraints);

             Dictionary<int, HashSet<int>> simulationRelation = x.ComputeSimulationRelation();

             foreach (Block block in loopHeaders)

@@ -149,7 +97,6 @@ namespace Microsoft.Boogie
                 {

                     IToken tok = block.tok;

                     moverTypeChecker.Error(impl, string.Format("Loop at {0}({1}, {2}) not simulated appropriately at phase {3}\n", tok.filename, tok.line, tok.col, currPhaseNum));

-                    yieldTypeCheckerAutomatonSolver.SaveAsDgml(implAutomaton, string.Format("{0}_{1}.dgml", impl.Name, currPhaseNum));

                 }

             }

         }

@@ -167,20 +114,6 @@ namespace Microsoft.Boogie
             return false;

         }

         

-        private string PrintErrorTrace(Automaton<BvSet> errorAutomaton)

-        {

-            String s = "\nBody of " + impl.Proc.Name + " is not yield_type_safe at phase " + currPhaseNum.ToString() + "\n";

-            foreach (var move in errorAutomaton.GetMoves())

-            {

-                if (nodeToAbsy.ContainsKey(move.SourceState))

-                {

-                    IToken tok = nodeToAbsy[move.SourceState].tok;

-                    s += string.Format("{0}({1}, {2})\n", tok.filename, tok.line, tok.col);

-                }

-            }

-            return s;

-        }

-

         public static void PerformYieldSafeCheck(MoverTypeChecker moverTypeChecker)

         {

             foreach (var decl in moverTypeChecker.program.TopLevelDeclarations)

@@ -390,5 +323,3 @@ namespace Microsoft.Boogie
         }

     }

 }

-

-#endif
\ No newline at end of file
diff --git a/Test/linear/async-bug.bpl b/Test/linear/async-bug.bpl
new file mode 100644
index 00000000..faa1a65d
--- /dev/null
+++ b/Test/linear/async-bug.bpl
@@ -0,0 +1,31 @@
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory -doModSetAnalysis "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+const GcTid:int;

+

+procedure {:yields} {:phase 100} Initialize({:cnst "tid"} tid:int)

+requires{:phase 100} tid == GcTid;

+{

+    yield;

+    assert{:phase 100} tid == GcTid;

+

+    async call GarbageCollect(tid);

+

+    yield;

+    assert{:phase 100} tid == GcTid;

+

+    async call GarbageCollect(tid);

+

+    yield;

+    assert{:phase 100} tid == GcTid;

+

+    yield;

+    assert{:phase 100} tid == GcTid;

+}

+

+procedure {:yields} {:phase 100} GarbageCollect({:cnst "tid"} tid:int)

+requires{:phase 100} tid == GcTid;

+{

+    yield;

+    assert{:phase 100} tid == GcTid;

+}

+

diff --git a/Test/linear/async-bug.bpl.expect b/Test/linear/async-bug.bpl.expect
new file mode 100644
index 00000000..8bfe61d1
--- /dev/null
+++ b/Test/linear/async-bug.bpl.expect
@@ -0,0 +1,3 @@
+async-bug.bpl(11,10): Error: Const linear variable cannot be an argument for a const parameter of an async procedure call

+async-bug.bpl(16,10): Error: Const linear variable cannot be an argument for a const parameter of an async procedure call

+2 type checking errors detected in async-bug.bpl

diff --git a/Test/og/lock-introduced.bpl b/Test/og/lock-introduced.bpl
index 33d84fa2..0b4e39f3 100644
--- a/Test/og/lock-introduced.bpl
+++ b/Test/og/lock-introduced.bpl
@@ -1,6 +1,5 @@
 // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

 // RUN: %diff "%s.expect" "%t"

-// XFAIL: *

 function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;

 function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool

 {

diff --git a/Test/og/lock-introduced.bpl.expect b/Test/og/lock-introduced.bpl.expect
new file mode 100644
index 00000000..f62a8f46
--- /dev/null
+++ b/Test/og/lock-introduced.bpl.expect
@@ -0,0 +1,2 @@
+

+Boogie program verifier finished with 12 verified, 0 errors

diff --git a/Test/og/termination.bpl b/Test/og/termination.bpl
index 26ff030d..35064f77 100644
--- a/Test/og/termination.bpl
+++ b/Test/og/termination.bpl
@@ -1,17 +1,15 @@
 // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

 // RUN: %diff "%s.expect" "%t"

-// XFAIL: *

-procedure {:yields} X();

-ensures {:atomic 0} |{ A: return true; }|;

+procedure {:yields} {:phase 0} X();

+ensures {:atomic} |{ A: return true; }|;

 

-procedure {:yields} Y();

-ensures {:left 0} |{ A: return true; }|;

+procedure {:yields} {:phase 0} Y();

+ensures {:left} |{ A: return true; }|;

 

-procedure {:yields} main() {

+procedure {:yields} {:phase 1} main() {

   yield;

   call X();

   while (*)

-//  invariant {:terminates} true;

   {

     call Y();

   }

diff --git a/Test/og/termination.bpl.expect b/Test/og/termination.bpl.expect
new file mode 100644
index 00000000..a924f8cf
--- /dev/null
+++ b/Test/og/termination.bpl.expect
@@ -0,0 +1,3 @@
+termination.bpl(9,31): Error: Loop at termination.bpl(12, 3) not simulated appropriately at phase 1
+

+1 type checking errors detected in termination.bpl

diff --git a/Test/og/termination2.bpl b/Test/og/termination2.bpl
new file mode 100644
index 00000000..d0d88a22
--- /dev/null
+++ b/Test/og/termination2.bpl
@@ -0,0 +1,19 @@
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+procedure {:yields} {:phase 0} X();

+ensures {:atomic} |{ A: return true; }|;

+

+procedure {:yields} {:phase 0} Y();

+ensures {:left} |{ A: return true; }|;

+

+procedure {:yields} {:phase 1} main() {

+  yield;

+  call X();

+  while (*)

+  invariant {:terminates} {:phase 1} true;

+  {

+    call Y();

+  }

+  yield;

+  assert {:phase 1} true;

+}

diff --git a/Test/og/termination2.bpl.expect b/Test/og/termination2.bpl.expect
new file mode 100644
index 00000000..6abb715b
--- /dev/null
+++ b/Test/og/termination2.bpl.expect
@@ -0,0 +1,2 @@
+

+Boogie program verifier finished with 1 verified, 0 errors