Trying to merge with recent changes, failing.

8 files changed, 426 insertions, 22 deletions

diff --git a/Source/AbsInt/AbsInt.csproj b/Source/AbsInt/AbsInt.csproj
index 93d304d7..9ccd0ffe 100644
--- a/Source/AbsInt/AbsInt.csproj
+++ b/Source/AbsInt/AbsInt.csproj
@@ -141,6 +141,67 @@
     <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>

     <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>

   </PropertyGroup>

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

+    <DebugSymbols>true</DebugSymbols>

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

+    <DefineConstants>DEBUG;TRACE</DefineConstants>

+    <DebugType>full</DebugType>

+    <PlatformTarget>x86</PlatformTarget>

+    <CodeAnalysisLogFile>bin\Debug\AbsInt.dll.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>

+  </PropertyGroup>

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

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

+    <DefineConstants>TRACE</DefineConstants>

+    <Optimize>true</Optimize>

+    <DebugType>pdbonly</DebugType>

+    <PlatformTarget>x86</PlatformTarget>

+    <CodeAnalysisLogFile>bin\Release\AbsInt.dll.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>

+  </PropertyGroup>

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

+    <DebugSymbols>true</DebugSymbols>

+    <OutputPath>bin\x86\z3apidebug\</OutputPath>

+    <DefineConstants>DEBUG;TRACE</DefineConstants>

+    <DebugType>full</DebugType>

+    <PlatformTarget>x86</PlatformTarget>

+    <CodeAnalysisLogFile>bin\z3apidebug\AbsInt.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>

+    <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>

+    <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>

+    <ErrorReport>prompt</ErrorReport>

+    <CodeAnalysisRuleSet>Migrated rules for AbsInt.ruleset</CodeAnalysisRuleSet>

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

+    <CodeAnalysisIgnoreBuiltInRuleSets>false</CodeAnalysisIgnoreBuiltInRuleSets>

+    <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>

+  </PropertyGroup>

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

+    <DebugSymbols>true</DebugSymbols>

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

+    <DefineConstants>DEBUG;TRACE</DefineConstants>

+    <DebugType>full</DebugType>

+    <PlatformTarget>x86</PlatformTarget>

+    <CodeAnalysisLogFile>bin\Debug\AbsInt.dll.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>

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

+  </PropertyGroup>

   <ItemGroup>

     <Reference Include="System" />

     <Reference Include="System.Core">

diff --git a/Source/Boogie.sln b/Source/Boogie.sln
index 955dfb46..1f9c96a3 100644
--- a/Source/Boogie.sln
+++ b/Source/Boogie.sln
@@ -79,7 +79,8 @@ Global
 		{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

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

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

 		{435D5BD0-6F62-49F8-BB24-33E2257519AD}.Checked|.NET.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

@@ -105,6 +106,7 @@ Global
 		{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

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

 		{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}.Checked|.NET.ActiveCfg = Checked|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

@@ -129,7 +131,9 @@ Global
 		{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

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

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

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

 		{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Checked|.NET.ActiveCfg = Checked|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

@@ -155,6 +159,8 @@ Global
 		{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

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

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

 		{E1F10180-C7B9-4147-B51F-FA1B701966DC}.Checked|.NET.ActiveCfg = Checked|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

@@ -180,6 +186,7 @@ Global
 		{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

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

 		{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}.Checked|.NET.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

@@ -204,6 +211,7 @@ Global
 		{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

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

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

@@ -228,6 +236,7 @@ Global
 		{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

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

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

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

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

@@ -237,6 +246,7 @@ Global
 		{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|Mixed Platforms.Build.0 = 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

@@ -249,6 +259,7 @@ Global
 		{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

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

 		{39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Checked|.NET.ActiveCfg = Checked|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

@@ -273,6 +284,7 @@ Global
 		{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

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

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

@@ -297,6 +309,7 @@ Global
 		{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

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

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

@@ -321,6 +334,7 @@ Global
 		{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

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

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

@@ -345,6 +359,7 @@ Global
 		{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

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

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

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

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

@@ -393,6 +408,7 @@ Global
 		{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU

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

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

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

 		{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Checked|.NET.ActiveCfg = Checked|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

@@ -417,6 +433,8 @@ Global
 		{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU

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

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

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

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

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

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

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

@@ -441,6 +459,7 @@ 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

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

 	EndGlobalSection

 	GlobalSection(SolutionProperties) = preSolution

 		HideSolutionNode = FALSE

diff --git a/Source/BoogieDriver/BoogieDriver.csproj b/Source/BoogieDriver/BoogieDriver.csproj
index 9b6e329b..18f94929 100644
--- a/Source/BoogieDriver/BoogieDriver.csproj
+++ b/Source/BoogieDriver/BoogieDriver.csproj
@@ -40,7 +40,7 @@
     <DebugSymbols>true</DebugSymbols>

     <DebugType>full</DebugType>

     <Optimize>false</Optimize>

-    <OutputPath>..\..\Binaries\</OutputPath>

+    <OutputPath>..\Provers\Z3api\bin\z3apidebug\</OutputPath>

     <DefineConstants>TRACE;DEBUG</DefineConstants>

     <ErrorReport>prompt</ErrorReport>

     <WarningLevel>4</WarningLevel>

@@ -86,10 +86,10 @@
   </PropertyGroup>

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

     <DebugSymbols>true</DebugSymbols>

-    <OutputPath>bin\z3apidebug\</OutputPath>

+    <OutputPath>..\Provers\Z3api\bin\z3apidebug\</OutputPath>

     <DefineConstants>DEBUG;TRACE</DefineConstants>

     <DebugType>full</DebugType>

-    <PlatformTarget>AnyCPU</PlatformTarget>

+    <PlatformTarget>x86</PlatformTarget>

     <CodeAnalysisRuleAssemblies>

     </CodeAnalysisRuleAssemblies>

     <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>

@@ -138,6 +138,68 @@
     <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>

     <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>

   </PropertyGroup>

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

+    <DebugSymbols>true</DebugSymbols>

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

+    <DefineConstants>TRACE;DEBUG</DefineConstants>

+    <DebugType>full</DebugType>

+    <PlatformTarget>x86</PlatformTarget>

+    <CodeAnalysisLogFile>..\..\Binaries\Boogie.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>false</CodeAnalysisIgnoreBuiltInRuleSets>

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

+  </PropertyGroup>

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

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

+    <DefineConstants>TRACE</DefineConstants>

+    <Optimize>true</Optimize>

+    <DebugType>pdbonly</DebugType>

+    <PlatformTarget>x86</PlatformTarget>

+    <CodeAnalysisLogFile>bin\Release\Boogie.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>false</CodeAnalysisIgnoreBuiltInRuleSets>

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

+    <CodeAnalysisIgnoreBuiltInRules>false</CodeAnalysisIgnoreBuiltInRules>

+  </PropertyGroup>

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

+    <DebugSymbols>true</DebugSymbols>

+    <OutputPath>bin\x86\z3apidebug\</OutputPath>

+    <DefineConstants>DEBUG;TRACE</DefineConstants>

+    <DebugType>full</DebugType>

+    <PlatformTarget>x86</PlatformTarget>

+    <CodeAnalysisLogFile>bin\z3apidebug\Boogie.exe.CodeAnalysisLog.xml</CodeAnalysisLogFile>

+    <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>

+    <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>

+    <ErrorReport>prompt</ErrorReport>

+    <CodeAnalysisRuleSet>Migrated rules for BoogieDriver.ruleset</CodeAnalysisRuleSet>

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

+    <CodeAnalysisIgnoreBuiltInRuleSets>false</CodeAnalysisIgnoreBuiltInRuleSets>

+    <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>

+  </PropertyGroup>

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

+    <DebugSymbols>true</DebugSymbols>

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

+    <DefineConstants>DEBUG;TRACE</DefineConstants>

+    <DebugType>full</DebugType>

+    <PlatformTarget>x86</PlatformTarget>

+    <CodeAnalysisLogFile>..\..\Binaries\Boogie.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;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>

+    <CodeAnalysisIgnoreBuiltInRuleSets>false</CodeAnalysisIgnoreBuiltInRuleSets>

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

+    <CodeAnalysisIgnoreBuiltInRules>false</CodeAnalysisIgnoreBuiltInRules>

+  </PropertyGroup>

   <ItemGroup>

     <Reference Include="System" />

     <Reference Include="System.Data" />

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 041d3a6f..c4b5d7a9 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -545,6 +545,8 @@ namespace Microsoft.Boogie {
       // header_last block that was created because of splitting header.

       Dictionary<Block, Block> newBlocksCreated = new Dictionary<Block, Block>();

 

+      bool headRecursion = false; // testing an option to put recursive call before loop body 

+

       IEnumerable<Block> sortedHeaders = g.SortHeadersByDominance();

       foreach (Block/*!*/ header in sortedHeaders)

       {

@@ -565,7 +567,17 @@ namespace Microsoft.Boogie {
               continue;

             Block newBlock = new Block();

             newBlock.Label = block.Label;

-            newBlock.Cmds = codeCopier.CopyCmdSeq(block.Cmds);

+            if (headRecursion && block == header)

+            {

+                CallCmd callCmd = (CallCmd)(loopHeaderToCallCmd2[header]).Clone();

+                addUniqueCallAttr(si_unique_loc, callCmd);

+                si_unique_loc++;

+                newBlock.Cmds.Add(callCmd);  // add the recursive call at head of loop

+                var rest = codeCopier.CopyCmdSeq(block.Cmds);

+                newBlock.Cmds.AddRange(rest);

+            }

+            else

+              newBlock.Cmds = codeCopier.CopyCmdSeq(block.Cmds);

             blockMap[block] = newBlock;

             if (newBlocksCreated.ContainsKey(block))

             {

@@ -616,14 +628,21 @@ namespace Microsoft.Boogie {
             }

           }

 

-          CallCmd callCmd = (CallCmd) (loopHeaderToCallCmd2[header]).Clone();

-          addUniqueCallAttr(si_unique_loc, callCmd);

-          si_unique_loc++;

+          CmdSeq cmdSeq;

+          if (headRecursion)

+              cmdSeq = new CmdSeq();

+          else

+          {

+              CallCmd callCmd = (CallCmd)(loopHeaderToCallCmd2[header]).Clone();

+              addUniqueCallAttr(si_unique_loc, callCmd);

+              si_unique_loc++;

+              cmdSeq = new CmdSeq(callCmd);

+          }

 

           Block/*!*/ block1 = new Block(Token.NoToken, source.Label + "_dummy",

                               new CmdSeq(new AssumeCmd(Token.NoToken, Expr.False)), new ReturnCmd(Token.NoToken));

           Block/*!*/ block2 = new Block(Token.NoToken, block1.Label,

-                              new CmdSeq(callCmd), new ReturnCmd(Token.NoToken));

+                              cmdSeq, new ReturnCmd(Token.NoToken));

           impl.Blocks.Add(block1);

           dummyBlocks.Add(block1.Label);

 

diff --git a/Source/Provers/Z3api/ContextLayer.cs b/Source/Provers/Z3api/ContextLayer.cs
index e0fddc63..df40df3d 100644
--- a/Source/Provers/Z3api/ContextLayer.cs
+++ b/Source/Provers/Z3api/ContextLayer.cs
@@ -20,6 +20,8 @@ namespace Microsoft.Boogie.Z3 {
     internal BacktrackDictionary<string, Term> constants = new BacktrackDictionary<string, Term>();

     internal BacktrackDictionary<string, FuncDecl> functions = new BacktrackDictionary<string, FuncDecl>();

     internal BacktrackDictionary<string, Term> labels = new BacktrackDictionary<string, Term>();

+    internal BacktrackDictionary<Term, VCExpr> constants_inv = null;

+    internal BacktrackDictionary<FuncDecl, Function> functions_inv = null;

 

     public Config config;

     public Context z3;

@@ -56,7 +58,13 @@ namespace Microsoft.Boogie.Z3 {
       z3 = new Context(config);

       z3.SetPrintMode(PrintMode.Smtlib2Compliant);

       if (logFilename != null)

-        z3.OpenLog(logFilename);

+      {

+#if true

+          Z3Log.Open(logFilename);

+#else

+          z3.OpenLog(logFilename);

+#endif

+      }

       foreach (string tag in debugTraces)

         z3.EnableDebugTrace(tag);

 

@@ -65,6 +73,227 @@ namespace Microsoft.Boogie.Z3 {
       this.namer = new UniqueNamer();

     }

 

+    public Z3apiProverContext(Context ctx, VCExpressionGenerator gen)

+        : base(gen, new VCGenerationOptions(new List<string>()))

+    {

+        z3 = ctx;

+

+        this.z3log = null;

+        this.tm = new Z3TypeCachedBuilder(this);

+        this.namer = new UniqueNamer();

+

+        // For external 

+

+        constants_inv = new BacktrackDictionary<Term, VCExpr>();

+        functions_inv = new BacktrackDictionary<FuncDecl, Function>();

+    }

+

+    public Term VCExprToTerm(VCExpr expr, LineariserOptions linOptions) {

+        Z3apiExprLineariser visitor = new Z3apiExprLineariser(this, namer);

+        return (Term)expr.Accept(visitor, linOptions);

+    }

+

+

+    private class fromZ3

+    {

+        private VCExpressionGenerator gen;

+        private Dictionary<Term, VCExpr> memo;

+        private BacktrackDictionary<Term, VCExpr> constants_inv;

+        private BacktrackDictionary<FuncDecl, Function> functions_inv;

+        private List<VCExprLetBinding> lets;

+        private int let_ctr = 0;

+

+        private VCExpr create_let(Term t, VCExpr u)

+        {

+            var name = "$x" + let_ctr.ToString();

+            let_ctr++;

+            var sym = gen.Variable(name, u.Type);

+            memo.Remove(t);

+            memo.Add(t, sym);

+            lets.Add(gen.LetBinding(sym, u));

+            return sym;

+        }

+

+        public fromZ3(VCExpressionGenerator _gen,

+                      BacktrackDictionary<Term, VCExpr> _constants_inv,

+                      BacktrackDictionary<FuncDecl, Function> _functions_inv)

+        {

+            gen = _gen;

+            constants_inv = _constants_inv;

+            functions_inv = _functions_inv;

+            memo = new Dictionary<Term, VCExpr>();

+            lets = new List<VCExprLetBinding>();

+        }

+

+        public void clear()

+        {

+            memo.Clear();

+            lets.Clear();

+        }

+        public VCExpr get(Term arg)

+        {

+            if (memo.ContainsKey(arg))

+                return memo[arg];

+            VCExpr res = null;

+            switch (arg.GetKind())

+            {

+                case TermKind.Numeral:

+                    var numstr = arg.GetNumeralString();

+                    var bignum = Basetypes.BigNum.FromString(numstr);

+                    res = gen.Integer(bignum);

+                    break;

+                case TermKind.App:

+                    var args = arg.GetAppArgs();

+                    var vcargs = new VCExpr[args.Length];

+                    for (int i = 0; i < args.Length; i++)

+                        vcargs[i] = get(args[i]);

+

+                    switch (arg.GetAppDecl().GetKind())

+                    {

+                        case DeclKind.Add:

+                            if (vcargs.Length == 0)

+                                res = gen.Integer(Basetypes.BigNum.FromInt(0));

+                            else

+                            {

+                                res = vcargs[0];

+                                for (int k = 1; k < vcargs.Length; k++)

+                                    res = gen.Add(res, vcargs[k]);

+                            }

+                            break;

+                        case DeclKind.And:

+                            res = VCExpressionGenerator.True;

+                            for (int i = 0; i < vcargs.Length; i++)

+                                res = gen.AndSimp(res, vcargs[i]);

+                            break;

+                        case DeclKind.Div:

+                            Debug.Assert(vcargs.Length == 2);

+                            res = gen.Function(VCExpressionGenerator.DivOp, vcargs[0], vcargs[1]);

+                            break;

+                        case DeclKind.Eq:

+                            Debug.Assert(vcargs.Length == 2);

+                            res = gen.Eq(vcargs[0], vcargs[1]);

+                            break;

+                        case DeclKind.False:

+                            res = VCExpressionGenerator.False;

+                            break;

+                        case DeclKind.Ge:

+                            Debug.Assert(vcargs.Length == 2);

+                            res = gen.Function(VCExpressionGenerator.GeOp, vcargs[0], vcargs[1]);

+                            break;

+                        case DeclKind.Gt:

+                            Debug.Assert(vcargs.Length == 2);

+                            res = gen.Gt(vcargs[0], vcargs[1]);

+                            break;

+                        case DeclKind.IDiv:

+                            Debug.Assert(vcargs.Length == 2);

+                            res = gen.Function(VCExpressionGenerator.DivOp, vcargs[0], vcargs[1]);

+                            break;

+                        case DeclKind.Iff:

+                            Debug.Assert(vcargs.Length == 2);

+                            var l = create_let(args[0], vcargs[0]);

+                            var r = create_let(args[1], vcargs[1]);

+                            return gen.And(gen.Implies(l, r), gen.Implies(r, l));

+                        case DeclKind.Implies:

+                            Debug.Assert(vcargs.Length == 2);

+                            res = gen.Implies(vcargs[0], vcargs[1]);

+                            break;

+                        case DeclKind.Ite:

+                            Debug.Assert(vcargs.Length == 3);

+                            res = gen.Function(VCExpressionGenerator.IfThenElseOp, vcargs[0], vcargs[1], vcargs[2]);

+                            break;

+                        case DeclKind.Le:

+                            Debug.Assert(vcargs.Length == 2);

+                            res = gen.Function(VCExpressionGenerator.LeOp, vcargs[0], vcargs[1]);

+                            break;

+                        case DeclKind.Lt:

+                            Debug.Assert(vcargs.Length == 2);

+                            res = gen.Function(VCExpressionGenerator.LtOp, vcargs[0], vcargs[1]);

+                            break;

+                        case DeclKind.Mod:

+                            Debug.Assert(vcargs.Length == 2);

+                            res = gen.Function(VCExpressionGenerator.ModOp, vcargs[0], vcargs[1]);

+                            break;

+                        case DeclKind.Mul:

+                            Debug.Assert(vcargs.Length == 2);

+                            res = gen.Function(VCExpressionGenerator.MulOp, vcargs[0], vcargs[1]);

+                            break;

+                        case DeclKind.Not:

+                            Debug.Assert(vcargs.Length == 1);

+                            res = gen.Not(vcargs[0]);

+                            break;

+                        case DeclKind.Or:

+                            res = VCExpressionGenerator.False;

+                            for (int i = 0; i < vcargs.Length; i++)

+                                res = gen.OrSimp(res, vcargs[i]);

+                            break;

+                        case DeclKind.Select:

+                            Debug.Assert(vcargs.Length == 2);

+                            res = gen.Select(vcargs[0], vcargs[1]);

+                            break;

+                        case DeclKind.Store:

+                            Debug.Assert(vcargs.Length == 3);

+                            res = gen.Store(vcargs[0], vcargs[1], vcargs[2]);

+                            break;

+                        case DeclKind.Sub:

+                            Debug.Assert(vcargs.Length == 2);

+                            res = gen.Function(VCExpressionGenerator.SubOp, vcargs[0], vcargs[1]);

+                            break;

+                        case DeclKind.True:

+                            res = VCExpressionGenerator.True;

+                            break;

+                        case DeclKind.Uminus:

+                            Debug.Assert(vcargs.Length == 1);

+                            var bigzero = Basetypes.BigNum.FromInt(0);

+                            res = gen.Function(VCExpressionGenerator.SubOp, gen.Integer(bigzero), vcargs[0]);

+                            break;

+                        case DeclKind.Uninterpreted:

+                            var name = arg.GetAppDecl().GetDeclName();

+                            if (args.Length == 0)

+                            { // a 0-ary constant is a VCExprVar

+                                if (!constants_inv.TryGetValue(arg, out res))

+                                    throw new Exception("Z3 returned unknown constant: " + name);

+                            }

+                            else

+                            {

+                                Function f;

+                                if (!functions_inv.TryGetValue(arg.GetAppDecl(), out f))

+                                    throw new Exception("Z3 returned unknown function: " + name);

+                                List<VCExpr> vcargsList = new List<VCExpr>(vcargs);

+                                res = gen.Function(f, vcargsList);

+                            }   

+                            break;

+                        default:

+                            throw new Exception("Unknown Z3 operator");

+                    }

+                    break;

+                default:

+                    Debug.Assert(false);

+                    throw new Exception("Unknown Z3 AST kind");

+            }

+

+            memo.Add(arg, res);

+            return res;

+        }

+        public VCExpr add_lets(VCExpr e)

+        {

+            foreach (var let in lets)

+            {

+                e = gen.Let(e, let);

+            }

+            return e;

+        }

+    }

+

+    public VCExpr TermToVCExpr(Term t)

+    {

+      var fZ = new fromZ3(gen, constants_inv, functions_inv);

+      return fZ.add_lets(fZ.get(t));

+    }

+

+

+    

+

+

     public override void DeclareType(TypeCtorDecl t, string attributes) {

       base.DeclareType(t, attributes);

       log("(declare-sort {0})", t.Name);

@@ -97,6 +326,7 @@ namespace Microsoft.Boogie.Z3 {
       Sort rangeAst = tm.GetType(range);

       FuncDecl constDeclAst = z3.MkFuncDecl(symbolAst, domainAst.ToArray(), rangeAst);

       functions.Add(functionName, constDeclAst);

+      if(functions_inv != null)functions_inv.Add(constDeclAst, f);

       log("(declare-funs (({0} {1} {2})))", functionName, domainStr, rangeAst);

     }

 

@@ -122,7 +352,11 @@ namespace Microsoft.Boogie.Z3 {
     }

 

     public void CloseLog() {

-      z3.CloseLog();

+#if true

+        Z3Log.Close();

+#else

+        z3.CloseLog();

+#endif

       if (z3log != null) {

         z3log.Close();

       }

@@ -134,6 +368,8 @@ namespace Microsoft.Boogie.Z3 {
       constants.CreateBacktrackPoint();

       functions.CreateBacktrackPoint();

       labels.CreateBacktrackPoint();

+      if(constants_inv != null)constants_inv.CreateBacktrackPoint();

+      if(functions_inv != null)functions_inv.CreateBacktrackPoint();

       z3.Push();

       log("(push)");

     }

@@ -144,6 +380,8 @@ namespace Microsoft.Boogie.Z3 {
       functions.Backtrack();

       constants.Backtrack();

       symbols.Backtrack();

+      if (constants_inv != null) constants_inv.Backtrack();

+      if (functions_inv != null) functions_inv.Backtrack();

       log("(pop)");

     }

 

@@ -368,13 +606,18 @@ namespace Microsoft.Boogie.Z3 {
       return result;

     }

 

-    public Term GetConstant(string constantName, Type constantType) {

+    public Term GetConstant(string constantName, Type constantType, VCExpr node)

+    {

       Term typeSafeTerm;

       if (!constants.ContainsKey(constantName))

         this.DeclareConstant(constantName, constantType);

 

       if (!constants.TryGetValue(constantName, out typeSafeTerm))

         throw new Exception("constant " + constantName + " is not defined");

+

+      if (constants_inv != null && !constants_inv.ContainsKey(typeSafeTerm))

+          constants_inv.Add(typeSafeTerm, node);

+

       return typeSafeTerm;

     }

 

diff --git a/Source/Provers/Z3api/VCExprVisitor.cs b/Source/Provers/Z3api/VCExprVisitor.cs
index 149a23f1..0605a854 100644
--- a/Source/Provers/Z3api/VCExprVisitor.cs
+++ b/Source/Provers/Z3api/VCExprVisitor.cs
@@ -188,7 +188,7 @@ namespace Microsoft.Boogie.Z3
             else

             {

                 string varName = namer.GetName(node, node.Name);

-                return cm.GetConstant(varName, node.Type);

+                return cm.GetConstant(varName, node.Type,node);

             }

         }

 

@@ -252,7 +252,7 @@ namespace Microsoft.Boogie.Z3
         private Term MakeQuantifier(bool isForall, uint weight, string qid, int skolemid, List<string> varNames, List<Type> boogieTypes, List<Pattern> patterns, List<Term> no_patterns, Term body) {

           List<Term> bound = new List<Term>();

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

-            Term t = cm.GetConstant(varNames[i], boogieTypes[i]);

+            Term t = cm.GetConstant(varNames[i], boogieTypes[i], null);

             bound.Add(t);

           }

 

diff --git a/Source/Provers/Z3api/Z3api.csproj b/Source/Provers/Z3api/Z3api.csproj
index 7c481438..f9511dbd 100644
--- a/Source/Provers/Z3api/Z3api.csproj
+++ b/Source/Provers/Z3api/Z3api.csproj
@@ -118,9 +118,8 @@
   </Target>

   -->

   <ItemGroup>

-    <Reference Include="Microsoft.Z3, Version=2.0.40827.2, Culture=neutral, PublicKeyToken=9c8d792caae602a2, processorArchitecture=x86">

-      <SpecificVersion>False</SpecificVersion>

-      <HintPath>..\..\..\Binaries\Microsoft.Z3.dll</HintPath>

+    <Reference Include="ManagedAPI">

+      <HintPath>..\..\..\..\..\iZ3\win\iZ3\Debug\ManagedAPI.dll</HintPath>

     </Reference>

     <Reference Include="System" />

     <Reference Include="System.Core">

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index ef3a88cc..e3b1cb2d 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -100,8 +100,9 @@ namespace Microsoft.Boogie {
 

     /// <summary>

     /// Constructor.  Initialize a checker with the program and log file.

+    /// Optionally, use prover context provided by parameter "ctx". 

     /// </summary>

-    public Checker(VC.ConditionGeneration vcgen, Program prog, string/*?*/ logFilePath, bool appendLogFile, int timeout) {

+    public Checker(VC.ConditionGeneration vcgen, Program prog, string/*?*/ logFilePath, bool appendLogFile, int timeout, ProverContext ctx = null) {

       Contract.Requires(vcgen != null);

       Contract.Requires(prog != null);

       this.timeout = timeout;

@@ -121,7 +122,6 @@ namespace Microsoft.Boogie {
       options.Parse(CommandLineOptions.Clo.ProverOptions);

 

       ContextCacheKey key = new ContextCacheKey(prog);

-      ProverContext ctx;

       ProverInterface prover;

 

       if (vcgen.CheckerCommonState == null) {

@@ -129,12 +129,13 @@ namespace Microsoft.Boogie {
       }

       IDictionary<ContextCacheKey, ProverContext>/*!>!*/ cachedContexts = (IDictionary<ContextCacheKey, ProverContext/*!*/>)vcgen.CheckerCommonState;

 

-      if (cachedContexts.TryGetValue(key, out ctx)) {

+      if (ctx == null && cachedContexts.TryGetValue(key, out ctx))

+      {

         ctx = (ProverContext)cce.NonNull(ctx).Clone();

         prover = (ProverInterface)

           CommandLineOptions.Clo.TheProverFactory.SpawnProver(options, ctx);

       } else {

-        ctx = (ProverContext)CommandLineOptions.Clo.TheProverFactory.NewProverContext(options);

+        if (ctx == null) ctx = (ProverContext)CommandLineOptions.Clo.TheProverFactory.NewProverContext(options);

 

         // set up the context

         foreach (Declaration decl in prog.TopLevelDeclarations) {