diff options
author | 2011-11-09 00:02:52 -0800 | |
---|---|---|
committer | 2011-11-09 00:02:52 -0800 | |
commit | 2551eb125aae4fd71eec5465fa919cd58163c105 (patch) | |
tree | c8e3b616e2542d8659ac70c69c931faaa4bf9d86 | |
parent | b66ed178322cd26bbaae2591f2518e20652733bb (diff) | |
parent | e1236df70d33b581d426d07764ff192eb5042f95 (diff) |
Merge
-rw-r--r-- | .hgtags | 1 | ||||
-rw-r--r-- | Source/Boogie.sln | 26 | ||||
-rw-r--r-- | Source/GPUVerify.sln | 420 | ||||
-rw-r--r-- | Source/GPUVerify/GPUVerifier.cs | 8 | ||||
-rw-r--r-- | Source/GPUVerify/GPUVerify.csproj | 90 | ||||
-rw-r--r-- | Source/ModelViewer/Namer.cs | 8 | ||||
-rw-r--r-- | Source/ModelViewer/VccProvider.cs | 5 |
7 files changed, 520 insertions, 38 deletions
@@ -8,3 +8,4 @@ e57f596b36edd27f66ff7400a6610034ce67d19d emicvccbld_build_2.1.30905.0 8b7a180291a5ecb7d1ffa0dbc3483cc4f7685064 emicvccbld_build_2.1.31020.0 f59d45429b672bb429d26e1aff6e9df1d9def6b5 emicvccbld_build_2.1.31022.0 f3b3df39e9877fb2b3fde172f300f995689e6402 emicvccbld_build_2.1.31028.0 +f5c14add09d2f57402c94574eeef490d900d58e8 emicvccbld_build_2.1.31109.0 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);
|