Some changes to support expanded use of z3api.

Should not affect function
of other provers. There is an option added in Check.cs to  allow creation
of a Checker with a user-specified ProverContext. Also, some extension of
z3api prover context to support conversion of Z3 formulas back to VCExpr.
Finally, some experimental code, not enabled, to allow conversion of loops to
recursion with "head recursion" rather than "tail recursion" (i.e., recursive
call before loop body rather than after).

9 files changed, 427 insertions, 23 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 53130382..6599ecc2 100644
--- a/Source/Boogie.sln
+++ b/Source/Boogie.sln
@@ -85,7 +85,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

@@ -111,6 +112,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

@@ -135,7 +137,8 @@ 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}.Checked|.NET.ActiveCfg = Checked|Any CPU

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

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

@@ -161,6 +164,7 @@ Global
 		{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

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

@@ -186,6 +190,7 @@ 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}.Checked|.NET.ActiveCfg = Checked|Any CPU

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

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

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

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

@@ -236,6 +242,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

@@ -260,6 +267,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

@@ -284,6 +292,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

@@ -293,6 +302,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

@@ -305,6 +315,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

@@ -329,6 +340,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

@@ -353,6 +365,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

@@ -377,6 +390,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

@@ -401,6 +415,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

@@ -449,6 +464,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

@@ -473,6 +489,7 @@ 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}.Checked|.NET.ActiveCfg = Checked|Any CPU

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

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

@@ -497,6 +514,7 @@ Global
 		{A598ED5A-93AD-4125-A555-3921A2F936FA}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU

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

 		{A598ED5A-93AD-4125-A555-3921A2F936FA}.z3apidebug|x86.ActiveCfg = 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

@@ -521,6 +539,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 52714dc9..de5fecd8 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 76eaf661..10077cc4 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -547,6 +547,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)

       {

@@ -567,7 +569,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))

             {

@@ -578,14 +590,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 f0aa3906..2eb01e24 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 94184957..0923cb36 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 9b7b6e36..bb225071 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) {

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index d13811e0..db7f2dca 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -2454,7 +2454,7 @@ namespace VC
                 {

                     GenerateVCForStratifiedInlining(program, info, checker);

                 }

-                //Console.WriteLine("Inlining {0}", procName);

+                Console.WriteLine("Inlining {0}", procName);

                 VCExpr expansion = cce.NonNull(info.vcexpr);

 

                 // Instantiate the "forall" variables