Starting work on Boogie Model Viewer.

13 files changed, 1118 insertions, 0 deletions

diff --git a/Source/Boogie.sln b/Source/Boogie.sln
index 21a3f940..a1041d90 100644
--- a/Source/Boogie.sln
+++ b/Source/Boogie.sln
@@ -31,17 +31,22 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Basetypes", "Basetypes\Base
 EndProject

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

 EndProject

+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ModelViewer", "ModelViewer\ModelViewer.csproj", "{A678C6EB-B329-46A9-BBFC-7585F01ACD7C}"

+EndProject

 Global

 	GlobalSection(SolutionConfigurationPlatforms) = preSolution

 		Debug|.NET = Debug|.NET

 		Debug|Any CPU = Debug|Any CPU

 		Debug|Mixed Platforms = Debug|Mixed Platforms

+		Debug|x86 = Debug|x86

 		Release|.NET = Release|.NET

 		Release|Any CPU = Release|Any CPU

 		Release|Mixed Platforms = Release|Mixed Platforms

+		Release|x86 = Release|x86

 		z3apidebug|.NET = z3apidebug|.NET

 		z3apidebug|Any CPU = z3apidebug|Any CPU

 		z3apidebug|Mixed Platforms = z3apidebug|Mixed Platforms

+		z3apidebug|x86 = z3apidebug|x86

 	EndGlobalSection

 	GlobalSection(ProjectConfigurationPlatforms) = postSolution

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

@@ -50,216 +55,276 @@ Global
 		{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|.NET.ActiveCfg = Release|Any CPU

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

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

 		{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|.NET.ActiveCfg = z3apidebug|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 = Debug|Any CPU

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

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

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

 		{435D5BD0-6F62-49F8-BB24-33E2257519AD}.Debug|.NET.Build.0 = Debug|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|.NET.ActiveCfg = Release|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|.NET.ActiveCfg = z3apidebug|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 = Debug|Any CPU

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

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

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

 		{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}.Debug|.NET.Build.0 = Debug|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|.NET.ActiveCfg = Release|Any CPU

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

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

 		{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|.NET.ActiveCfg = z3apidebug|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 = Debug|Any CPU

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

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

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

 		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.Debug|.NET.Build.0 = Debug|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|.NET.ActiveCfg = Release|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|.NET.ActiveCfg = z3apidebug|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 = Debug|Any CPU

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

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

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

 		{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Debug|.NET.Build.0 = Debug|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|.NET.ActiveCfg = Release|Any CPU

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

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

 		{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|.NET.ActiveCfg = z3apidebug|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 = Debug|Any CPU

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

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

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

 		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.Debug|.NET.Build.0 = Debug|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|.NET.ActiveCfg = Release|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|.NET.ActiveCfg = z3apidebug|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 = Debug|Any CPU

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

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

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

 		{E1F10180-C7B9-4147-B51F-FA1B701966DC}.Debug|.NET.Build.0 = Debug|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|.NET.ActiveCfg = Release|Any CPU

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

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

 		{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|.NET.ActiveCfg = z3apidebug|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 = Debug|Any CPU

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

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

 		{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}.Debug|.NET.ActiveCfg = Debug|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|.NET.ActiveCfg = Release|Any CPU

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

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

 		{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|.NET.ActiveCfg = z3apidebug|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 = Debug|Any CPU

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

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

 		{B230A69C-C466-4065-B9C1-84D80E76D802}.Debug|.NET.ActiveCfg = Debug|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|.NET.ActiveCfg = Release|Any CPU

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

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

 		{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|.NET.ActiveCfg = z3apidebug|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 = Debug|Any CPU

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

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

 		{966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Debug|.NET.ActiveCfg = Debug|Any CPU

 		{966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Debug|Any CPU.ActiveCfg = Debug|Any CPU

 		{966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Debug|Any CPU.Build.0 = Debug|Any CPU

 		{966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU

+		{966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Debug|x86.ActiveCfg = Debug|Any CPU

 		{966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Release|.NET.ActiveCfg = Release|Any CPU

 		{966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Release|Any CPU.ActiveCfg = Release|Any CPU

 		{966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Release|Any CPU.Build.0 = Release|Any CPU

 		{966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU

 		{966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Release|Mixed Platforms.Build.0 = Release|Any CPU

+		{966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Release|x86.ActiveCfg = Release|Any CPU

 		{966DD87B-A29D-4F3C-9406-F680A61DC0E0}.z3apidebug|.NET.ActiveCfg = z3apidebug|Any CPU

 		{966DD87B-A29D-4F3C-9406-F680A61DC0E0}.z3apidebug|Any CPU.ActiveCfg = z3apidebug|Any CPU

 		{966DD87B-A29D-4F3C-9406-F680A61DC0E0}.z3apidebug|Any CPU.Build.0 = z3apidebug|Any CPU

 		{966DD87B-A29D-4F3C-9406-F680A61DC0E0}.z3apidebug|Mixed Platforms.ActiveCfg = z3apidebug|Any CPU

 		{966DD87B-A29D-4F3C-9406-F680A61DC0E0}.z3apidebug|Mixed Platforms.Build.0 = z3apidebug|Any CPU

+		{966DD87B-A29D-4F3C-9406-F680A61DC0E0}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU

 		{39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Debug|.NET.ActiveCfg = Debug|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|.NET.ActiveCfg = Release|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|.NET.ActiveCfg = z3apidebug|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 = Debug|Any CPU

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

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

 		{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.Debug|.NET.ActiveCfg = Debug|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|.NET.ActiveCfg = Release|Any CPU

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

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

 		{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|.NET.ActiveCfg = z3apidebug|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 = Debug|Any CPU

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

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

 		{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Debug|.NET.ActiveCfg = Debug|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|.NET.ActiveCfg = Release|Any CPU

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

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

 		{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|.NET.ActiveCfg = z3apidebug|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 = Debug|Any CPU

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

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

 		{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}.Debug|.NET.ActiveCfg = Debug|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|.NET.ActiveCfg = Release|Any CPU

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

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

 		{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|.NET.ActiveCfg = z3apidebug|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 = Debug|Any CPU

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

 	EndGlobalSection

 	GlobalSection(SolutionProperties) = preSolution

 		HideSolutionNode = FALSE

diff --git a/Source/ModelViewer/Main.Designer.cs b/Source/ModelViewer/Main.Designer.cs
new file mode 100644
index 00000000..64aab748
--- /dev/null
+++ b/Source/ModelViewer/Main.Designer.cs
@@ -0,0 +1,91 @@
+namespace ModelViewer

+{

+  partial class Main

+  {

+    /// <summary>

+    /// Required designer variable.

+    /// </summary>

+    private System.ComponentModel.IContainer components = null;

+

+    /// <summary>

+    /// Clean up any resources being used.

+    /// </summary>

+    /// <param name="disposing">true if managed resources should be disposed; otherwise, false.</param>

+    protected override void Dispose(bool disposing)

+    {

+      if (disposing && (components != null)) {

+        components.Dispose();

+      }

+      base.Dispose(disposing);

+    }

+

+    #region Windows Form Designer generated code

+

+    /// <summary>

+    /// Required method for Designer support - do not modify

+    /// the contents of this method with the code editor.

+    /// </summary>

+    private void InitializeComponent()

+    {

+      this.listView1 = new System.Windows.Forms.ListView();

+      this.name = ((System.Windows.Forms.ColumnHeader)(new System.Windows.Forms.ColumnHeader()));

+      this.value = ((System.Windows.Forms.ColumnHeader)(new System.Windows.Forms.ColumnHeader()));

+      this.SuspendLayout();

+      // 

+      // listView1

+      // 

+      this.listView1.Columns.AddRange(new System.Windows.Forms.ColumnHeader[] {

+            this.name,

+            this.value});

+      this.listView1.Dock = System.Windows.Forms.DockStyle.Fill;

+      this.listView1.FullRowSelect = true;

+      this.listView1.GridLines = true;

+      this.listView1.HeaderStyle = System.Windows.Forms.ColumnHeaderStyle.Nonclickable;

+      this.listView1.Location = new System.Drawing.Point(0, 0);

+      this.listView1.MultiSelect = false;

+      this.listView1.Name = "listView1";

+      this.listView1.OwnerDraw = true;

+      this.listView1.ShowItemToolTips = true;

+      this.listView1.Size = new System.Drawing.Size(851, 689);

+      this.listView1.TabIndex = 0;

+      this.listView1.UseCompatibleStateImageBehavior = false;

+      this.listView1.View = System.Windows.Forms.View.Details;

+      this.listView1.ColumnWidthChanged += new System.Windows.Forms.ColumnWidthChangedEventHandler(this.listView1_ColumnWidthChanged);

+      this.listView1.DrawColumnHeader += new System.Windows.Forms.DrawListViewColumnHeaderEventHandler(this.listView1_DrawColumnHeader);

+      this.listView1.DrawItem += new System.Windows.Forms.DrawListViewItemEventHandler(this.listView1_DrawItem);

+      this.listView1.DrawSubItem += new System.Windows.Forms.DrawListViewSubItemEventHandler(this.listView1_DrawSubItem);

+      this.listView1.MouseMove += new System.Windows.Forms.MouseEventHandler(this.listView1_MouseMove);

+      this.listView1.MouseUp += new System.Windows.Forms.MouseEventHandler(this.listView1_MouseUp);

+      // 

+      // name

+      // 

+      this.name.Text = "Name";

+      this.name.Width = 190;

+      // 

+      // value

+      // 

+      this.value.Text = "Value";

+      this.value.Width = 500;

+      // 

+      // Main

+      // 

+      this.AutoScaleDimensions = new System.Drawing.SizeF(6F, 13F);

+      this.AutoScaleMode = System.Windows.Forms.AutoScaleMode.Font;

+      this.ClientSize = new System.Drawing.Size(851, 689);

+      this.Controls.Add(this.listView1);

+      this.Name = "Main";

+      this.Text = "Boogie Model Viewer";

+      this.ResumeLayout(false);

+

+    }

+

+    #endregion

+

+    private System.Windows.Forms.ListView listView1;

+    private System.Windows.Forms.ColumnHeader name;

+    private System.Windows.Forms.ColumnHeader value;

+

+

+  }

+}

+

diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs
new file mode 100644
index 00000000..575721cd
--- /dev/null
+++ b/Source/ModelViewer/Main.cs
@@ -0,0 +1,257 @@
+using System;

+using System.Collections.Generic;

+using System.ComponentModel;

+using System.Data;

+using System.Drawing;

+using System.Drawing.Drawing2D;

+using System.Linq;

+using System.Text;

+using System.Windows.Forms;

+

+using System.IO;

+using Microsoft.Boogie;

+

+namespace ModelViewer

+{

+  public partial class Main : Form

+  {

+    public string SearchText;

+

+    public Main()

+    {

+      InitializeComponent();

+

+      var args = Environment.GetCommandLineArgs();

+      Model m;

+

+      using (var rd = File.OpenText(args[1])) {

+        var models = Model.ParseModels(rd);

+        m = models[0];

+      }

+

+      var items = new List<ListViewItem>();

+      foreach (var s in m.States)

+        items.Add(new DisplayItem(new StateNode(s)));

+      listView1.Items.AddRange(items.ToArray());

+

+      listView1.Columns[1].Width = listView1.Width - listView1.Columns[0].Width - 5;

+    }

+

+    internal void Activate(TreeNode treeNode)

+    {

+      throw new NotImplementedException();

+    }

+

+    private void listBox1_SelectedIndexChanged(object sender, EventArgs e)

+    {

+

+    }

+

+    const int levelMult = 10;

+    const int plusWidth = 17;

+    

+    private void listView1_DrawItem(object sender, DrawListViewItemEventArgs e)

+    {

+      var item = (DisplayItem)e.Item;

+      var rect = e.Bounds;

+      rect.Height -= 1;

+

+      var textBrush = Brushes.Black;

+      if ((e.State & ListViewItemStates.Selected) != 0) {

+        // Draw the background and focus rectangle for a selected item.

+        e.Graphics.FillRectangle(Brushes.Navy, rect);

+        e.DrawFocusRectangle();

+        textBrush = Brushes.White;

+      } else {

+        e.Graphics.FillRectangle(Brushes.White, rect);

+      }

+

+      var off = levelMult * item.level;

+      var plusRect = rect;

+      plusRect.Width = plusWidth;

+      plusRect.X += off;

+      e.Graphics.FillRectangle(Brushes.Gray, plusRect);

+      e.Graphics.DrawString(item.expanded ? "[-]" : "[+]", listView1.Font, Brushes.Black, plusRect); // , StringFormat.GenericDefault);

+

+      off += plusWidth + 3;

+      var valRect = rect;

+      valRect.Width = listView1.Columns[0].Width - 1 - off;

+      if (valRect.Width > 10) {

+        valRect.X += off;

+        e.Graphics.DrawString(item.displayNode.Name, listView1.Font, textBrush, valRect); // , StringFormat.GenericDefault);

+      }

+

+      var nameRect = rect;

+      nameRect.Width = listView1.Columns[1].Width - 1;

+      nameRect.X += listView1.Columns[0].Width + 1;

+      e.Graphics.DrawString(item.SubItems[1].Text, listView1.Font, textBrush, nameRect); // , StringFormat.GenericDefault);

+    }

+

+    private void listView1_DrawSubItem(object sender, DrawListViewSubItemEventArgs e)

+    {

+    }

+

+    private void listView1_DrawColumnHeader(object sender, DrawListViewColumnHeaderEventArgs e)

+    {

+      e.DrawBackground();

+      e.DrawText();

+    }

+

+    private void listView1_MouseMove(object sender, MouseEventArgs e)

+    {

+    }

+

+    private void listView1_MouseUp(object sender, MouseEventArgs e)

+    {

+      var clickedItem = (DisplayItem)listView1.GetItemAt(5, e.Y);

+      if (clickedItem != null) {

+        clickedItem.Selected = true;

+        clickedItem.Focused = true;

+

+        int plusLoc = clickedItem.level * levelMult;

+        if (e.X >= plusLoc && e.X <= plusLoc + plusWidth) {

+          clickedItem.expanded = !clickedItem.expanded;

+

+          if (clickedItem.expanded) {

+            if (clickedItem.collapsedChildren == null) {

+              var items = new List<DisplayItem>();

+              foreach (var ch in clickedItem.displayNode.Expand()) {

+                var it = new DisplayItem(ch);

+                it.level = clickedItem.level + 1;

+                items.Add(it);

+              }

+              clickedItem.collapsedChildren = items.ToArray();

+            }

+            var pos = clickedItem.Index + 1;

+            listView1.BeginUpdate();

+            foreach (var it in clickedItem.collapsedChildren) {

+              listView1.Items.Insert(pos, it);

+              pos++;

+            }

+            listView1.EndUpdate();

+          } else {

+            var collapsed = new List<DisplayItem>();

+            var beg = clickedItem.Index + 1;

+            for (int i = beg; i < listView1.Items.Count; ++i) {

+              var curr = (DisplayItem)listView1.Items[i];

+              if (curr.level == clickedItem.level) break;

+              collapsed.Add(curr);

+            }

+            clickedItem.collapsedChildren = collapsed.ToArray();

+            listView1.BeginUpdate();

+            for (int i = 0; i < collapsed.Count; ++i)

+              listView1.Items.RemoveAt(beg);

+            listView1.EndUpdate();

+          }

+

+          listView1.Invalidate();

+        }

+      }

+    }

+

+    private void listView1_ColumnWidthChanged(object sender, ColumnWidthChangedEventArgs e)

+    {

+      listView1.Invalidate();

+    }

+

+  }

+

+  internal class DisplayItem : ListViewItem

+  {

+    internal IDisplayNode displayNode;

+    internal bool expanded;

+    internal int level;

+    internal DisplayItem[] collapsedChildren;

+

+    internal DisplayItem(IDisplayNode d)

+       : base(d.Name)

+    {

+      displayNode = d;

+      displayNode.ViewSync = this;

+      expanded = false;

+

+      var sb = new StringBuilder();

+      foreach (var n in displayNode.Values) {

+        sb.Append(n).Append(", ");

+        if (sb.Length > 300)

+          break;

+      }

+      if (sb.Length > 2) sb.Length -= 2;

+

+      this.SubItems.Add(sb.ToString());

+    }

+  }

+

+  public interface IDisplayNode

+  {

+    string Name { get; }

+    IEnumerable<string> Values { get; }

+    bool Expandable { get; }

+    IEnumerable<IDisplayNode> Expand();

+    object ViewSync { get; set; }

+  }

+

+  public class StateNode : IDisplayNode

+  {

+    protected Model.CapturedState state;

+

+    public StateNode(Model.CapturedState s)

+    {

+      state = s;

+    }

+

+    public virtual string Name

+    {

+      get { return "State"; }

+    }

+

+    public virtual IEnumerable<string> Values

+    {

+      get { yield return state.Name; }

+    }

+

+    public virtual bool Expandable { get { return state.VariableCount != 0; } }

+    

+    public virtual IEnumerable<IDisplayNode> Expand()

+    {

+      foreach (var v in state.Variables) {

+        yield return new ElementNode(v, state.TryGet(v));

+      }

+    }

+

+    public object ViewSync { get; set; }

+  }

+

+  public class ElementNode : IDisplayNode

+  {

+    protected Model.Element elt;

+    protected string name;

+

+    public ElementNode(string name, Model.Element elt) { 

+      this.name = name; 

+      this.elt = elt; 

+    }

+

+    public virtual string Name

+    {

+      get { return name; }

+    }

+

+    public virtual IEnumerable<string> Values

+    {

+      get {

+        if (!(elt is Model.Uninterpreted))

+          yield return elt.ToString();

+        foreach (var tupl in elt.Names) {

+          if (tupl.Func.Arity == 0)

+            yield return tupl.Func.Name;

+        }

+      }

+    }

+

+    public virtual bool Expandable { get { return false; } }

+    public virtual IEnumerable<IDisplayNode> Expand() { yield break; }

+

+    public object ViewSync { get; set; }

+  }

+}

diff --git a/Source/ModelViewer/Main.resx b/Source/ModelViewer/Main.resx
new file mode 100644
index 00000000..29dcb1b3
--- /dev/null
+++ b/Source/ModelViewer/Main.resx
@@ -0,0 +1,120 @@
+<?xml version="1.0" encoding="utf-8"?>

+<root>

+  <!-- 

+    Microsoft ResX Schema 

+    

+    Version 2.0

+    

+    The primary goals of this format is to allow a simple XML format 

+    that is mostly human readable. The generation and parsing of the 

+    various data types are done through the TypeConverter classes 

+    associated with the data types.

+    

+    Example:

+    

+    ... ado.net/XML headers & schema ...

+    <resheader name="resmimetype">text/microsoft-resx</resheader>

+    <resheader name="version">2.0</resheader>

+    <resheader name="reader">System.Resources.ResXResourceReader, System.Windows.Forms, ...</resheader>

+    <resheader name="writer">System.Resources.ResXResourceWriter, System.Windows.Forms, ...</resheader>

+    <data name="Name1"><value>this is my long string</value><comment>this is a comment</comment></data>

+    <data name="Color1" type="System.Drawing.Color, System.Drawing">Blue</data>

+    <data name="Bitmap1" mimetype="application/x-microsoft.net.object.binary.base64">

+        <value>[base64 mime encoded serialized .NET Framework object]</value>

+    </data>

+    <data name="Icon1" type="System.Drawing.Icon, System.Drawing" mimetype="application/x-microsoft.net.object.bytearray.base64">

+        <value>[base64 mime encoded string representing a byte array form of the .NET Framework object]</value>

+        <comment>This is a comment</comment>

+    </data>

+                

+    There are any number of "resheader" rows that contain simple 

+    name/value pairs.

+    

+    Each data row contains a name, and value. The row also contains a 

+    type or mimetype. Type corresponds to a .NET class that support 

+    text/value conversion through the TypeConverter architecture. 

+    Classes that don't support this are serialized and stored with the 

+    mimetype set.

+    

+    The mimetype is used for serialized objects, and tells the 

+    ResXResourceReader how to depersist the object. This is currently not 

+    extensible. For a given mimetype the value must be set accordingly:

+    

+    Note - application/x-microsoft.net.object.binary.base64 is the format 

+    that the ResXResourceWriter will generate, however the reader can 

+    read any of the formats listed below.

+    

+    mimetype: application/x-microsoft.net.object.binary.base64

+    value   : The object must be serialized with 

+            : System.Runtime.Serialization.Formatters.Binary.BinaryFormatter

+            : and then encoded with base64 encoding.

+    

+    mimetype: application/x-microsoft.net.object.soap.base64

+    value   : The object must be serialized with 

+            : System.Runtime.Serialization.Formatters.Soap.SoapFormatter

+            : and then encoded with base64 encoding.

+

+    mimetype: application/x-microsoft.net.object.bytearray.base64

+    value   : The object must be serialized into a byte array 

+            : using a System.ComponentModel.TypeConverter

+            : and then encoded with base64 encoding.

+    -->

+  <xsd:schema id="root" xmlns="" xmlns:xsd="http://www.w3.org/2001/XMLSchema" xmlns:msdata="urn:schemas-microsoft-com:xml-msdata">

+    <xsd:import namespace="http://www.w3.org/XML/1998/namespace" />

+    <xsd:element name="root" msdata:IsDataSet="true">

+      <xsd:complexType>

+        <xsd:choice maxOccurs="unbounded">

+          <xsd:element name="metadata">

+            <xsd:complexType>

+              <xsd:sequence>

+                <xsd:element name="value" type="xsd:string" minOccurs="0" />

+              </xsd:sequence>

+              <xsd:attribute name="name" use="required" type="xsd:string" />

+              <xsd:attribute name="type" type="xsd:string" />

+              <xsd:attribute name="mimetype" type="xsd:string" />

+              <xsd:attribute ref="xml:space" />

+            </xsd:complexType>

+          </xsd:element>

+          <xsd:element name="assembly">

+            <xsd:complexType>

+              <xsd:attribute name="alias" type="xsd:string" />

+              <xsd:attribute name="name" type="xsd:string" />

+            </xsd:complexType>

+          </xsd:element>

+          <xsd:element name="data">

+            <xsd:complexType>

+              <xsd:sequence>

+                <xsd:element name="value" type="xsd:string" minOccurs="0" msdata:Ordinal="1" />

+                <xsd:element name="comment" type="xsd:string" minOccurs="0" msdata:Ordinal="2" />

+              </xsd:sequence>

+              <xsd:attribute name="name" type="xsd:string" use="required" msdata:Ordinal="1" />

+              <xsd:attribute name="type" type="xsd:string" msdata:Ordinal="3" />

+              <xsd:attribute name="mimetype" type="xsd:string" msdata:Ordinal="4" />

+              <xsd:attribute ref="xml:space" />

+            </xsd:complexType>

+          </xsd:element>

+          <xsd:element name="resheader">

+            <xsd:complexType>

+              <xsd:sequence>

+                <xsd:element name="value" type="xsd:string" minOccurs="0" msdata:Ordinal="1" />

+              </xsd:sequence>

+              <xsd:attribute name="name" type="xsd:string" use="required" />

+            </xsd:complexType>

+          </xsd:element>

+        </xsd:choice>

+      </xsd:complexType>

+    </xsd:element>

+  </xsd:schema>

+  <resheader name="resmimetype">

+    <value>text/microsoft-resx</value>

+  </resheader>

+  <resheader name="version">

+    <value>2.0</value>

+  </resheader>

+  <resheader name="reader">

+    <value>System.Resources.ResXResourceReader, System.Windows.Forms, Version=4.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089</value>

+  </resheader>

+  <resheader name="writer">

+    <value>System.Resources.ResXResourceWriter, System.Windows.Forms, Version=4.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089</value>

+  </resheader>

+</root>
\ No newline at end of file
diff --git a/Source/ModelViewer/ModelViewer.csproj b/Source/ModelViewer/ModelViewer.csproj
new file mode 100644
index 00000000..db4e039c
--- /dev/null
+++ b/Source/ModelViewer/ModelViewer.csproj
@@ -0,0 +1,94 @@
+<?xml version="1.0" encoding="utf-8"?>

+<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>

+    <ProductVersion>8.0.30703</ProductVersion>

+    <SchemaVersion>2.0</SchemaVersion>

+    <ProjectGuid>{A678C6EB-B329-46A9-BBFC-7585F01ACD7C}</ProjectGuid>

+    <OutputType>WinExe</OutputType>

+    <AppDesignerFolder>Properties</AppDesignerFolder>

+    <RootNamespace>ModelViewer</RootNamespace>

+    <AssemblyName>ModelViewer</AssemblyName>

+    <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>

+    <TargetFrameworkProfile>Client</TargetFrameworkProfile>

+    <FileAlignment>512</FileAlignment>

+  </PropertyGroup>

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

+    <PlatformTarget>x86</PlatformTarget>

+    <DebugSymbols>true</DebugSymbols>

+    <DebugType>full</DebugType>

+    <Optimize>false</Optimize>

+    <OutputPath>bin\Debug\</OutputPath>

+    <DefineConstants>DEBUG;TRACE</DefineConstants>

+    <ErrorReport>prompt</ErrorReport>

+    <WarningLevel>4</WarningLevel>

+  </PropertyGroup>

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

+    <PlatformTarget>x86</PlatformTarget>

+    <DebugType>pdbonly</DebugType>

+    <Optimize>true</Optimize>

+    <OutputPath>bin\Release\</OutputPath>

+    <DefineConstants>TRACE</DefineConstants>

+    <ErrorReport>prompt</ErrorReport>

+    <WarningLevel>4</WarningLevel>

+  </PropertyGroup>

+  <ItemGroup>

+    <Reference Include="System" />

+    <Reference Include="System.Core" />

+    <Reference Include="System.Xml.Linq" />

+    <Reference Include="System.Data.DataSetExtensions" />

+    <Reference Include="Microsoft.CSharp" />

+    <Reference Include="System.Data" />

+    <Reference Include="System.Deployment" />

+    <Reference Include="System.Drawing" />

+    <Reference Include="System.Windows.Forms" />

+    <Reference Include="System.Xml" />

+  </ItemGroup>

+  <ItemGroup>

+    <Compile Include="Main.cs">

+      <SubType>Form</SubType>

+    </Compile>

+    <Compile Include="Main.Designer.cs">

+      <DependentUpon>Main.cs</DependentUpon>

+    </Compile>

+    <Compile Include="..\VCGeneration\Model.cs" />

+    <Compile Include="Program.cs" />

+    <Compile Include="Properties\AssemblyInfo.cs" />

+    <Compile Include="SearchBox.cs">

+      <SubType>Form</SubType>

+    </Compile>

+    <Compile Include="SearchBox.Designer.cs">

+      <DependentUpon>SearchBox.cs</DependentUpon>

+    </Compile>

+    <EmbeddedResource Include="Main.resx">

+      <DependentUpon>Main.cs</DependentUpon>

+    </EmbeddedResource>

+    <EmbeddedResource Include="Properties\Resources.resx">

+      <Generator>ResXFileCodeGenerator</Generator>

+      <LastGenOutput>Resources.Designer.cs</LastGenOutput>

+      <SubType>Designer</SubType>

+    </EmbeddedResource>

+    <Compile Include="Properties\Resources.Designer.cs">

+      <AutoGen>True</AutoGen>

+      <DependentUpon>Resources.resx</DependentUpon>

+    </Compile>

+    <None Include="Properties\Settings.settings">

+      <Generator>SettingsSingleFileGenerator</Generator>

+      <LastGenOutput>Settings.Designer.cs</LastGenOutput>

+    </None>

+    <Compile Include="Properties\Settings.Designer.cs">

+      <AutoGen>True</AutoGen>

+      <DependentUpon>Settings.settings</DependentUpon>

+      <DesignTimeSharedInput>True</DesignTimeSharedInput>

+    </Compile>

+  </ItemGroup>

+  <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />

+  <!-- To modify your build process, add your task inside one of the targets below and uncomment it. 

+       Other similar extension points exist, see Microsoft.Common.targets.

+  <Target Name="BeforeBuild">

+  </Target>

+  <Target Name="AfterBuild">

+  </Target>

+  -->

+</Project>

diff --git a/Source/ModelViewer/Program.cs b/Source/ModelViewer/Program.cs
new file mode 100644
index 00000000..ca2c85cc
--- /dev/null
+++ b/Source/ModelViewer/Program.cs
@@ -0,0 +1,21 @@
+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Windows.Forms;

+

+namespace ModelViewer

+{

+  static class Program

+  {

+    /// <summary>

+    /// The main entry point for the application.

+    /// </summary>

+    [STAThread]

+    static void Main()

+    {

+      Application.EnableVisualStyles();

+      Application.SetCompatibleTextRenderingDefault(false);

+      Application.Run(new Main());

+    }

+  }

+}

diff --git a/Source/ModelViewer/Properties/AssemblyInfo.cs b/Source/ModelViewer/Properties/AssemblyInfo.cs
new file mode 100644
index 00000000..10000461
--- /dev/null
+++ b/Source/ModelViewer/Properties/AssemblyInfo.cs
@@ -0,0 +1,36 @@
+using System.Reflection;

+using System.Runtime.CompilerServices;

+using System.Runtime.InteropServices;

+

+// General Information about an assembly is controlled through the following 

+// set of attributes. Change these attribute values to modify the information

+// associated with an assembly.

+[assembly: AssemblyTitle("ModelViewer")]

+[assembly: AssemblyDescription("")]

+[assembly: AssemblyConfiguration("")]

+[assembly: AssemblyCompany("Microsoft")]

+[assembly: AssemblyProduct("ModelViewer")]

+[assembly: AssemblyCopyright("Copyright © Microsoft 2010")]

+[assembly: AssemblyTrademark("")]

+[assembly: AssemblyCulture("")]

+

+// Setting ComVisible to false makes the types in this assembly not visible 

+// to COM components.  If you need to access a type in this assembly from 

+// COM, set the ComVisible attribute to true on that type.

+[assembly: ComVisible(false)]

+

+// The following GUID is for the ID of the typelib if this project is exposed to COM

+[assembly: Guid("fb95289d-cd57-47f2-aafa-d9e39f46555e")]

+

+// Version information for an assembly consists of the following four values:

+//

+//      Major Version

+//      Minor Version 

+//      Build Number

+//      Revision

+//

+// You can specify all the values or you can default the Build and Revision Numbers 

+// by using the '*' as shown below:

+// [assembly: AssemblyVersion("1.0.*")]

+[assembly: AssemblyVersion("1.0.0.0")]

+[assembly: AssemblyFileVersion("1.0.0.0")]

diff --git a/Source/ModelViewer/Properties/Resources.Designer.cs b/Source/ModelViewer/Properties/Resources.Designer.cs
new file mode 100644
index 00000000..3ed62cd5
--- /dev/null
+++ b/Source/ModelViewer/Properties/Resources.Designer.cs
@@ -0,0 +1,70 @@
+//------------------------------------------------------------------------------

+// <auto-generated>

+//     This code was generated by a tool.

+//     Runtime Version:4.0.30319.1

+//

+//     Changes to this file may cause incorrect behavior and will be lost if

+//     the code is regenerated.

+// </auto-generated>

+//------------------------------------------------------------------------------

+

+namespace ModelViewer.Properties

+{

+

+

+  /// <summary>

+  ///   A strongly-typed resource class, for looking up localized strings, etc.

+  /// </summary>

+  // This class was auto-generated by the StronglyTypedResourceBuilder

+  // class via a tool like ResGen or Visual Studio.

+  // To add or remove a member, edit your .ResX file then rerun ResGen

+  // with the /str option, or rebuild your VS project.

+  [global::System.CodeDom.Compiler.GeneratedCodeAttribute("System.Resources.Tools.StronglyTypedResourceBuilder", "4.0.0.0")]

+  [global::System.Diagnostics.DebuggerNonUserCodeAttribute()]

+  [global::System.Runtime.CompilerServices.CompilerGeneratedAttribute()]

+  internal class Resources

+  {

+

+    private static global::System.Resources.ResourceManager resourceMan;

+

+    private static global::System.Globalization.CultureInfo resourceCulture;

+

+    [global::System.Diagnostics.CodeAnalysis.SuppressMessageAttribute("Microsoft.Performance", "CA1811:AvoidUncalledPrivateCode")]

+    internal Resources()

+    {

+    }

+

+    /// <summary>

+    ///   Returns the cached ResourceManager instance used by this class.

+    /// </summary>

+    [global::System.ComponentModel.EditorBrowsableAttribute(global::System.ComponentModel.EditorBrowsableState.Advanced)]

+    internal static global::System.Resources.ResourceManager ResourceManager

+    {

+      get

+      {

+        if ((resourceMan == null)) {

+          global::System.Resources.ResourceManager temp = new global::System.Resources.ResourceManager("ModelViewer.Properties.Resources", typeof(Resources).Assembly);

+          resourceMan = temp;

+        }

+        return resourceMan;

+      }

+    }

+

+    /// <summary>

+    ///   Overrides the current thread's CurrentUICulture property for all

+    ///   resource lookups using this strongly typed resource class.

+    /// </summary>

+    [global::System.ComponentModel.EditorBrowsableAttribute(global::System.ComponentModel.EditorBrowsableState.Advanced)]

+    internal static global::System.Globalization.CultureInfo Culture

+    {

+      get

+      {

+        return resourceCulture;

+      }

+      set

+      {

+        resourceCulture = value;

+      }

+    }

+  }

+}

diff --git a/Source/ModelViewer/Properties/Resources.resx b/Source/ModelViewer/Properties/Resources.resx
new file mode 100644
index 00000000..ffecec85
--- /dev/null
+++ b/Source/ModelViewer/Properties/Resources.resx
@@ -0,0 +1,117 @@
+<?xml version="1.0" encoding="utf-8"?>

+<root>

+  <!-- 

+    Microsoft ResX Schema 

+    

+    Version 2.0

+    

+    The primary goals of this format is to allow a simple XML format 

+    that is mostly human readable. The generation and parsing of the 

+    various data types are done through the TypeConverter classes 

+    associated with the data types.

+    

+    Example:

+    

+    ... ado.net/XML headers & schema ...

+    <resheader name="resmimetype">text/microsoft-resx</resheader>

+    <resheader name="version">2.0</resheader>

+    <resheader name="reader">System.Resources.ResXResourceReader, System.Windows.Forms, ...</resheader>

+    <resheader name="writer">System.Resources.ResXResourceWriter, System.Windows.Forms, ...</resheader>

+    <data name="Name1"><value>this is my long string</value><comment>this is a comment</comment></data>

+    <data name="Color1" type="System.Drawing.Color, System.Drawing">Blue</data>

+    <data name="Bitmap1" mimetype="application/x-microsoft.net.object.binary.base64">

+        <value>[base64 mime encoded serialized .NET Framework object]</value>

+    </data>

+    <data name="Icon1" type="System.Drawing.Icon, System.Drawing" mimetype="application/x-microsoft.net.object.bytearray.base64">

+        <value>[base64 mime encoded string representing a byte array form of the .NET Framework object]</value>

+        <comment>This is a comment</comment>

+    </data>

+                

+    There are any number of "resheader" rows that contain simple 

+    name/value pairs.

+    

+    Each data row contains a name, and value. The row also contains a 

+    type or mimetype. Type corresponds to a .NET class that support 

+    text/value conversion through the TypeConverter architecture. 

+    Classes that don't support this are serialized and stored with the 

+    mimetype set.

+    

+    The mimetype is used for serialized objects, and tells the 

+    ResXResourceReader how to depersist the object. This is currently not 

+    extensible. For a given mimetype the value must be set accordingly:

+    

+    Note - application/x-microsoft.net.object.binary.base64 is the format 

+    that the ResXResourceWriter will generate, however the reader can 

+    read any of the formats listed below.

+    

+    mimetype: application/x-microsoft.net.object.binary.base64

+    value   : The object must be serialized with 

+            : System.Serialization.Formatters.Binary.BinaryFormatter

+            : and then encoded with base64 encoding.

+    

+    mimetype: application/x-microsoft.net.object.soap.base64

+    value   : The object must be serialized with 

+            : System.Runtime.Serialization.Formatters.Soap.SoapFormatter

+            : and then encoded with base64 encoding.

+

+    mimetype: application/x-microsoft.net.object.bytearray.base64

+    value   : The object must be serialized into a byte array 

+            : using a System.ComponentModel.TypeConverter

+            : and then encoded with base64 encoding.

+    -->

+  <xsd:schema id="root" xmlns="" xmlns:xsd="http://www.w3.org/2001/XMLSchema" xmlns:msdata="urn:schemas-microsoft-com:xml-msdata">

+    <xsd:element name="root" msdata:IsDataSet="true">

+      <xsd:complexType>

+        <xsd:choice maxOccurs="unbounded">

+          <xsd:element name="metadata">

+            <xsd:complexType>

+              <xsd:sequence>

+                <xsd:element name="value" type="xsd:string" minOccurs="0" />

+              </xsd:sequence>

+              <xsd:attribute name="name" type="xsd:string" />

+              <xsd:attribute name="type" type="xsd:string" />

+              <xsd:attribute name="mimetype" type="xsd:string" />

+            </xsd:complexType>

+          </xsd:element>

+          <xsd:element name="assembly">

+            <xsd:complexType>

+              <xsd:attribute name="alias" type="xsd:string" />

+              <xsd:attribute name="name" type="xsd:string" />

+            </xsd:complexType>

+          </xsd:element>

+          <xsd:element name="data">

+            <xsd:complexType>

+              <xsd:sequence>

+                <xsd:element name="value" type="xsd:string" minOccurs="0" msdata:Ordinal="1" />

+                <xsd:element name="comment" type="xsd:string" minOccurs="0" msdata:Ordinal="2" />

+              </xsd:sequence>

+              <xsd:attribute name="name" type="xsd:string" msdata:Ordinal="1" />

+              <xsd:attribute name="type" type="xsd:string" msdata:Ordinal="3" />

+              <xsd:attribute name="mimetype" type="xsd:string" msdata:Ordinal="4" />

+            </xsd:complexType>

+          </xsd:element>

+          <xsd:element name="resheader">

+            <xsd:complexType>

+              <xsd:sequence>

+                <xsd:element name="value" type="xsd:string" minOccurs="0" msdata:Ordinal="1" />

+              </xsd:sequence>

+              <xsd:attribute name="name" type="xsd:string" use="required" />

+            </xsd:complexType>

+          </xsd:element>

+        </xsd:choice>

+      </xsd:complexType>

+    </xsd:element>

+  </xsd:schema>

+  <resheader name="resmimetype">

+    <value>text/microsoft-resx</value>

+  </resheader>

+  <resheader name="version">

+    <value>2.0</value>

+  </resheader>

+  <resheader name="reader">

+    <value>System.Resources.ResXResourceReader, System.Windows.Forms, Version=2.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089</value>

+  </resheader>

+  <resheader name="writer">

+    <value>System.Resources.ResXResourceWriter, System.Windows.Forms, Version=2.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089</value>

+  </resheader>

+</root>
\ No newline at end of file
diff --git a/Source/ModelViewer/Properties/Settings.Designer.cs b/Source/ModelViewer/Properties/Settings.Designer.cs
new file mode 100644
index 00000000..5f03f3a1
--- /dev/null
+++ b/Source/ModelViewer/Properties/Settings.Designer.cs
@@ -0,0 +1,30 @@
+//------------------------------------------------------------------------------

+// <auto-generated>

+//     This code was generated by a tool.

+//     Runtime Version:4.0.30319.1

+//

+//     Changes to this file may cause incorrect behavior and will be lost if

+//     the code is regenerated.

+// </auto-generated>

+//------------------------------------------------------------------------------

+

+namespace ModelViewer.Properties

+{

+

+

+  [global::System.Runtime.CompilerServices.CompilerGeneratedAttribute()]

+  [global::System.CodeDom.Compiler.GeneratedCodeAttribute("Microsoft.VisualStudio.Editors.SettingsDesigner.SettingsSingleFileGenerator", "10.0.0.0")]

+  internal sealed partial class Settings : global::System.Configuration.ApplicationSettingsBase

+  {

+

+    private static Settings defaultInstance = ((Settings)(global::System.Configuration.ApplicationSettingsBase.Synchronized(new Settings())));

+

+    public static Settings Default

+    {

+      get

+      {

+        return defaultInstance;

+      }

+    }

+  }

+}

diff --git a/Source/ModelViewer/Properties/Settings.settings b/Source/ModelViewer/Properties/Settings.settings
new file mode 100644
index 00000000..abf36c5d
--- /dev/null
+++ b/Source/ModelViewer/Properties/Settings.settings
@@ -0,0 +1,7 @@
+<?xml version='1.0' encoding='utf-8'?>

+<SettingsFile xmlns="http://schemas.microsoft.com/VisualStudio/2004/01/settings" CurrentProfile="(Default)">

+  <Profiles>

+    <Profile Name="(Default)" />

+  </Profiles>

+  <Settings />

+</SettingsFile>

diff --git a/Source/ModelViewer/SearchBox.Designer.cs b/Source/ModelViewer/SearchBox.Designer.cs
new file mode 100644
index 00000000..0bf884ce
--- /dev/null
+++ b/Source/ModelViewer/SearchBox.Designer.cs
@@ -0,0 +1,81 @@
+namespace ModelViewer

+{

+  partial class SearchBox

+  {

+    /// <summary>

+    /// Required designer variable.

+    /// </summary>

+    private System.ComponentModel.IContainer components = null;

+

+    /// <summary>

+    /// Clean up any resources being used.

+    /// </summary>

+    /// <param name="disposing">true if managed resources should be disposed; otherwise, false.</param>

+    protected override void Dispose(bool disposing)

+    {

+      if (disposing && (components != null)) {

+        components.Dispose();

+      }

+      base.Dispose(disposing);

+    }

+

+    #region Windows Form Designer generated code

+

+    /// <summary>

+    /// Required method for Designer support - do not modify

+    /// the contents of this method with the code editor.

+    /// </summary>

+    private void InitializeComponent()

+    {

+      this.textBox1 = new System.Windows.Forms.TextBox();

+      this.listBox1 = new System.Windows.Forms.ListBox();

+      this.SuspendLayout();

+      // 

+      // textBox1

+      // 

+      this.textBox1.Anchor = ((System.Windows.Forms.AnchorStyles)(((System.Windows.Forms.AnchorStyles.Top | System.Windows.Forms.AnchorStyles.Left)

+                  | System.Windows.Forms.AnchorStyles.Right)));

+      this.textBox1.Location = new System.Drawing.Point(2, 1);

+      this.textBox1.Name = "textBox1";

+      this.textBox1.Size = new System.Drawing.Size(479, 20);

+      this.textBox1.TabIndex = 0;

+      this.textBox1.TextChanged += new System.EventHandler(this.textBox1_TextChanged);

+      this.textBox1.KeyDown += new System.Windows.Forms.KeyEventHandler(this.textBox1_KeyDown);

+      this.textBox1.KeyPress += new System.Windows.Forms.KeyPressEventHandler(this.textBox1_KeyPress);

+      // 

+      // listBox1

+      // 

+      this.listBox1.Anchor = ((System.Windows.Forms.AnchorStyles)((((System.Windows.Forms.AnchorStyles.Top | System.Windows.Forms.AnchorStyles.Bottom)

+                  | System.Windows.Forms.AnchorStyles.Left)

+                  | System.Windows.Forms.AnchorStyles.Right)));

+      this.listBox1.FormattingEnabled = true;

+      this.listBox1.Location = new System.Drawing.Point(2, 27);

+      this.listBox1.Name = "listBox1";

+      this.listBox1.Size = new System.Drawing.Size(479, 498);

+      this.listBox1.TabIndex = 1;

+      this.listBox1.KeyDown += new System.Windows.Forms.KeyEventHandler(this.listBox1_KeyDown);

+      this.listBox1.Click += new System.EventHandler(this.listBox1_Click);

+      // 

+      // SearchBox

+      // 

+      this.AutoScaleDimensions = new System.Drawing.SizeF(6F, 13F);

+      this.AutoScaleMode = System.Windows.Forms.AutoScaleMode.Font;

+      this.ClientSize = new System.Drawing.Size(483, 527);

+      this.Controls.Add(this.listBox1);

+      this.Controls.Add(this.textBox1);

+      this.Name = "SearchBox";

+      this.ShowIcon = false;

+      this.Text = "Search...";

+      this.TopMost = true;

+      this.FormClosing += new System.Windows.Forms.FormClosingEventHandler(this.SearchBox_FormClosing);

+      this.ResumeLayout(false);

+      this.PerformLayout();

+

+    }

+

+    #endregion

+

+    private System.Windows.Forms.TextBox textBox1;

+    private System.Windows.Forms.ListBox listBox1;

+  }

+}
\ No newline at end of file
diff --git a/Source/ModelViewer/SearchBox.cs b/Source/ModelViewer/SearchBox.cs
new file mode 100644
index 00000000..abe428b2
--- /dev/null
+++ b/Source/ModelViewer/SearchBox.cs
@@ -0,0 +1,129 @@
+using System;

+using System.Collections.Generic;

+using System.ComponentModel;

+using System.Data;

+using System.Drawing;

+using System.Linq;

+using System.Text;

+using System.Windows.Forms;

+

+namespace ModelViewer

+{

+  public partial class SearchBox : Form

+  {

+    public SearchBox(Main a)

+    {

+      this.axprof = a;

+      InitializeComponent();

+      this.textBox1.Text = a.SearchText;

+    }

+

+    class NodeText

+    {

+      internal TreeNode n;

+      public NodeText(TreeNode n) { this.n = n; }

+      public override string ToString()

+      {

+        return n.Text;

+      }

+    }

+

+    List<NodeText> nodes = new List<NodeText>();

+    Main axprof;

+

+    private void AddNodes(TreeNodeCollection coll)

+    {

+      foreach (TreeNode n in coll) {

+        nodes.Add(new NodeText(n));

+        if (n.IsExpanded) {

+          AddNodes(n.Nodes);

+        }

+      }

+    }

+

+    public void SetFilter(string s)

+    {

+      axprof.SearchText = this.textBox1.Text;

+      var words0 = s.Split(' ');

+      var words = new List<string>();

+      foreach (var w in words0) if (w != "") words.Add(w.ToLower());

+      var objs = new List<object>();

+      foreach (var n in nodes) {

+        bool wrong = false;

+        string x = n.ToString().ToLower();

+        foreach (var w in words) {

+          if (!x.Contains(w)) { wrong = true; break; }

+        }

+        if (!wrong) objs.Add(n);

+      }

+      listBox1.BeginUpdate();

+      listBox1.Items.Clear();

+      listBox1.Items.AddRange(objs.ToArray());

+      listBox1.EndUpdate();

+    }

+

+    public void Populate(TreeNodeCollection coll)

+    {

+      nodes.Clear();

+      AddNodes(coll);

+      SetFilter(this.textBox1.Text);

+    }

+

+    private void textBox1_TextChanged(object sender, EventArgs e)

+    {

+      SetFilter(textBox1.Text);

+    }

+

+    private void SearchBox_FormClosing(object sender, FormClosingEventArgs e)

+    {

+

+    }

+

+    private void textBox1_KeyPress(object sender, KeyPressEventArgs e)

+    {

+      if (e.KeyChar == (char)13 || e.KeyChar == (char)27)

+        e.Handled = true;

+

+    }

+

+    private void textBox1_KeyDown(object sender, KeyEventArgs e)

+    {

+      if (e.KeyCode == Keys.Down) {

+        listBox1.SelectedIndex = 0;

+        listBox1.Focus();

+        e.Handled = true;

+      } else if (e.KeyCode == Keys.Enter) {

+        Execute(true);

+        e.Handled = true;

+      } else if (e.KeyCode == Keys.Escape) {

+        this.Hide();

+        e.Handled = true;

+      }

+    }

+

+    private void Execute(bool first)

+    {

+      if (listBox1.Items.Count == 0) return;

+

+      NodeText n =

+        (first ? listBox1.Items[0] : listBox1.SelectedItem) as NodeText;

+      if (n != null) {

+        axprof.Activate(n.n);

+        this.Hide();

+      }

+    }

+

+    private void listBox1_Click(object sender, EventArgs e)

+    {

+      Execute(false);

+    }

+

+    private void listBox1_KeyDown(object sender, KeyEventArgs e)

+    {

+      if (e.KeyCode == Keys.Enter) {

+        Execute(false);

+        e.Handled = true;

+      }

+    }

+  }

+}