Merge

6 files changed, 519 insertions, 38 deletions

diff --git a/Source/Boogie.sln b/Source/Boogie.sln
index adaf7cf3..53130382 100644
--- a/Source/Boogie.sln
+++ b/Source/Boogie.sln
@@ -41,8 +41,6 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "TPTP", "Provers\TPTP\TPTP.c
 EndProject

 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Houdini", "Houdini\Houdini.csproj", "{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}"

 EndProject

-Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "GPUVerify", "GPUVerify\GPUVerify.csproj", "{E5D16606-06D0-434F-A9D7-7D079BC80229}"

-EndProject

 Global

 	GlobalSection(SolutionConfigurationPlatforms) = preSolution

 		Checked|.NET = Checked|.NET

@@ -523,30 +521,6 @@ Global
 		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.z3apidebug|Mixed Platforms.ActiveCfg = Debug|Any CPU

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

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

-		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|.NET.ActiveCfg = Release|x86

-		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|Any CPU.ActiveCfg = Release|x86

-		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|Mixed Platforms.ActiveCfg = Checked|x86

-		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|Mixed Platforms.Build.0 = Checked|x86

-		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|x86.ActiveCfg = Release|x86

-		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|x86.Build.0 = Release|x86

-		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Debug|.NET.ActiveCfg = Debug|x86

-		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Debug|Any CPU.ActiveCfg = Debug|x86

-		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Debug|Mixed Platforms.ActiveCfg = Debug|x86

-		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Debug|Mixed Platforms.Build.0 = Debug|x86

-		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Debug|x86.ActiveCfg = Debug|x86

-		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Debug|x86.Build.0 = Debug|x86

-		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Release|.NET.ActiveCfg = Release|x86

-		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Release|Any CPU.ActiveCfg = Release|x86

-		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Release|Mixed Platforms.ActiveCfg = Release|x86

-		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Release|Mixed Platforms.Build.0 = Release|x86

-		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Release|x86.ActiveCfg = Release|x86

-		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Release|x86.Build.0 = Release|x86

-		{E5D16606-06D0-434F-A9D7-7D079BC80229}.z3apidebug|.NET.ActiveCfg = Release|x86

-		{E5D16606-06D0-434F-A9D7-7D079BC80229}.z3apidebug|Any CPU.ActiveCfg = Release|x86

-		{E5D16606-06D0-434F-A9D7-7D079BC80229}.z3apidebug|Mixed Platforms.ActiveCfg = Release|x86

-		{E5D16606-06D0-434F-A9D7-7D079BC80229}.z3apidebug|Mixed Platforms.Build.0 = Release|x86

-		{E5D16606-06D0-434F-A9D7-7D079BC80229}.z3apidebug|x86.ActiveCfg = Release|x86

-		{E5D16606-06D0-434F-A9D7-7D079BC80229}.z3apidebug|x86.Build.0 = Release|x86

 	EndGlobalSection

 	GlobalSection(SolutionProperties) = preSolution

 		HideSolutionNode = FALSE

diff --git a/Source/GPUVerify.sln b/Source/GPUVerify.sln
new file mode 100644
index 00000000..4fb930ef
--- /dev/null
+++ b/Source/GPUVerify.sln
@@ -0,0 +1,420 @@
+

+Microsoft Visual Studio Solution File, Format Version 11.00

+# Visual Studio 2010

+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "GPUVerify", "GPUVerify\GPUVerify.csproj", "{E5D16606-06D0-434F-A9D7-7D079BC80229}"

+EndProject

+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "AIFramework", "AIFramework\AIFramework.csproj", "{39B0658D-C955-41C5-9A43-48C97A1EF5FD}"

+EndProject

+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Basetypes", "Basetypes\Basetypes.csproj", "{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}"

+EndProject

+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Core", "Core\Core.csproj", "{B230A69C-C466-4065-B9C1-84D80E76D802}"

+EndProject

+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "CodeContractsExtender", "CodeContractsExtender\CodeContractsExtender.csproj", "{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}"

+EndProject

+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Graph", "Graph\Graph.csproj", "{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}"

+EndProject

+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ParserHelper", "ParserHelper\ParserHelper.csproj", "{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}"

+EndProject

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

+EndProject

+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "AbsInt", "AbsInt\AbsInt.csproj", "{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}"

+EndProject

+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Houdini", "Houdini\Houdini.csproj", "{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}"

+EndProject

+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Isabelle", "Provers\Isabelle\Isabelle.csproj", "{435D5BD0-6F62-49F8-BB24-33E2257519AD}"

+EndProject

+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Z3", "Provers\Z3\Z3.csproj", "{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}"

+EndProject

+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "SMTLib", "Provers\SMTLib\SMTLib.csproj", "{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}"

+EndProject

+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "TPTP", "Provers\TPTP\TPTP.csproj", "{A598ED5A-93AD-4125-A555-3921A2F936FA}"

+EndProject

+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Simplify", "Provers\Simplify\Simplify.csproj", "{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}"

+EndProject

+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "VCGeneration", "VCGeneration\VCGeneration.csproj", "{E1F10180-C7B9-4147-B51F-FA1B701966DC}"

+EndProject

+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Model", "Model\Model.csproj", "{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}"

+EndProject

+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "VCExpr", "VCExpr\VCExpr.csproj", "{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}"

+EndProject

+Global

+	GlobalSection(SolutionConfigurationPlatforms) = preSolution

+		Checked|Any CPU = Checked|Any CPU

+		Checked|Mixed Platforms = Checked|Mixed Platforms

+		Checked|x86 = Checked|x86

+		Debug|Any CPU = Debug|Any CPU

+		Debug|Mixed Platforms = Debug|Mixed Platforms

+		Debug|x86 = Debug|x86

+		Release|Any CPU = Release|Any CPU

+		Release|Mixed Platforms = Release|Mixed Platforms

+		Release|x86 = Release|x86

+		z3apidebug|Any CPU = z3apidebug|Any CPU

+		z3apidebug|Mixed Platforms = z3apidebug|Mixed Platforms

+		z3apidebug|x86 = z3apidebug|x86

+	EndGlobalSection

+	GlobalSection(ProjectConfigurationPlatforms) = postSolution

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|Any CPU.ActiveCfg = Checked|Any CPU

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|Mixed Platforms.Build.0 = Checked|Any CPU

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|x86.ActiveCfg = Checked|Any CPU

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|x86.Build.0 = Checked|Any CPU

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Debug|Any CPU.ActiveCfg = Debug|Any CPU

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Debug|x86.ActiveCfg = Debug|Any CPU

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Debug|x86.Build.0 = Debug|Any CPU

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Release|Any CPU.ActiveCfg = Release|Any CPU

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Release|Mixed Platforms.Build.0 = Release|Any CPU

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Release|x86.ActiveCfg = Release|Any CPU

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Release|x86.Build.0 = Release|Any CPU

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.z3apidebug|Any CPU.ActiveCfg = Release|Any CPU

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.z3apidebug|x86.ActiveCfg = Release|Any CPU

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.z3apidebug|x86.Build.0 = Release|Any CPU

+		{39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Checked|Any CPU.ActiveCfg = Checked|Any CPU

+		{39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Checked|Any CPU.Build.0 = Checked|Any CPU

+		{39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU

+		{39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Checked|Mixed Platforms.Build.0 = Checked|Any CPU

+		{39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Checked|x86.ActiveCfg = Checked|Any CPU

+		{39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Debug|Any CPU.ActiveCfg = Debug|Any CPU

+		{39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Debug|Any CPU.Build.0 = Debug|Any CPU

+		{39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU

+		{39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU

+		{39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Debug|x86.ActiveCfg = Debug|Any CPU

+		{39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Release|Any CPU.ActiveCfg = Release|Any CPU

+		{39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Release|Any CPU.Build.0 = Release|Any CPU

+		{39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU

+		{39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Release|Mixed Platforms.Build.0 = Release|Any CPU

+		{39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Release|x86.ActiveCfg = Release|Any CPU

+		{39B0658D-C955-41C5-9A43-48C97A1EF5FD}.z3apidebug|Any CPU.ActiveCfg = z3apidebug|Any CPU

+		{39B0658D-C955-41C5-9A43-48C97A1EF5FD}.z3apidebug|Any CPU.Build.0 = z3apidebug|Any CPU

+		{39B0658D-C955-41C5-9A43-48C97A1EF5FD}.z3apidebug|Mixed Platforms.ActiveCfg = z3apidebug|Any CPU

+		{39B0658D-C955-41C5-9A43-48C97A1EF5FD}.z3apidebug|Mixed Platforms.Build.0 = z3apidebug|Any CPU

+		{39B0658D-C955-41C5-9A43-48C97A1EF5FD}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU

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

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

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

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

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

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

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

+		{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}.Release|Any CPU.ActiveCfg = Release|Any CPU

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

+		{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}.Release|Any CPU.ActiveCfg = Release|Any CPU

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

+		{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}.Release|Any CPU.ActiveCfg = Release|Any CPU

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

+		{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}.Release|Any CPU.ActiveCfg = Release|Any CPU

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

+		{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}.Release|Any CPU.ActiveCfg = Release|Any CPU

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

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

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

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

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

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

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

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

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

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

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

+		{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU

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

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

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

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

+		{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}.Release|Any CPU.ActiveCfg = Release|Any CPU

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

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

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

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

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

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

+		{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.z3apidebug|Mixed Platforms.ActiveCfg = z3apidebug|Any CPU

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

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

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

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

+		{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU

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

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

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

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

+		{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}.Release|Any CPU.ActiveCfg = Release|Any CPU

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

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

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

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

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

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

+		{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}.z3apidebug|Mixed Platforms.ActiveCfg = z3apidebug|Any CPU

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

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

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

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

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

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

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

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

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

+		{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}.Release|Any CPU.ActiveCfg = Release|Any CPU

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

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

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

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

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

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

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

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

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

+		{435D5BD0-6F62-49F8-BB24-33E2257519AD}.Checked|Any CPU.ActiveCfg = Checked|Any CPU

+		{435D5BD0-6F62-49F8-BB24-33E2257519AD}.Checked|Any CPU.Build.0 = Checked|Any CPU

+		{435D5BD0-6F62-49F8-BB24-33E2257519AD}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU

+		{435D5BD0-6F62-49F8-BB24-33E2257519AD}.Checked|Mixed Platforms.Build.0 = Checked|Any CPU

+		{435D5BD0-6F62-49F8-BB24-33E2257519AD}.Checked|x86.ActiveCfg = Checked|Any CPU

+		{435D5BD0-6F62-49F8-BB24-33E2257519AD}.Debug|Any CPU.ActiveCfg = Debug|Any CPU

+		{435D5BD0-6F62-49F8-BB24-33E2257519AD}.Debug|Any CPU.Build.0 = Debug|Any CPU

+		{435D5BD0-6F62-49F8-BB24-33E2257519AD}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU

+		{435D5BD0-6F62-49F8-BB24-33E2257519AD}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU

+		{435D5BD0-6F62-49F8-BB24-33E2257519AD}.Debug|x86.ActiveCfg = Debug|Any CPU

+		{435D5BD0-6F62-49F8-BB24-33E2257519AD}.Release|Any CPU.ActiveCfg = Release|Any CPU

+		{435D5BD0-6F62-49F8-BB24-33E2257519AD}.Release|Any CPU.Build.0 = Release|Any CPU

+		{435D5BD0-6F62-49F8-BB24-33E2257519AD}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU

+		{435D5BD0-6F62-49F8-BB24-33E2257519AD}.Release|Mixed Platforms.Build.0 = Release|Any CPU

+		{435D5BD0-6F62-49F8-BB24-33E2257519AD}.Release|x86.ActiveCfg = Release|Any CPU

+		{435D5BD0-6F62-49F8-BB24-33E2257519AD}.z3apidebug|Any CPU.ActiveCfg = z3apidebug|Any CPU

+		{435D5BD0-6F62-49F8-BB24-33E2257519AD}.z3apidebug|Any CPU.Build.0 = z3apidebug|Any CPU

+		{435D5BD0-6F62-49F8-BB24-33E2257519AD}.z3apidebug|Mixed Platforms.ActiveCfg = z3apidebug|Any CPU

+		{435D5BD0-6F62-49F8-BB24-33E2257519AD}.z3apidebug|Mixed Platforms.Build.0 = z3apidebug|Any CPU

+		{435D5BD0-6F62-49F8-BB24-33E2257519AD}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU

+		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.Checked|Any CPU.ActiveCfg = Checked|Any CPU

+		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.Checked|Any CPU.Build.0 = Checked|Any CPU

+		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU

+		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.Checked|Mixed Platforms.Build.0 = Checked|Any CPU

+		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.Checked|x86.ActiveCfg = Checked|Any CPU

+		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.Debug|Any CPU.ActiveCfg = Debug|Any CPU

+		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.Debug|Any CPU.Build.0 = Debug|Any CPU

+		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU

+		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU

+		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.Debug|x86.ActiveCfg = Debug|Any CPU

+		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.Release|Any CPU.ActiveCfg = Release|Any CPU

+		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.Release|Any CPU.Build.0 = Release|Any CPU

+		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU

+		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.Release|Mixed Platforms.Build.0 = Release|Any CPU

+		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.Release|x86.ActiveCfg = Release|Any CPU

+		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.z3apidebug|Any CPU.ActiveCfg = z3apidebug|Any CPU

+		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.z3apidebug|Any CPU.Build.0 = z3apidebug|Any CPU

+		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.z3apidebug|Mixed Platforms.ActiveCfg = z3apidebug|Any CPU

+		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.z3apidebug|Mixed Platforms.Build.0 = z3apidebug|Any CPU

+		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU

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

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

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

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

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

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

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

+		{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}.Release|Any CPU.ActiveCfg = Release|Any CPU

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

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

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

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

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

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

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

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

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

+		{A598ED5A-93AD-4125-A555-3921A2F936FA}.Checked|Any CPU.ActiveCfg = Checked|Any CPU

+		{A598ED5A-93AD-4125-A555-3921A2F936FA}.Checked|Any CPU.Build.0 = Checked|Any CPU

+		{A598ED5A-93AD-4125-A555-3921A2F936FA}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU

+		{A598ED5A-93AD-4125-A555-3921A2F936FA}.Checked|Mixed Platforms.Build.0 = Checked|Any CPU

+		{A598ED5A-93AD-4125-A555-3921A2F936FA}.Checked|x86.ActiveCfg = Checked|Any CPU

+		{A598ED5A-93AD-4125-A555-3921A2F936FA}.Debug|Any CPU.ActiveCfg = Debug|Any CPU

+		{A598ED5A-93AD-4125-A555-3921A2F936FA}.Debug|Any CPU.Build.0 = Debug|Any CPU

+		{A598ED5A-93AD-4125-A555-3921A2F936FA}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU

+		{A598ED5A-93AD-4125-A555-3921A2F936FA}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU

+		{A598ED5A-93AD-4125-A555-3921A2F936FA}.Debug|x86.ActiveCfg = Debug|Any CPU

+		{A598ED5A-93AD-4125-A555-3921A2F936FA}.Release|Any CPU.ActiveCfg = Release|Any CPU

+		{A598ED5A-93AD-4125-A555-3921A2F936FA}.Release|Any CPU.Build.0 = Release|Any CPU

+		{A598ED5A-93AD-4125-A555-3921A2F936FA}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU

+		{A598ED5A-93AD-4125-A555-3921A2F936FA}.Release|Mixed Platforms.Build.0 = Release|Any CPU

+		{A598ED5A-93AD-4125-A555-3921A2F936FA}.Release|x86.ActiveCfg = Release|Any CPU

+		{A598ED5A-93AD-4125-A555-3921A2F936FA}.z3apidebug|Any CPU.ActiveCfg = Checked|Any CPU

+		{A598ED5A-93AD-4125-A555-3921A2F936FA}.z3apidebug|Any CPU.Build.0 = Checked|Any CPU

+		{A598ED5A-93AD-4125-A555-3921A2F936FA}.z3apidebug|Mixed Platforms.ActiveCfg = Checked|Any CPU

+		{A598ED5A-93AD-4125-A555-3921A2F936FA}.z3apidebug|Mixed Platforms.Build.0 = Checked|Any CPU

+		{A598ED5A-93AD-4125-A555-3921A2F936FA}.z3apidebug|x86.ActiveCfg = Checked|Any CPU

+		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.Checked|Any CPU.ActiveCfg = Checked|Any CPU

+		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.Checked|Any CPU.Build.0 = Checked|Any CPU

+		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU

+		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.Checked|Mixed Platforms.Build.0 = Checked|Any CPU

+		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.Checked|x86.ActiveCfg = Checked|Any CPU

+		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.Debug|Any CPU.ActiveCfg = Debug|Any CPU

+		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.Debug|Any CPU.Build.0 = Debug|Any CPU

+		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU

+		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU

+		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.Debug|x86.ActiveCfg = Debug|Any CPU

+		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.Release|Any CPU.ActiveCfg = Release|Any CPU

+		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.Release|Any CPU.Build.0 = Release|Any CPU

+		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU

+		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.Release|Mixed Platforms.Build.0 = Release|Any CPU

+		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.Release|x86.ActiveCfg = Release|Any CPU

+		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.z3apidebug|Any CPU.ActiveCfg = z3apidebug|Any CPU

+		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.z3apidebug|Any CPU.Build.0 = z3apidebug|Any CPU

+		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.z3apidebug|Mixed Platforms.ActiveCfg = z3apidebug|Any CPU

+		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.z3apidebug|Mixed Platforms.Build.0 = z3apidebug|Any CPU

+		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU

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

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

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

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

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

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

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

+		{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}.Release|Any CPU.ActiveCfg = Release|Any CPU

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

+		{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}.Release|Any CPU.ActiveCfg = Release|Any CPU

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

+		{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}.Release|Any CPU.ActiveCfg = Release|Any CPU

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

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

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

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

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

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

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

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

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

+	EndGlobalSection

+	GlobalSection(SolutionProperties) = preSolution

+		HideSolutionNode = FALSE

+	EndGlobalSection

+EndGlobal

diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index 52e227f2..1aac817c 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -855,23 +855,21 @@ namespace GPUVerify
             return true;

         }

 

-        

-

         public Microsoft.Boogie.Type GetTypeOfIdX()

         {

-            Contract.Requires(_X != null);

+            Contract.Assert(_X != null);

             return _X.TypedIdent.Type;

         }

 

         public Microsoft.Boogie.Type GetTypeOfIdY()

         {

-            Contract.Requires(_Y != null);

+            Contract.Assert(_Y != null);

             return _Y.TypedIdent.Type;

         }

 

         public Microsoft.Boogie.Type GetTypeOfIdZ()

         {

-            Contract.Requires(_Z != null);

+            Contract.Assert(_Z != null);

             return _Z.TypedIdent.Type;

         }

 

diff --git a/Source/GPUVerify/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj
index fcf68350..3b4e3bc5 100644
--- a/Source/GPUVerify/GPUVerify.csproj
+++ b/Source/GPUVerify/GPUVerify.csproj
@@ -2,7 +2,7 @@
 <Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">

   <PropertyGroup>

     <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>

-    <Platform Condition=" '$(Platform)' == '' ">x86</Platform>

+    <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>

     <ProductVersion>8.0.30703</ProductVersion>

     <SchemaVersion>2.0</SchemaVersion>

     <ProjectGuid>{E5D16606-06D0-434F-A9D7-7D079BC80229}</ProjectGuid>

@@ -15,8 +15,8 @@
     <FileAlignment>512</FileAlignment>

     <CodeContractsAssemblyMode>1</CodeContractsAssemblyMode>

   </PropertyGroup>

-  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|x86' ">

-    <PlatformTarget>x86</PlatformTarget>

+  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">

+    <PlatformTarget>AnyCPU</PlatformTarget>

     <DebugSymbols>true</DebugSymbols>

     <DebugType>full</DebugType>

     <Optimize>false</Optimize>

@@ -24,7 +24,7 @@
     <DefineConstants>DEBUG;TRACE</DefineConstants>

     <ErrorReport>prompt</ErrorReport>

     <WarningLevel>4</WarningLevel>

-    <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>

+    <CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>

     <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>

     <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>

     <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>

@@ -51,15 +51,93 @@
     <CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>

     <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>

     <CodeContractsAnalysisPrecisionLevel>0</CodeContractsAnalysisPrecisionLevel>

+    <CodeContractsInferRequires>False</CodeContractsInferRequires>

+    <CodeContractsInferEnsures>False</CodeContractsInferEnsures>

+    <CodeContractsSuggestRequires>True</CodeContractsSuggestRequires>

+    <CodeContractsSuggestEnsures>False</CodeContractsSuggestEnsures>

+    <CodeContractsDisjunctiveRequires>False</CodeContractsDisjunctiveRequires>

   </PropertyGroup>

-  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|x86' ">

-    <PlatformTarget>x86</PlatformTarget>

+  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">

+    <PlatformTarget>AnyCPU</PlatformTarget>

     <DebugType>pdbonly</DebugType>

     <Optimize>true</Optimize>

     <OutputPath>bin\Release\</OutputPath>

     <DefineConstants>TRACE</DefineConstants>

     <ErrorReport>prompt</ErrorReport>

     <WarningLevel>4</WarningLevel>

+    <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>

+    <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>

+    <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>

+    <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>

+    <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>

+    <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>

+    <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>

+    <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>

+    <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>

+    <CodeContractsEnumObligations>False</CodeContractsEnumObligations>

+    <CodeContractsPointerObligations>False</CodeContractsPointerObligations>

+    <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>

+    <CodeContractsInferRequires>False</CodeContractsInferRequires>

+    <CodeContractsInferEnsures>False</CodeContractsInferEnsures>

+    <CodeContractsSuggestRequires>True</CodeContractsSuggestRequires>

+    <CodeContractsSuggestEnsures>False</CodeContractsSuggestEnsures>

+    <CodeContractsDisjunctiveRequires>False</CodeContractsDisjunctiveRequires>

+    <CodeContractsRunInBackground>True</CodeContractsRunInBackground>

+    <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>

+    <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>

+    <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>

+    <CodeContractsCustomRewriterAssembly />

+    <CodeContractsCustomRewriterClass />

+    <CodeContractsLibPaths />

+    <CodeContractsExtraRewriteOptions />

+    <CodeContractsExtraAnalysisOptions />

+    <CodeContractsBaseLineFile />

+    <CodeContractsCacheAnalysisResults>False</CodeContractsCacheAnalysisResults>

+    <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>

+    <CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>

+    <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>

+  </PropertyGroup>

+  <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|AnyCPU'">

+    <DebugSymbols>true</DebugSymbols>

+    <OutputPath>bin\Checked\</OutputPath>

+    <DefineConstants>DEBUG;TRACE</DefineConstants>

+    <DebugType>full</DebugType>

+    <PlatformTarget>AnyCPU</PlatformTarget>

+    <CodeAnalysisLogFile>bin\Debug\GPUVerify.exe.CodeAnalysisLog.xml</CodeAnalysisLogFile>

+    <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>

+    <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>

+    <ErrorReport>prompt</ErrorReport>

+    <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>

+    <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>

+    <CodeAnalysisIgnoreBuiltInRuleSets>true</CodeAnalysisIgnoreBuiltInRuleSets>

+    <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>

+    <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>

+    <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>

+    <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>

+    <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>

+    <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>

+    <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>

+    <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>

+    <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>

+    <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>

+    <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>

+    <CodeContractsEnumObligations>False</CodeContractsEnumObligations>

+    <CodeContractsPointerObligations>False</CodeContractsPointerObligations>

+    <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>

+    <CodeContractsRunInBackground>True</CodeContractsRunInBackground>

+    <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>

+    <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>

+    <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>

+    <CodeContractsCustomRewriterAssembly />

+    <CodeContractsCustomRewriterClass />

+    <CodeContractsLibPaths />

+    <CodeContractsExtraRewriteOptions />

+    <CodeContractsExtraAnalysisOptions />

+    <CodeContractsBaseLineFile />

+    <CodeContractsCacheAnalysisResults>False</CodeContractsCacheAnalysisResults>

+    <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>

+    <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>

+    <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>

   </PropertyGroup>

   <ItemGroup>

     <Reference Include="System" />

diff --git a/Source/ModelViewer/Namer.cs b/Source/ModelViewer/Namer.cs
index c1d7fcd3..afcb0fe6 100644
--- a/Source/ModelViewer/Namer.cs
+++ b/Source/ModelViewer/Namer.cs
@@ -159,7 +159,13 @@ namespace Microsoft.Boogie.ModelViewer
 

       Action<IEnumerable<IDisplayNode>> addList = (IEnumerable<IDisplayNode> nodes) =>

       {

-        var ch = nodes.ToDictionary(x => x.Name);

+        var ch = new Dictionary<string, IDisplayNode>();

+        foreach (var x in nodes) {

+          if (ch.ContainsKey(x.Name)) {

+            // throw new System.InvalidOperationException("duplicated model entry: " + x.Name);

+          }

+          ch[x.Name] = x;

+        }

         foreach (var k in SortFields(nodes))

           workList.Enqueue(ch[k]);

       };

diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs
index ede520cb..0ce39c88 100644
--- a/Source/ModelViewer/VccProvider.cs
+++ b/Source/ModelViewer/VccProvider.cs
@@ -395,6 +395,11 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
         return name.Substring(2);

       }

 

+      if (name.StartsWith("OP#")) {

+        kind = "out-param";

+        return name.Substring(3);

+      }

+

       if (name.StartsWith("SL#")) {

         kind = "spec local";

         return name.Substring(3);