Merge

28 files changed, 1025 insertions, 400 deletions

diff --git a/Source/AbsInt/AbsInt.csproj b/Source/AbsInt/AbsInt.csproj
index 7e421eb1..2c5f836d 100644
--- a/Source/AbsInt/AbsInt.csproj
+++ b/Source/AbsInt/AbsInt.csproj
@@ -97,6 +97,8 @@
     <ErrorReport>prompt</ErrorReport>

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

     <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>

+    <WarningLevel>4</WarningLevel>

+    <Optimize>false</Optimize>

   </PropertyGroup>

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

     <DebugSymbols>true</DebugSymbols>

@@ -140,6 +142,8 @@
     <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>

     <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>

     <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>

+    <WarningLevel>4</WarningLevel>

+    <Optimize>false</Optimize>

   </PropertyGroup>

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

     <DebugSymbols>true</DebugSymbols>

@@ -156,6 +160,8 @@
     <CodeAnalysisIgnoreBuiltInRuleSets>true</CodeAnalysisIgnoreBuiltInRuleSets>

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

     <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>

+    <WarningLevel>4</WarningLevel>

+    <Optimize>false</Optimize>

   </PropertyGroup>

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

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

@@ -172,6 +178,7 @@
     <CodeAnalysisIgnoreBuiltInRuleSets>true</CodeAnalysisIgnoreBuiltInRuleSets>

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

     <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>

+    <WarningLevel>4</WarningLevel>

   </PropertyGroup>

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

     <DebugSymbols>true</DebugSymbols>

@@ -187,6 +194,8 @@
     <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>

     <CodeAnalysisIgnoreBuiltInRuleSets>false</CodeAnalysisIgnoreBuiltInRuleSets>

     <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>

+    <WarningLevel>4</WarningLevel>

+    <Optimize>false</Optimize>

   </PropertyGroup>

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

     <DebugSymbols>true</DebugSymbols>

@@ -201,6 +210,8 @@
     <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>

+    <WarningLevel>4</WarningLevel>

+    <Optimize>false</Optimize>

   </PropertyGroup>

   <ItemGroup>

     <Reference Include="System" />

diff --git a/Source/BVD/BVD.csproj b/Source/BVD/BVD.csproj
index 0b32dd22..448adff7 100644
--- a/Source/BVD/BVD.csproj
+++ b/Source/BVD/BVD.csproj
@@ -9,7 +9,6 @@
     <AppDesignerFolder>Properties</AppDesignerFolder>

     <RootNamespace>Microsoft.Boogie.ModelViewer</RootNamespace>

     <AssemblyName>BVD</AssemblyName>

-    <TargetFrameworkVersion>v4.5</TargetFrameworkVersion>

     <FileAlignment>512</FileAlignment>

     <PublishUrl>publish\</PublishUrl>

     <Install>true</Install>

@@ -26,6 +25,8 @@
     <IsWebBootstrapper>false</IsWebBootstrapper>

     <UseApplicationTrust>false</UseApplicationTrust>

     <BootstrapperEnabled>true</BootstrapperEnabled>

+    <ProductVersion>12.0.0</ProductVersion>

+    <SchemaVersion>2.0</SchemaVersion>

   </PropertyGroup>

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

     <PlatformTarget>AnyCPU</PlatformTarget>

@@ -46,9 +47,6 @@
     <ErrorReport>prompt</ErrorReport>

     <WarningLevel>4</WarningLevel>

   </PropertyGroup>

-  <PropertyGroup>

-    <StartupObject />

-  </PropertyGroup>

   <ItemGroup>

     <Reference Include="System" />

     <Reference Include="System.Core" />

@@ -67,7 +65,7 @@
   </ItemGroup>

   <ItemGroup>

     <ProjectReference Include="..\ModelViewer\ModelViewer.csproj">

-      <Project>{a678c6eb-b329-46a9-bbfc-7585f01acd7c}</Project>

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

       <Name>ModelViewer</Name>

     </ProjectReference>

   </ItemGroup>

diff --git a/Source/Basetypes/Basetypes.csproj b/Source/Basetypes/Basetypes.csproj
index a7b7cb71..520300fd 100644
--- a/Source/Basetypes/Basetypes.csproj
+++ b/Source/Basetypes/Basetypes.csproj
@@ -97,6 +97,8 @@
     <ErrorReport>prompt</ErrorReport>

     <CodeAnalysisRuleSet>Migrated rules for Basetypes.ruleset</CodeAnalysisRuleSet>

     <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>

+    <WarningLevel>4</WarningLevel>

+    <Optimize>false</Optimize>

   </PropertyGroup>

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

     <DebugSymbols>true</DebugSymbols>

@@ -137,6 +139,8 @@
     <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>

     <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>

     <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>

+    <WarningLevel>4</WarningLevel>

+    <Optimize>false</Optimize>

   </PropertyGroup>

   <ItemGroup>

     <Reference Include="System" />

diff --git a/Source/BoogieDriver/BoogieDriver.csproj b/Source/BoogieDriver/BoogieDriver.csproj
index f407c0dd..d0cc2fe6 100644
--- a/Source/BoogieDriver/BoogieDriver.csproj
+++ b/Source/BoogieDriver/BoogieDriver.csproj
@@ -97,6 +97,8 @@
     <ErrorReport>prompt</ErrorReport>

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

     <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>

+    <WarningLevel>4</WarningLevel>

+    <Optimize>false</Optimize>

   </PropertyGroup>

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

     <DebugSymbols>true</DebugSymbols>

@@ -137,6 +139,8 @@
     <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>

     <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>

     <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>

+    <WarningLevel>4</WarningLevel>

+    <Optimize>false</Optimize>

   </PropertyGroup>

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

     <DebugSymbols>true</DebugSymbols>

@@ -152,6 +156,8 @@
     <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>

+    <WarningLevel>4</WarningLevel>

+    <Optimize>false</Optimize>

   </PropertyGroup>

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

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

@@ -168,6 +174,7 @@
     <CodeAnalysisIgnoreBuiltInRuleSets>false</CodeAnalysisIgnoreBuiltInRuleSets>

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

     <CodeAnalysisIgnoreBuiltInRules>false</CodeAnalysisIgnoreBuiltInRules>

+    <WarningLevel>4</WarningLevel>

   </PropertyGroup>

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

     <DebugSymbols>true</DebugSymbols>

@@ -183,6 +190,8 @@
     <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>

     <CodeAnalysisIgnoreBuiltInRuleSets>false</CodeAnalysisIgnoreBuiltInRuleSets>

     <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>

+    <WarningLevel>4</WarningLevel>

+    <Optimize>false</Optimize>

   </PropertyGroup>

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

     <DebugSymbols>true</DebugSymbols>

@@ -199,6 +208,8 @@
     <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>

+    <WarningLevel>4</WarningLevel>

+    <Optimize>false</Optimize>

   </PropertyGroup>

   <ItemGroup>

     <Reference Include="System" />

@@ -211,7 +222,7 @@
   </ItemGroup>

   <ItemGroup>

     <ProjectReference Include="..\AbsInt\AbsInt.csproj">

-      <Project>{0efa3e43-690b-48dc-a72c-384a3ea7f31f}</Project>

+      <Project>{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}</Project>

       <Name>AbsInt</Name>

     </ProjectReference>

     <ProjectReference Include="..\Basetypes\Basetypes.csproj">

@@ -227,39 +238,39 @@
       <Name>Core</Name>

     </ProjectReference>

     <ProjectReference Include="..\Doomed\Doomed.csproj">

-      <Project>{884386a3-58e9-40bb-a273-b24976775553}</Project>

+      <Project>{884386A3-58E9-40BB-A273-B24976775553}</Project>

       <Name>Doomed</Name>

     </ProjectReference>

     <ProjectReference Include="..\ExecutionEngine\ExecutionEngine.csproj">

-      <Project>{eaa5eb79-d475-4601-a59b-825c191cd25f}</Project>

+      <Project>{EAA5EB79-D475-4601-A59B-825C191CD25F}</Project>

       <Name>ExecutionEngine</Name>

     </ProjectReference>

     <ProjectReference Include="..\Graph\Graph.csproj">

-      <Project>{69a2b0b8-bcac-4101-ae7a-556fcc58c06e}</Project>

+      <Project>{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}</Project>

       <Name>Graph</Name>

     </ProjectReference>

     <ProjectReference Include="..\Houdini\Houdini.csproj">

-      <Project>{cf41e903-78eb-43ba-a355-e5feb5ececd4}</Project>

+      <Project>{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}</Project>

       <Name>Houdini</Name>

     </ProjectReference>

     <ProjectReference Include="..\ParserHelper\ParserHelper.csproj">

-      <Project>{fcd3ac7f-9dfd-46c8-ab1e-09f0b0f16dc5}</Project>

+      <Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project>

       <Name>ParserHelper</Name>

     </ProjectReference>

     <ProjectReference Include="..\Predication\Predication.csproj">

-      <Project>{afaa5ce1-c41b-44f0-88f8-fd8a43826d44}</Project>

+      <Project>{AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}</Project>

       <Name>Predication</Name>

     </ProjectReference>

     <ProjectReference Include="..\Provers\SMTLib\SMTLib.csproj">

-      <Project>{9b163aa3-36bc-4afb-88ab-79bc9e97e401}</Project>

+      <Project>{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}</Project>

       <Name>SMTLib</Name>

     </ProjectReference>

     <ProjectReference Include="..\VCExpr\VCExpr.csproj">

-      <Project>{56ffdbca-7d14-43b8-a6ca-22a20e417ee1}</Project>

+      <Project>{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}</Project>

       <Name>VCExpr</Name>

     </ProjectReference>

     <ProjectReference Include="..\VCGeneration\VCGeneration.csproj">

-      <Project>{e1f10180-c7b9-4147-b51f-fa1b701966dc}</Project>

+      <Project>{E1F10180-C7B9-4147-B51F-FA1B701966DC}</Project>

       <Name>VCGeneration</Name>

     </ProjectReference>

   </ItemGroup>

diff --git a/Source/CodeContractsExtender/CodeContractsExtender.csproj b/Source/CodeContractsExtender/CodeContractsExtender.csproj
index 9473cf40..f307e35e 100644
--- a/Source/CodeContractsExtender/CodeContractsExtender.csproj
+++ b/Source/CodeContractsExtender/CodeContractsExtender.csproj
@@ -97,6 +97,8 @@
     <ErrorReport>prompt</ErrorReport>

     <CodeAnalysisRuleSet>Migrated rules for CodeContractsExtender.ruleset</CodeAnalysisRuleSet>

     <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>

+    <WarningLevel>4</WarningLevel>

+    <Optimize>false</Optimize>

   </PropertyGroup>

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

     <DebugSymbols>true</DebugSymbols>

@@ -137,6 +139,8 @@
     <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>

     <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>

     <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>

+    <WarningLevel>4</WarningLevel>

+    <Optimize>false</Optimize>

   </PropertyGroup>

   <ItemGroup>

     <Reference Include="System" />

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index d09678dc..46d030d2 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -412,6 +412,7 @@ namespace Microsoft.Boogie {
     public bool SimplifyLogFileAppend = false;

     public bool SoundnessSmokeTest = false;

     public string Z3ExecutablePath = null;

+	public string CVC4ExecutablePath = null;

 

     public enum ProverWarnings {

       None,

@@ -467,6 +468,7 @@ namespace Microsoft.Boogie {
     public string PrintCFGPrefix = null;

     public bool ForceBplErrors = false; // if true, boogie error is shown even if "msg" attribute is present

     public bool UseArrayTheory = false;

+	public bool UseSmtOutputFormat = false;

     public bool WeakArrayTheory = false;

     public bool UseLabels = true;

     public bool MonomorphicArrays {

@@ -1241,7 +1243,14 @@ namespace Microsoft.Boogie {
         case "errorLimit":

           ps.GetNumericArgument(ref ProverCCLimit);

           return true;

-

+		

+		case "useSmtOutputFormat": {

+		  if (ps.ConfirmArgumentCount(0)) {

+			UseSmtOutputFormat = true;

+		  }

+	      return true;

+		}

+		

         case "z3opt":

           if (ps.ConfirmArgumentCount(1)) {

             Z3Options.Add(cce.NonNull(args[ps.i]));

@@ -1279,6 +1288,12 @@ namespace Microsoft.Boogie {
           }

           return true;

 

+		case "cvc4exe":

+			if (ps.ConfirmArgumentCount(1)) {

+				CVC4ExecutablePath = args[ps.i];

+			}

+			return true;

+

         case "doBitVectorAnalysis":

           DoBitVectorAnalysis = true;

           if (ps.ConfirmArgumentCount(1)) {

@@ -1848,12 +1863,17 @@ namespace Microsoft.Boogie {
   /useArrayTheory

                 use Z3's native theory (as opposed to axioms).  Currently

                 implies /monomorphize.

-

+  /useSmtOutputFormat

+                Z3 outputs a model in the SMTLIB2 format.

   /z3types      generate multi-sorted VC that make use of Z3 types

   /z3lets:<n>   0 - no LETs, 1 - only LET TERM, 2 - only LET FORMULA,

                 3 - (default) any

   /z3exe:<path>

                 path to Z3 executable

+

+  CVC4 specific options:

+  /cvc4exe:<path>

+                path to CVC4 executable

 ");

     }

   }

diff --git a/Source/Core/Core.csproj b/Source/Core/Core.csproj
index d41fb40b..f3db4f9a 100644
--- a/Source/Core/Core.csproj
+++ b/Source/Core/Core.csproj
@@ -97,6 +97,8 @@
     <ErrorReport>prompt</ErrorReport>

     <CodeAnalysisRuleSet>Migrated rules for Core.ruleset</CodeAnalysisRuleSet>

     <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>

+    <WarningLevel>4</WarningLevel>

+    <Optimize>false</Optimize>

   </PropertyGroup>

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

     <DebugSymbols>true</DebugSymbols>

@@ -139,6 +141,8 @@
     <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>

     <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>

     <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>

+    <WarningLevel>4</WarningLevel>

+    <Optimize>false</Optimize>

   </PropertyGroup>

   <ItemGroup>

     <Reference Include="System" />

diff --git a/Source/Doomed/Doomed.csproj b/Source/Doomed/Doomed.csproj
index c3319022..a2390a39 100644
--- a/Source/Doomed/Doomed.csproj
+++ b/Source/Doomed/Doomed.csproj
@@ -12,6 +12,8 @@
     <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>

     <FileAlignment>512</FileAlignment>

     <TargetFrameworkProfile>Client</TargetFrameworkProfile>

+    <ProductVersion>12.0.0</ProductVersion>

+    <SchemaVersion>2.0</SchemaVersion>

   </PropertyGroup>

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

     <DebugSymbols>true</DebugSymbols>

@@ -55,35 +57,35 @@
   </ItemGroup>

   <ItemGroup>

     <ProjectReference Include="..\Basetypes\Basetypes.csproj">

-      <Project>{43dfad18-3e35-4558-9be2-caff6b5ba8a0}</Project>

+      <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>

       <Name>Basetypes</Name>

     </ProjectReference>

     <ProjectReference Include="..\CodeContractsExtender\CodeContractsExtender.csproj">

-      <Project>{accc0156-0921-43ed-8f67-ad8bdc8cde31}</Project>

+      <Project>{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}</Project>

       <Name>CodeContractsExtender</Name>

     </ProjectReference>

     <ProjectReference Include="..\Core\Core.csproj">

-      <Project>{b230a69c-c466-4065-b9c1-84d80e76d802}</Project>

+      <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>

       <Name>Core</Name>

     </ProjectReference>

     <ProjectReference Include="..\Graph\Graph.csproj">

-      <Project>{69a2b0b8-bcac-4101-ae7a-556fcc58c06e}</Project>

+      <Project>{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}</Project>

       <Name>Graph</Name>

     </ProjectReference>

     <ProjectReference Include="..\Model\Model.csproj">

-      <Project>{acef88d5-dadd-46da-bae1-2144d63f4c83}</Project>

+      <Project>{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}</Project>

       <Name>Model</Name>

     </ProjectReference>

     <ProjectReference Include="..\ParserHelper\ParserHelper.csproj">

-      <Project>{fcd3ac7f-9dfd-46c8-ab1e-09f0b0f16dc5}</Project>

+      <Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project>

       <Name>ParserHelper</Name>

     </ProjectReference>

     <ProjectReference Include="..\VCExpr\VCExpr.csproj">

-      <Project>{56ffdbca-7d14-43b8-a6ca-22a20e417ee1}</Project>

+      <Project>{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}</Project>

       <Name>VCExpr</Name>

     </ProjectReference>

     <ProjectReference Include="..\VCGeneration\VCGeneration.csproj">

-      <Project>{e1f10180-c7b9-4147-b51f-fa1b701966dc}</Project>

+      <Project>{E1F10180-C7B9-4147-B51F-FA1B701966DC}</Project>

       <Name>VCGeneration</Name>

     </ProjectReference>

   </ItemGroup>

diff --git a/Source/ExecutionEngine/ExecutionEngine.csproj b/Source/ExecutionEngine/ExecutionEngine.csproj
index 91f13ed4..bebe686d 100644
--- a/Source/ExecutionEngine/ExecutionEngine.csproj
+++ b/Source/ExecutionEngine/ExecutionEngine.csproj
@@ -14,6 +14,8 @@
     <TargetFrameworkProfile>Client</TargetFrameworkProfile>

     <SignAssembly>true</SignAssembly>

     <AssemblyOriginatorKeyFile>..\InterimKey.snk</AssemblyOriginatorKeyFile>

+    <ProductVersion>12.0.0</ProductVersion>

+    <SchemaVersion>2.0</SchemaVersion>

   </PropertyGroup>

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

     <DebugSymbols>true</DebugSymbols>

@@ -44,47 +46,47 @@
   </ItemGroup>

   <ItemGroup>

     <ProjectReference Include="..\AbsInt\AbsInt.csproj">

-      <Project>{0efa3e43-690b-48dc-a72c-384a3ea7f31f}</Project>

+      <Project>{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}</Project>

       <Name>AbsInt</Name>

     </ProjectReference>

     <ProjectReference Include="..\Basetypes\Basetypes.csproj">

-      <Project>{43dfad18-3e35-4558-9be2-caff6b5ba8a0}</Project>

+      <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>

       <Name>Basetypes</Name>

     </ProjectReference>

     <ProjectReference Include="..\CodeContractsExtender\CodeContractsExtender.csproj">

-      <Project>{accc0156-0921-43ed-8f67-ad8bdc8cde31}</Project>

+      <Project>{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}</Project>

       <Name>CodeContractsExtender</Name>

     </ProjectReference>

     <ProjectReference Include="..\Core\Core.csproj">

-      <Project>{b230a69c-c466-4065-b9c1-84d80e76d802}</Project>

+      <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>

       <Name>Core</Name>

     </ProjectReference>

     <ProjectReference Include="..\Doomed\Doomed.csproj">

-      <Project>{884386a3-58e9-40bb-a273-b24976775553}</Project>

+      <Project>{884386A3-58E9-40BB-A273-B24976775553}</Project>

       <Name>Doomed</Name>

     </ProjectReference>

     <ProjectReference Include="..\Graph\Graph.csproj">

-      <Project>{69a2b0b8-bcac-4101-ae7a-556fcc58c06e}</Project>

+      <Project>{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}</Project>

       <Name>Graph</Name>

     </ProjectReference>

     <ProjectReference Include="..\Houdini\Houdini.csproj">

-      <Project>{cf41e903-78eb-43ba-a355-e5feb5ececd4}</Project>

+      <Project>{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}</Project>

       <Name>Houdini</Name>

     </ProjectReference>

     <ProjectReference Include="..\Model\Model.csproj">

-      <Project>{acef88d5-dadd-46da-bae1-2144d63f4c83}</Project>

+      <Project>{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}</Project>

       <Name>Model</Name>

     </ProjectReference>

     <ProjectReference Include="..\ParserHelper\ParserHelper.csproj">

-      <Project>{fcd3ac7f-9dfd-46c8-ab1e-09f0b0f16dc5}</Project>

+      <Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project>

       <Name>ParserHelper</Name>

     </ProjectReference>

     <ProjectReference Include="..\Predication\Predication.csproj">

-      <Project>{afaa5ce1-c41b-44f0-88f8-fd8a43826d44}</Project>

+      <Project>{AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}</Project>

       <Name>Predication</Name>

     </ProjectReference>

     <ProjectReference Include="..\VCGeneration\VCGeneration.csproj">

-      <Project>{e1f10180-c7b9-4147-b51f-fa1b701966dc}</Project>

+      <Project>{E1F10180-C7B9-4147-B51F-FA1B701966DC}</Project>

       <Name>VCGeneration</Name>

     </ProjectReference>

   </ItemGroup>

diff --git a/Source/Graph/Graph.csproj b/Source/Graph/Graph.csproj
index 718ced5d..9ed20759 100644
--- a/Source/Graph/Graph.csproj
+++ b/Source/Graph/Graph.csproj
@@ -97,6 +97,8 @@
     <ErrorReport>prompt</ErrorReport>

     <CodeAnalysisRuleSet>Migrated rules for Graph.ruleset</CodeAnalysisRuleSet>

     <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>

+    <WarningLevel>4</WarningLevel>

+    <Optimize>false</Optimize>

   </PropertyGroup>

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

     <DebugSymbols>true</DebugSymbols>

@@ -137,6 +139,8 @@
     <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>

     <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>

     <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>

+    <WarningLevel>4</WarningLevel>

+    <Optimize>false</Optimize>

   </PropertyGroup>

   <ItemGroup>

     <Reference Include="System" />

diff --git a/Source/Houdini/Houdini.csproj b/Source/Houdini/Houdini.csproj
index 75518155..6c98c2a8 100644
--- a/Source/Houdini/Houdini.csproj
+++ b/Source/Houdini/Houdini.csproj
@@ -64,6 +64,8 @@
     <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>

     <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>

     <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>

+    <WarningLevel>4</WarningLevel>

+    <Optimize>false</Optimize>

   </PropertyGroup>

   <ItemGroup>

     <Reference Include="System" />

@@ -102,7 +104,7 @@
       <Name>Graph</Name>

     </ProjectReference>

     <ProjectReference Include="..\Model\Model.csproj">

-      <Project>{acef88d5-dadd-46da-bae1-2144d63f4c83}</Project>

+      <Project>{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}</Project>

       <Name>Model</Name>

     </ProjectReference>

     <ProjectReference Include="..\ParserHelper\ParserHelper.csproj">

diff --git a/Source/Model/Model.cs b/Source/Model/Model.cs
index 16dec8b0..3fafea97 100644
--- a/Source/Model/Model.cs
+++ b/Source/Model/Model.cs
@@ -695,305 +695,24 @@ namespace Microsoft.Boogie
       foreach (var f in functions) f.Substitute(mapping);

     }

 

-    class Parser

-    {

-      internal System.IO.TextReader rd;

-      string lastLine = "";

-      int lineNo;

-      internal List<Model> resModels = new List<Model>();

-      Model currModel;

-

-      void BadModel(string msg)

-      {

-        throw new ArgumentException(string.Format("Invalid model: {0}, at line {1} ({2})", msg, lineNo, lastLine));

-      }

-

-      static char[] seps = new char[] { ' ' };

-

-      int CountOpenParentheses(string s, int n) {

-        int f = n;

-        foreach (char c in s) {

-          if (c == '(')

-            f++;

-          else if (c == ')')

-            f--;

-        }

-        if (f < 0) BadModel("mismatched parentheses in datatype term");

-        return f;

-      }

-     

-      static Regex bv = new Regex(@"\(_ BitVec (\d+)\)");

-

-      /*

-      List<object> GetFunctionTuple(string newLine) {

-        if (newLine == null)

-          return null;

-        newLine = bv.Replace(newLine, "bv${1}");

-        string line = newLine;

-        int openParenCounter = CountOpenParentheses(newLine, 0);

-        if (!newLine.Contains("}")) {

-          while (openParenCounter > 0) {

-            newLine = ReadLine();

-            if (newLine == null) {

-              return null;

-            }

-            line += newLine;

-            openParenCounter = CountOpenParentheses(newLine, openParenCounter);

-          }

-        }

-

-        line = line.Replace("(", " ( ");

-        line = line.Replace(")", " ) ");

-        line = line.Replace(",", " ");

-        var tuple = line.Split(seps, StringSplitOptions.RemoveEmptyEntries);

-

-        List<object> newTuple = new List<object>();

-        Stack<int> wordStack = new Stack<int>();

-        for (int i = 0; i < tuple.Length; i++) {

-          string elem = tuple[i];

-          if (elem == "(") {

-            wordStack.Push(newTuple.Count - 1);

-          }

-          else if (elem == ")") {

-            int openParenIndex = wordStack.Pop();

-            List<object> ls = new List<object>();

-            for (int j = openParenIndex; j < newTuple.Count; j++)

-            {

-                ls.Add(newTuple[j]);

-            }

-            newTuple.RemoveRange(openParenIndex, newTuple.Count - openParenIndex);

-            newTuple.Add(ls);

-          }

-          else {

-            newTuple.Add(elem);

-          }

-        }

-        return newTuple;

-      }

-      */

-      

-      List<object> GetFunctionTuple(string newLine)

-      {

-          if (newLine == null)

-              return null;

-          newLine = bv.Replace(newLine, "bv${1}");

-          string line = newLine;

-          int openParenCounter = CountOpenParentheses(newLine, 0);

-          if (!newLine.Contains("}"))

-          {

-              while (openParenCounter > 0)

-              {

-                  newLine = ReadLine();

-                  if (newLine == null)

-                  {

-                      return null;

-                  }

-                  line += newLine;

-                  openParenCounter = CountOpenParentheses(newLine, openParenCounter);

-              }

-          }

-

-          line = line.Replace("(", " ( ");

-          line = line.Replace(")", " ) ");

-          var tuple = line.Split(seps, StringSplitOptions.RemoveEmptyEntries);

-

-          List<object> newTuple = new List<object>();

-          Stack<List<object>> wordStack = new Stack<List<object>>();

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

-          {

-              string elem = tuple[i];

-              if (elem == "(")

-              {

-                  List<object> ls = new List<object>();

-                  wordStack.Push(ls);

-              }

-              else if (elem == ")")

-              {

-                  List<object> ls = wordStack.Pop();

-                  if (wordStack.Count > 0)

-                  {

-                      wordStack.Peek().Add(ls);

-                  }

-                  else

-                  {

-                      newTuple.Add(ls);

-                  }

-              }

-              else if (wordStack.Count > 0)

-              {

-                  wordStack.Peek().Add(elem);

-              }

-              else

-              {

-                  newTuple.Add(elem);

-              }

-          }

-          return newTuple;

-      }

-  

-      string[] GetWords(string line)

-      {

-        if (line == null)

-          return null;

-        var words = line.Split(seps, StringSplitOptions.RemoveEmptyEntries);

-        return words;

-      }

-

-      string ReadLine()

-      {

-        var l = rd.ReadLine();

-        if (l != null) {

-          lineNo++;

-          lastLine = l;

-        }

-        return l;

-      }

-

-      Element GetElt(object o) {

-        string s = o as string;

-        if (s != null)

-          return GetElt(s);

-        List<object> os = (List<object>)o;

-        List<Element> args = new List<Element>();

-        for (int i = 1; i < os.Count; i++) {

-          args.Add(GetElt(os[i]));

-        }

-        return new DatatypeValue(currModel, (string)os[0], args);

-      }

-

-      Element GetElt(string name) {

-        Element ret = currModel.TryMkElement(name);

-        if (ret == null)

-          BadModel("invalid element name " + name);

-        return ret;

-      }

-

-      void NewModel()

-      {

-        lastLine = "";

-        currModel = new Model();

-        resModels.Add(currModel);

-      }

-

-      internal void Run()

-      {

-        var selectFunctions = new Dictionary<int, Model.Func>();

-        var storeFunctions = new Dictionary<int, Model.Func>();

-        for (; ; ) {

-          var line = ReadLine();

-          if (line == null) break; // end of model, everything fine

-

-          if (line == "Counterexample:" || line == "Z3 error model: " || line == "*** MODEL") {

-            NewModel();

-            continue;

-          }

-

-          if (line.EndsWith(": Invalid.") || line.EndsWith(": Valid.")|| line.StartsWith("labels:"))

-            continue;

-          if (line == "END_OF_MODEL" || line == "." || line == "*** END_MODEL")

-            continue;

-

-          var words = GetFunctionTuple(line);

-          if (words.Count == 0) continue;

-          var lastWord = words[words.Count - 1];

-

-          if (currModel == null)

-            BadModel("model begin marker not found");

-

-          if (line.StartsWith("*** STATE ")) {

-            var name = line.Substring(10);

-            CapturedState cs;

-            if (name == "<initial>")

-              cs = currModel.InitialState;

-            else

-              cs = currModel.MkState(name);

-            for (; ; ) {

-              var tmpline = ReadLine();

-              if (tmpline == "*** END_STATE") break;

-              var tuple = GetFunctionTuple(tmpline);

-              if (tuple == null) BadModel("EOF in state table");

-              if (tuple.Count == 0) continue;

-              if (tuple.Count == 3 && tuple[0] is string && tuple[1] is string && ((string) tuple[1]) == "->")

-              {

-                  cs.AddBinding((string)tuple[0], GetElt(tuple[2]));

-              }

-              else

-              {

-                  BadModel("invalid state tuple definition");

-              }

-            }

-            continue;

-          }

-

-          if (words.Count == 3 && words[1] is string && ((string) words[1]) == "->") {

-            var funName = (string) words[0];

-            Func fn = null;

-

-            if (lastWord is string && ((string) lastWord) == "{") {

-              fn = currModel.TryGetFunc(funName);

-              for ( ; ; ) {

-                var tuple = GetFunctionTuple(ReadLine());

-                if (tuple == null) BadModel("EOF in function table");

-                if (tuple.Count == 0) continue;

-                string tuple0 = tuple[0] as string;

-                if (tuple.Count == 1) {

-                  if (fn == null)

-                    fn = currModel.MkFunc(funName, 1);

-                  if (tuple0 == "}") break;

-                  if (fn.Else == null)

-                    fn.Else = GetElt(tuple[0]);

-                  continue;

-                }

-                string tuplePenultimate = tuple[tuple.Count - 2] as string;

-                if (tuplePenultimate != "->") BadModel("invalid function tuple definition");

-                var resultName = tuple[tuple.Count - 1];

-                if (tuple0 == "else") {

-                  if (fn != null && !(resultName is string && ((string)resultName) == "#unspecified") && fn.Else == null) {

-                    fn.Else = GetElt(resultName);

-                  }

-                  continue;

-                }

-

-                if (fn == null) {

-                  var arity = tuple.Count - 2;

-                  if (Regex.IsMatch(funName, "^MapType[0-9]*Select$")) {

-                    funName = string.Format("[{0}]", arity);

-                    if (!selectFunctions.TryGetValue(arity, out fn)) {

-                      fn = currModel.MkFunc(funName, arity);

-                      selectFunctions.Add(arity, fn);

-                    }

-                  } else if (Regex.IsMatch(funName, "^MapType[0-9]*Store$")) {

-                    funName = string.Format("[{0}:=]", arity);

-                    if (!storeFunctions.TryGetValue(arity, out fn)) {

-                      fn = currModel.MkFunc(funName, arity);

-                      storeFunctions.Add(arity, fn);

-                    }

-                  } else {

-                    fn = currModel.MkFunc(funName, arity);

-                  }

-                }

-                var args = new Element[fn.Arity];

-                for (int i = 0; i < fn.Arity; ++i)

-                  args[i] = GetElt(tuple[i]);

-                fn.AddApp(GetElt(resultName), args);

-              }

-            } else {

-              fn = currModel.MkFunc(funName, 0);

-              fn.SetConstant(GetElt(lastWord));

-            }

-          } else {

-            BadModel("unidentified line");

-          }

-        }

-      }

-    }

-

-    public static List<Model> ParseModels(System.IO.TextReader rd)

-    {

-      var p = new Parser();

-      p.rd = rd;

-      p.Run();

-      return p.resModels;

-    }

+	public static List<Model> ParseModels(System.IO.TextReader rd, string prover)

+	{

+	  ModelParser p;

+	

+	  switch (prover)

+	  {

+	    case "SMTLIB2":

+		  p = new ParserSMT();

+		  break;

+		default:

+		  p = new ParserZ3();

+		  break;

+	  }

+	

+	  p.rd = rd;

+	  p.Run();

+	

+	  return p.resModels;

+	}

   }

 }

diff --git a/Source/Model/Model.csproj b/Source/Model/Model.csproj
index a14dde8e..cfd5f852 100644
--- a/Source/Model/Model.csproj
+++ b/Source/Model/Model.csproj
@@ -36,7 +36,7 @@
     <SignAssembly>true</SignAssembly>

   </PropertyGroup>

   <PropertyGroup>

-    <AssemblyOriginatorKeyFile>../InterimKey.snk</AssemblyOriginatorKeyFile>

+    <AssemblyOriginatorKeyFile>..\InterimKey.snk</AssemblyOriginatorKeyFile>

   </PropertyGroup>

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

     <DebugSymbols>true</DebugSymbols>

@@ -77,12 +77,15 @@
     <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>

     <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>

     <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>

+    <WarningLevel>4</WarningLevel>

+    <Optimize>false</Optimize>

   </PropertyGroup>

   <ItemGroup>

     <Reference Include="System" />

   </ItemGroup>

   <ItemGroup>

     <Compile Include="Model.cs" />

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

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

     <Compile Include="..\version.cs" />

   </ItemGroup>

diff --git a/Source/Model/ModelParser.cs b/Source/Model/ModelParser.cs
new file mode 100644
index 00000000..dc6e06b5
--- /dev/null
+++ b/Source/Model/ModelParser.cs
@@ -0,0 +1,719 @@
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Linq;
+using System.Collections.Generic;
+using System.Text;
+using System.Diagnostics;
+using System.Text.RegularExpressions;
+
+namespace Microsoft.Boogie
+{
+	abstract internal class ModelParser
+	{
+		protected Model currModel;
+		int lineNo;
+		internal List<Model> resModels = new List<Model> ();
+		internal System.IO.TextReader rd;
+		string lastLine = "";
+		protected static char[] seps = new char[] { ' ' };
+		protected static Regex bv = new Regex (@"\(_ BitVec (\d+)\)");
+
+		protected void NewModel ()
+		{
+			lastLine = "";
+			currModel = new Model ();
+			resModels.Add (currModel);
+		}
+
+		protected void BadModel (string msg)
+		{
+			throw new ArgumentException (string.Format ("Invalid model: {0}, at line {1} ({2})", msg, lineNo, lastLine));
+		}
+
+		protected string ReadLine ()
+		{
+			var l = rd.ReadLine ();
+			if (l != null) {
+				lineNo++;
+				lastLine = l;
+			}
+			return l;
+		}
+
+		string[] GetWords (string line)
+		{
+			if (line == null)
+				return null;
+			var words = line.Split (seps, StringSplitOptions.RemoveEmptyEntries);
+			return words;
+		}
+
+		Model.Element GetElt (string name)
+		{
+			Model.Element ret = currModel.TryMkElement (name);
+			if (ret == null)
+				BadModel ("invalid element name " + name);
+			return ret;
+		}
+
+		protected Model.Element GetElt (object o)
+		{
+			string s = o as string;
+			if (s != null)
+				return GetElt (s);
+			List<object> os = (List<object>)o;
+			List<Model.Element> args = new List<Model.Element> ();
+			for (int i = 1; i < os.Count; i++) {
+				args.Add (GetElt (os [i]));
+			}
+			return new Model.DatatypeValue (currModel, (string)os [0], args);
+		}
+
+		protected int CountOpenParentheses (string s, int n)
+		{
+			int f = n;
+			foreach (char c in s) {
+				if (c == '(')
+					f++;
+				else if (c == ')')
+					f--;
+			}
+			if (f < 0)
+				BadModel ("mismatched parentheses in datatype term");
+			return f;
+		}
+
+		abstract internal void Run ();
+	}
+
+	class ParserZ3 : ModelParser
+	{
+		List<object> GetFunctionTokens (string newLine)
+		{
+			if (newLine == null)
+				return null;
+			newLine = bv.Replace (newLine, "bv${1}");
+			string line = newLine;
+			int openParenCounter = CountOpenParentheses (newLine, 0);
+			if (!newLine.Contains ("}")) {
+				while (openParenCounter > 0) {
+					newLine = ReadLine ();
+					if (newLine == null) {
+						return null;
+					}
+					line += newLine;
+					openParenCounter = CountOpenParentheses (newLine, openParenCounter);
+				}
+			}
+
+			line = line.Replace ("(", " ( ");
+			line = line.Replace (")", " ) ");
+			var tuple = line.Split (seps, StringSplitOptions.RemoveEmptyEntries);
+
+			List<object> newTuple = new List<object> ();
+			Stack<List<object>> wordStack = new Stack<List<object>> ();
+			for (int i = 0; i < tuple.Length; i++) {
+				string elem = tuple [i];
+				if (elem == "(") {
+					List<object> ls = new List<object> ();
+					wordStack.Push (ls);
+				} else if (elem == ")") {
+					List<object> ls = wordStack.Pop ();
+					if (wordStack.Count > 0) {
+						wordStack.Peek ().Add (ls);
+					} else {
+						newTuple.Add (ls);
+					}
+				} else if (wordStack.Count > 0) {
+					wordStack.Peek ().Add (elem);
+				} else {
+					newTuple.Add (elem);
+				}
+			}
+			return newTuple;
+		}
+
+		internal override void Run ()
+		{
+			var selectFunctions = new Dictionary<int, Model.Func> ();
+			var storeFunctions = new Dictionary<int, Model.Func> ();
+			for (; ;) {
+				var line = ReadLine ();
+				if (line == null)
+					break; // end of model, everything fine
+
+				if (line == "Counterexample:" || line == "Error model: " || line == "*** MODEL") {
+					NewModel ();
+					continue;
+				}
+
+				if (line.EndsWith (": Invalid.") || line.EndsWith (": Valid.") || line.StartsWith ("labels:"))
+					continue;
+				if (line == "END_OF_MODEL" || line == "." || line == "*** END_MODEL")
+					continue;
+
+				var words = GetFunctionTokens (line);
+				if (words.Count == 0)
+					continue;
+				var lastWord = words [words.Count - 1];
+
+				if (currModel == null)
+					BadModel ("model begin marker not found");
+
+				if (line.StartsWith ("*** STATE ")) {
+					var name = line.Substring (10);
+					Model.CapturedState cs;
+					if (name == "<initial>")
+						cs = currModel.InitialState;
+					else
+						cs = currModel.MkState (name);
+					for (; ;) {
+						var tmpline = ReadLine ();
+						if (tmpline == "*** END_STATE")
+							break;
+						var tuple = GetFunctionTokens (tmpline);
+						if (tuple == null)
+							BadModel ("EOF in state table");
+						if (tuple.Count == 0)
+							continue;
+						if (tuple.Count == 3 && tuple [0] is string && tuple [1] is string && ((string)tuple [1]) == "->") {
+							cs.AddBinding ((string)tuple [0], GetElt (tuple [2]));
+						} else {
+							BadModel ("invalid state tuple definition");
+						}
+					}
+					continue;
+				}
+
+				if (words.Count == 3 && words [1] is string && ((string)words [1]) == "->") {
+					var funName = (string)words [0];
+					Model.Func fn = null;
+
+					if (lastWord is string && ((string)lastWord) == "{") {
+						fn = currModel.TryGetFunc (funName);
+						for (; ;) {
+							var tuple = GetFunctionTokens (ReadLine ());
+							if (tuple == null)
+								BadModel ("EOF in function table");
+							if (tuple.Count == 0)
+								continue;
+							string tuple0 = tuple [0] as string;
+							if (tuple.Count == 1) {
+								if (fn == null)
+									fn = currModel.MkFunc (funName, 1);
+								if (tuple0 == "}")
+									break;
+								if (fn.Else == null)
+									fn.Else = GetElt (tuple [0]);
+								continue;
+							}
+							string tuplePenultimate = tuple [tuple.Count - 2] as string;
+							if (tuplePenultimate != "->")
+								BadModel ("invalid function tuple definition");
+							var resultName = tuple [tuple.Count - 1];
+							if (tuple0 == "else") {
+								if (fn != null && !(resultName is string && ((string)resultName) == "#unspecified") && fn.Else == null) {
+									fn.Else = GetElt (resultName);
+								}
+								continue;
+							}
+
+							if (fn == null) {
+								var arity = tuple.Count - 2;
+								if (Regex.IsMatch (funName, "^MapType[0-9]*Select$")) {
+									funName = string.Format ("[{0}]", arity);
+									if (!selectFunctions.TryGetValue (arity, out fn)) {
+										fn = currModel.MkFunc (funName, arity);
+										selectFunctions.Add (arity, fn);
+									}
+								} else if (Regex.IsMatch (funName, "^MapType[0-9]*Store$")) {
+									funName = string.Format ("[{0}:=]", arity);
+									if (!storeFunctions.TryGetValue (arity, out fn)) {
+										fn = currModel.MkFunc (funName, arity);
+										storeFunctions.Add (arity, fn);
+									}
+								} else {
+									fn = currModel.MkFunc (funName, arity);
+								}
+							}
+							var args = new Model.Element[fn.Arity];
+							for (int i = 0; i < fn.Arity; ++i)
+								args [i] = GetElt (tuple [i]);
+							fn.AddApp (GetElt (resultName), args);
+						}
+					} else {
+						fn = currModel.MkFunc (funName, 0);
+						fn.SetConstant (GetElt (lastWord));
+					}
+				} else {
+					BadModel ("unidentified line");
+				}
+			}
+		}
+	}
+
+	class ParserSMT : ModelParser
+	{
+		string[] tokens;
+		List<string> output;
+		int arity;
+		int arrayNum;
+		int index;
+
+		void FindArity ()
+		{
+			arity = 0;
+			int p_count = 1;
+			int i = 4;
+
+			while (p_count > 0) {
+				if (i == tokens.Length - 1)
+					break;
+				else if (tokens [i] == ")")
+					p_count--;
+				else if (tokens [i] == "(" && tokens [i + 1] != "ite") {
+					p_count++;
+					arity++;
+				}
+
+				i++;
+			}
+		}
+
+		string GetValue (int idx)
+		{
+			string value = tokens [idx];
+
+			if (tokens [idx - 1] == "-") {
+				value = "(- " + value + ")";
+			} else if (tokens [idx - 2] == "_") {
+				value = tokens [idx - 1] + "[" + tokens [idx] + "]";
+			}
+
+			return value;
+		}
+
+		List<string>[] TrySplitExpr (List<string> expr)
+		{
+			int splits = 1;
+			foreach (string tok in expr)
+				if (tok.Equals ("@SPLIT"))
+					splits++;
+
+			List<string>[] newExpr = new List<string>[splits];
+
+			for (int s = 0; s < splits; s++)
+				newExpr [s] = new List<string> ();
+
+			int i = 0;
+			foreach (string tok in expr) {
+				if (tok.Equals ("@SPLIT")) {
+					i++;
+					continue;
+				}
+
+				newExpr [i].Add (tok);
+			}
+
+			return newExpr;
+		}
+
+		void SplitArrayExpression ()
+		{
+			output.Add ("as-array[k!" + arrayNum + "]");
+
+			if (output.Contains ("@SPLIT")) {
+				output.Add (" ");
+				output.Add ("}");
+			}
+
+			output.Add ("@SPLIT");
+			output.Add ("k!" + arrayNum);
+			output.Add ("->");
+			output.Add ("{");
+			output.Add (" ");
+
+			arrayNum++;
+		}
+
+		void ParseArrayExpr ()
+		{
+			while (tokens [index] != "as-array" && tokens [index] != "store" && tokens [index] != "__array_store_all__")
+				index++;
+
+			if (tokens [index] == "store") {
+				SplitArrayExpression ();
+
+				List<string> args = new List<string> ();
+				int p_count = 1;
+				index += 4;
+
+				while (p_count > 0) {
+					if (tokens [index] == ")")
+						p_count--;
+					else if (tokens [index] == "(")
+						p_count++;
+					index++;
+				}
+
+				if ((tokens [index] == "(" && tokens [index + 1] == "__array_store_all__") ||
+					(tokens [index] == "(" && tokens [index + 1] == "store")) {
+					SplitArrayExpression ();
+				} else {
+					while (args.Count < 3) {
+						if (tokens [index] == ")")
+							index++;
+						else if (tokens [index] == "(") {
+							while (tokens [index] != ")")
+								index++;
+							args.Add (GetValue (index - 1));
+						} else {
+							args.Add (GetValue (index));
+						}
+
+						index++;
+					}
+
+					output.Add (args [1]);
+					output.Add ("->");
+					output.Add (args [2]);
+					output.Add (" ");
+					output.Add ("else");
+					output.Add ("->");
+					output.Add (args [0]);
+				}
+			} else if (tokens [index] == "__array_store_all__") {
+				SplitArrayExpression ();
+
+				while (tokens[index] == "__array_store_all__") {
+					int p_count = 1;
+					index += 2;
+
+					while (p_count > 0) {
+						if (tokens [index] == ")")
+							p_count--;
+						else if (tokens [index] == "(")
+							p_count++;
+						index++;
+					}
+
+					if (tokens [index] == "(" && tokens [index + 1] == "__array_store_all__") {
+						SplitArrayExpression ();
+						index++;
+					} else {
+						if (tokens [index] == ")")
+							index++;
+						else if (tokens [index] == "(") {
+							while (tokens [index] != ")")
+								index++;
+							output.Add (GetValue (index - 1));
+						} else {
+							output.Add (GetValue (index));
+						}
+
+						index++;
+					}
+				}
+			} else if (tokens [index] == "as-array") {
+				output.Add ("as-array[" + tokens [index + 1] + "]");
+			}
+		}
+
+		void ParseIteExpr ()
+		{
+			List<string> args = new List<string> ();
+			List<string> results = new List<string> ();
+
+			FindArity ();
+
+			for (; ;) {
+				index++;
+
+				if (tokens [index] == "=") {
+					while (tokens[index] != ")")
+						index++;
+					args.Add (GetValue (index - 1));
+				}
+
+				if (args.Count > 0 && args.Count % arity == 0) {
+					while (tokens[index] == ")")
+						index++;
+
+					if (tokens [index] == "(") {
+						while (tokens[index] != ")")
+							index++;
+						results.Add (GetValue (index - 1));
+					} else {
+						results.Add (GetValue (index));
+					}
+
+					while (index < tokens.Length - 1 && tokens[index + 1] != "=")
+						index++;
+
+					if (index == tokens.Length - 1) {
+						while (tokens[index] == ")")
+							index += -1;
+						results.Add (GetValue (index));
+						break;
+					}
+				}
+			}
+
+			int i = 0;
+
+			for (int j = 0; j < results.Count - 1; j++) {
+				for (int r = 0; r < arity; r++) {
+					output.Add (args [i]);
+					i++;
+				}
+
+				output.Add ("->");
+				output.Add (results [j]);
+				output.Add (" ");
+			}
+
+			output.Add ("else");
+			output.Add ("->");
+			output.Add (results [results.Count - 1]);
+		}
+
+		void ParseEndOfExpr ()
+		{
+			index++;
+
+			if (index == tokens.Length && output.Count == 2) {
+				index += -2;
+
+				if (tokens [index] == ")") {
+					index += -1;
+					output.Add (GetValue (index));
+				} else {
+					output.Add (GetValue (index));
+				}
+			}
+
+			if (index == tokens.Length && output.Contains ("{")) {
+				output.Add (" ");
+				output.Add ("}");
+			}
+		}
+
+		List<string> GetParsedTokens (string newLine)
+		{
+			if (newLine == null)
+				return null;
+			newLine = bv.Replace (newLine, "bv${1}");
+			string line = newLine;
+			int openParenCounter = CountOpenParentheses (newLine, 0);
+			while (openParenCounter > 0) {
+				newLine = ReadLine ();
+				if (newLine == null) {
+					return null;
+				}
+				line += newLine;
+				openParenCounter = CountOpenParentheses (newLine, openParenCounter);
+			}
+
+			line = line.Replace ("(", " ( ");
+			line = line.Replace (")", " ) ");
+
+			tokens = line.Split (seps, StringSplitOptions.RemoveEmptyEntries);
+			output = new List<string> ();
+
+			index = 0;
+			bool doneParsing = false;
+
+			while (!doneParsing) {
+				switch (tokens [index]) {
+				case ")":
+					ParseEndOfExpr ();
+					break;
+
+				case "define-fun":
+					output.Add (GetValue (index + 1));
+					output.Add ("->");
+					index += 2;
+					break;
+
+				case "_ufmt_1":
+				case "x!1":
+					output.Add ("{");
+					output.Add (" ");
+					if (Array.IndexOf (tokens, "ite") > -1)
+						ParseIteExpr ();
+					else
+						index++;
+					break;
+
+				case "Array":
+					ParseArrayExpr ();
+					break;
+
+				default:
+					index++;
+					break;
+				}
+
+				if (index == tokens.Length)
+					doneParsing = true;
+			}
+
+			return output;
+		}
+
+		internal override void Run ()
+		{
+			var selectFunctions = new Dictionary<int, Model.Func> ();
+			var storeFunctions = new Dictionary<int, Model.Func> ();
+			arrayNum = 0;
+
+			for (; ;) {
+				var line = ReadLine ();
+				if (line == null)
+					break; // end of model, everything fine
+				if (line == "Counterexample:" || line == "Error model: " || line == "*** MODEL") {
+					NewModel ();
+					continue;
+				}
+				if (line.EndsWith (": Invalid.") || line.EndsWith (": Valid.") || line.StartsWith ("labels:"))
+					continue;
+				if (line == "END_OF_MODEL" || line == "." || line == "*** END_MODEL")
+					continue;
+
+//				Console.WriteLine("\n\n# :: " + line);
+
+				var words = GetParsedTokens (line);
+				if (words.Count == 0)
+					continue;
+				var exprs = TrySplitExpr (words);
+
+				foreach (List<string> expr in exprs) {
+//					Console.WriteLine ("");
+//					for (int i = 0; i < expr.Count; i++) {
+//						Console.Write (expr [i] + " ");
+//					}
+
+					var lastToken = expr [expr.Count - 1];
+					if (currModel == null)
+						BadModel ("model begin marker not found");
+
+					if (expr.Count > 3 && expr [1] == "->") {
+						var funName = (string)expr [0];
+						Model.Func fn = null;
+						int i = 4;
+
+						if (expr [2] != "{" && expr [6] != "{")
+							BadModel ("unidentified function definition 5");
+
+						fn = currModel.TryGetFunc (funName);
+
+						for (; ;) {
+							if (expr [i] == "}") {
+								if (i == expr.Count - 1) {
+									if (fn == null)
+										fn = currModel.MkFunc (funName, 1);
+									break;
+								} else {
+									i++;
+									continue;
+								}
+							}
+
+							for (; ;) {
+								if (expr [i] == " ") {
+									i++;
+									break;
+								}
+
+								if ((i == 4 || i == 8) && expr [i - 1] == " " && expr [i + 1] == " ") {
+									if (fn.Else == null)
+										fn.Else = GetElt (expr [i]);
+									i++;
+									continue;
+								}
+
+								if (expr [i] == "else") {
+									if (expr [i + 1] == "->") {
+										i += 2;
+
+										if (expr [i] == "}")
+											BadModel ("unidentified function definition 1");
+
+										if (expr [i] == "{") {
+											i++;
+											continue;
+										} else {
+											if (fn != null && !(expr [i] == "#unspecified") && fn.Else == null)
+												fn.Else = GetElt (expr [i]);
+											i++;
+											continue;
+										}
+									} else
+										BadModel ("unidentified function definition 2");
+								}
+
+								int arity = 0;
+								for (; ;) {
+									arity++;
+									if (expr [arity + i] == " ") {
+										arity -= 2;
+										break;
+									}
+								}
+
+								if (expr [i + arity] == "->") {
+									i += arity + 1;
+
+									if (expr [i] == "}")
+										BadModel ("unidentified function definition 3");
+								} else
+									BadModel ("unidentified function definition 4");
+
+								if (fn == null) {
+									if (Regex.IsMatch (funName, "^MapType[0-9]*Select$")) {
+										funName = string.Format ("[{0}]", arity);
+
+										if (!selectFunctions.TryGetValue (arity, out fn)) {
+											fn = currModel.MkFunc (funName, arity);
+											selectFunctions.Add (arity, fn);
+										}
+									} else if (Regex.IsMatch (funName, "^MapType[0-9]*Store$")) {
+										funName = string.Format ("[{0}:=]", arity);
+
+										if (!storeFunctions.TryGetValue (arity, out fn)) {
+											fn = currModel.MkFunc (funName, arity);
+											storeFunctions.Add (arity, fn);
+										}
+									} else {
+										fn = currModel.MkFunc (funName, arity);
+									}
+								}
+
+								var args = new Model.Element[fn.Arity];
+
+								for (var idx = 0; idx < fn.Arity; ++idx)
+									args [idx] = GetElt (expr [idx + i - arity - 1]);
+
+								fn.AddApp (GetElt (expr [i]), args);
+
+								i++;
+								break;
+							}
+						}
+					} else if (expr.Count == 3 && expr [1] == "->") {
+						var funName = (string)expr [0];
+						Model.Func fn = null;
+
+						fn = currModel.MkFunc (funName, 0);
+						fn.SetConstant (GetElt (lastToken));
+					} else
+						BadModel ("unidentified line");
+				}
+			}
+		}
+	}
+}
diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs
index 1caed654..dfe24b6f 100644
--- a/Source/ModelViewer/Main.cs
+++ b/Source/ModelViewer/Main.cs
@@ -99,7 +99,7 @@ namespace Microsoft.Boogie.ModelViewer
 

       using (var rd = new StringReader(model))

       {

-        allModels = Model.ParseModels(rd).ToArray();

+        allModels = Model.ParseModels(rd, "").ToArray();

       }

 

       AddAndLoadModel(setModelIdTo);

@@ -112,7 +112,7 @@ namespace Microsoft.Boogie.ModelViewer
 

       if (!string.IsNullOrWhiteSpace(modelFileName) && File.Exists(modelFileName)) {

         using (var rd = File.OpenText(modelFileName)) {

-          allModels = Model.ParseModels(rd).ToArray();

+          allModels = Model.ParseModels(rd,"").ToArray();

         }

 

         AddAndLoadModel(setModelIdTo);

@@ -231,8 +231,13 @@ namespace Microsoft.Boogie.ModelViewer
       stateList.Columns[1].Width = stateList.Width - stateList.Columns[0].Width - stateList.Columns[2].Width - 25;

     }

 

-    void SetState(int id)

+    public void SetState(int id, bool updateView = false)

     {

+      if (updateView)

+      {

+        stateList.SelectedIndices.Clear();

+        stateList.SelectedIndices.Add(id);

+      }

       if (currentState != id) {

         previousState = currentState;

         currentState = id;

diff --git a/Source/ModelViewer/ModelViewer.csproj b/Source/ModelViewer/ModelViewer.csproj
index f708ddda..75e5521c 100644
--- a/Source/ModelViewer/ModelViewer.csproj
+++ b/Source/ModelViewer/ModelViewer.csproj
@@ -97,6 +97,8 @@
     <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>

     <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>

     <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>

+    <WarningLevel>4</WarningLevel>

+    <Optimize>false</Optimize>

   </PropertyGroup>

   <PropertyGroup>

     <StartupObject />

@@ -122,6 +124,7 @@
       <DependentUpon>Main.cs</DependentUpon>

     </Compile>

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

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

     <Compile Include="Namer.cs" />

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

     <Compile Include="SourceView.cs">

diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs
index c226d646..b4540717 100644
--- a/Source/ModelViewer/VccProvider.cs
+++ b/Source/ModelViewer/VccProvider.cs
@@ -274,7 +274,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       new string[] {

       "$_pow2", "$as_composite_field", "$as_field_with_type", "$as_in_range_t",

       "$as_primitive_field", "$base", "$call_transition", "tickleBool", "Ctor",

-      "@MV_state", "$field", "$field_arr_root", "$field_kind", "$field_offset",

+      "$mv_state", "$field", "$field_arr_root", "$field_kind", "$field_offset",

       "$field_parent_type", "$field_type", "$file_name_is", "$good_state",

       "$good_state_ext", "$function_arg_type", "$has_field_at0", "$map_domain",

       "$map_range", "$map_t", "$ptr_to", "$ptr_to_i1", "$ptr_to_i2",

diff --git a/Source/ParserHelper/ParserHelper.csproj b/Source/ParserHelper/ParserHelper.csproj
index cd665a75..f8155b61 100644
--- a/Source/ParserHelper/ParserHelper.csproj
+++ b/Source/ParserHelper/ParserHelper.csproj
@@ -99,6 +99,8 @@
     <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>

     <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>

     <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>

+    <WarningLevel>4</WarningLevel>

+    <Optimize>false</Optimize>

   </PropertyGroup>

   <ItemGroup>

     <Reference Include="System" />

diff --git a/Source/Predication/Predication.csproj b/Source/Predication/Predication.csproj
index 8060f52f..663de263 100644
--- a/Source/Predication/Predication.csproj
+++ b/Source/Predication/Predication.csproj
@@ -12,6 +12,8 @@
     <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>

     <FileAlignment>512</FileAlignment>

     <TargetFrameworkProfile>Client</TargetFrameworkProfile>

+    <ProductVersion>12.0.0</ProductVersion>

+    <SchemaVersion>2.0</SchemaVersion>

   </PropertyGroup>

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

     <DebugSymbols>true</DebugSymbols>

@@ -52,23 +54,23 @@
   </ItemGroup>

   <ItemGroup>

     <ProjectReference Include="..\Basetypes\Basetypes.csproj">

-      <Project>{43dfad18-3e35-4558-9be2-caff6b5ba8a0}</Project>

+      <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>

       <Name>Basetypes</Name>

     </ProjectReference>

     <ProjectReference Include="..\Core\Core.csproj">

-      <Project>{b230a69c-c466-4065-b9c1-84d80e76d802}</Project>

+      <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>

       <Name>Core</Name>

     </ProjectReference>

     <ProjectReference Include="..\Graph\Graph.csproj">

-      <Project>{69a2b0b8-bcac-4101-ae7a-556fcc58c06e}</Project>

+      <Project>{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}</Project>

       <Name>Graph</Name>

     </ProjectReference>

     <ProjectReference Include="..\ParserHelper\ParserHelper.csproj">

-      <Project>{fcd3ac7f-9dfd-46c8-ab1e-09f0b0f16dc5}</Project>

+      <Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project>

       <Name>ParserHelper</Name>

     </ProjectReference>

     <ProjectReference Include="..\VCGeneration\VCGeneration.csproj">

-      <Project>{e1f10180-c7b9-4147-b51f-fa1b701966dc}</Project>

+      <Project>{E1F10180-C7B9-4147-B51F-FA1B701966DC}</Project>

       <Name>VCGeneration</Name>

     </ProjectReference>

   </ItemGroup>

diff --git a/Source/Provers/SMTLib/CVC4.cs b/Source/Provers/SMTLib/CVC4.cs
new file mode 100644
index 00000000..0ac2ec20
--- /dev/null
+++ b/Source/Provers/SMTLib/CVC4.cs
@@ -0,0 +1,71 @@
+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+using System.Diagnostics.Contracts;

+using System.IO;

+using System.Text.RegularExpressions;

+

+namespace Microsoft.Boogie.SMTLib

+{

+    class CVC4

+    {

+        static string _proverPath;

+

+        static string CodebaseString()

+        {

+            Contract.Ensures(Contract.Result<string>() != null);

+            return Path.GetDirectoryName(cce.NonNull(System.Reflection.Assembly.GetExecutingAssembly().Location));

+        }

+

+        public static string ExecutablePath()

+        {

+            if (_proverPath == null)

+                FindExecutable();

+            return _proverPath;

+        }

+

+        static void FindExecutable()

+        // throws ProverException, System.IO.FileNotFoundException;

+        {

+            Contract.Ensures(_proverPath != null);

+

+            // Command line option 'cvc4exe' always has priority if set 

+            if (CommandLineOptions.Clo.CVC4ExecutablePath != null)

+            {

+                _proverPath = CommandLineOptions.Clo.CVC4ExecutablePath;

+                if (!File.Exists(_proverPath))

+                {

+                    throw new ProverException("Cannot find prover specified with cvc4exe: " + _proverPath);

+                }

+                if (CommandLineOptions.Clo.Trace)

+                {

+                    Console.WriteLine("[TRACE] Using prover: " + _proverPath);

+                }

+                return;

+            }

+

+            var proverExe = "cvc4.exe";

+

+            if (_proverPath == null)

+            {

+                // Initialize '_proverPath'

+                _proverPath = Path.Combine(CodebaseString(), proverExe);

+                string firstTry = _proverPath;

+

+                if (File.Exists(firstTry))

+                {

+                    if (CommandLineOptions.Clo.Trace)

+                    {

+                        Console.WriteLine("[TRACE] Using prover: " + _proverPath);

+                    }

+                    return;

+                }

+                else

+                {

+                    throw new ProverException("Cannot find executable: " + firstTry);

+                }

+            }

+        }

+    }

+}

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index ee955def..36e45fbc 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -109,14 +109,10 @@ namespace Microsoft.Boogie.SMTLib
           if (path == null)

             path = Z3.ExecutablePath();

           return SMTLibProcess.ComputerProcessStartInfo(path, "AUTO_CONFIG=false -smt2 -in");

-        case SolverKind.CVC3:

-          if (path == null)

-            path = "cvc3";

-          return SMTLibProcess.ComputerProcessStartInfo(path, "-lang smt2 +interactive -showPrompt");

         case SolverKind.CVC4:

           if (path == null)

             path = "cvc4";

-          return SMTLibProcess.ComputerProcessStartInfo(path, "--smtlib2 --no-strict-parsing");

+          return SMTLibProcess.ComputerProcessStartInfo(path, "--lang=smt --no-strict-parsing --no-condense-function-values --incremental");

         default:

           Debug.Assert(false);

           return null;

@@ -400,34 +396,38 @@ namespace Microsoft.Boogie.SMTLib
       FlushLogFile();

     }

 

-    public override void Reset()

+    public override void Reset ()

     {

-      SendThisVC("(reset)");

-      

-      if (0 < common.Length)

-      {

-        var c = common.ToString();

-        Process.Send(c);

-        if (currentLogFile != null)

-        {

-          currentLogFile.WriteLine(c);

+      if (options.Solver == SolverKind.Z3) {

+        SendThisVC ("(reset)");

+		

+	    if (0 < common.Length)

+		{

+          var c = common.ToString ();

+          Process.Send (c);

+          if (currentLogFile != null)

+		  {

+            currentLogFile.WriteLine (c);

+          }

         }

       }

     }

-

-    public override void FullReset()

+	

+    public override void FullReset ()

     {

-      Namer.Reset();

-      common.Clear();

-      SetupAxiomBuilder(gen);

-      Axioms.Clear();

-      TypeDecls.Clear();

-      AxiomsAreSetup = false;

-      ctx.Reset();

-      ctx.KnownDatatypeConstructors.Clear();

-      ctx.parent = this;

-      DeclCollector.Reset();

-      SendThisVC("; doing a full reset...");

+      if (options.Solver == SolverKind.Z3) {

+        Namer.Reset ();

+        common.Clear ();

+        SetupAxiomBuilder (gen);

+        Axioms.Clear ();

+        TypeDecls.Clear ();

+        AxiomsAreSetup = false;

+        ctx.Reset ();

+        ctx.KnownDatatypeConstructors.Clear ();

+        ctx.parent = this;

+        DeclCollector.Reset ();

+        SendThisVC ("; doing a full reset...");

+      }

     }

 

     private RPFP.Node SExprToCex(SExpr resp, ErrorHandler handler, 

@@ -556,7 +556,7 @@ namespace Microsoft.Boogie.SMTLib
         // Concatenate all the arguments

         string modelString = resp[0].Name;

         // modelString = modelString.Substring(7, modelString.Length - 8); // remove "(model " and final ")"

-        var models = Model.ParseModels(new StringReader("Z3 error model: \n" + modelString));

+        var models = Model.ParseModels(new StringReader("Z3 error model: \n" + modelString), "");

         if (models == null || models.Count == 0)

         {

             HandleProverError("no model from prover: " + resp.ToString());

@@ -923,9 +923,14 @@ namespace Microsoft.Boogie.SMTLib
         if (theModel != null)

           HandleProverError("Expecting only one model but got many");

         

+		

         string modelStr = null;

         if (resp.Name == "model" && resp.ArgCount >= 1) {

-          modelStr = resp[0].Name;

+          modelStr = resp.Arguments[0] + "\n";

+          for (int i = 1; i < resp.ArgCount; i++) {

+            if (resp.Arguments[i].ToString().Contains("define-fun") &&!resp.Arguments[i].ToString().Contains("not"))

+              modelStr += resp.Arguments[i] + "\n";

+          }

         }

         else if (resp.ArgCount == 0 && resp.Name.Contains("->")) {

           modelStr = resp.Name;

@@ -933,9 +938,24 @@ namespace Microsoft.Boogie.SMTLib
         else {

           HandleProverError("Unexpected prover response getting model: " + resp.ToString());

         }

+        

         List<Model> models = null;

         try {

-          models = Model.ParseModels(new StringReader("Z3 error model: \n" + modelStr));

+          switch (options.Solver) {

+            case SolverKind.Z3:

+              if (CommandLineOptions.Clo.UseSmtOutputFormat) {

+                models = Model.ParseModels(new StringReader("Error model: \n" + modelStr), "SMTLIB2");

+              } else {

+                models = Model.ParseModels(new StringReader("Error model: \n" + modelStr), "");

+              }

+              break;

+            case SolverKind.CVC4:

+              models = Model.ParseModels(new StringReader("Error model: \n" + modelStr), "SMTLIB2");

+              break;

+            default:

+              Debug.Assert(false);

+              return null;

+          }

         }

         catch (ArgumentException exn) {

           HandleProverError("Model parsing error: " + exn.Message);

@@ -1211,15 +1231,17 @@ namespace Microsoft.Boogie.SMTLib
         SendThisVC("(check-sat)");

         FlushLogFile();

     }

-

+	

     public override void SetTimeOut(int ms)

     {

-        var name = Z3.SetTimeoutOption();

-        var value = ms.ToString();

-        options.TimeLimit = ms;

-        options.SmtOptions.RemoveAll(ov => ov.Option == name);

-        options.AddSmtOption(name, value);

-        SendThisVC(string.Format("(set-option :{0} {1})", name, value));

+	    if (options.Solver == SolverKind.Z3) {

+            var name = Z3.SetTimeoutOption();

+            var value = ms.ToString();

+            options.TimeLimit = ms;

+            options.SmtOptions.RemoveAll(ov => ov.Option == name);

+            options.AddSmtOption(name, value);

+            SendThisVC(string.Format("(set-option :{0} {1})", name, value));

+	    }

     }

 

     public override object Evaluate(VCExpr expr)

diff --git a/Source/Provers/SMTLib/SMTLib.csproj b/Source/Provers/SMTLib/SMTLib.csproj
index c58d3349..bc1b7e02 100644
--- a/Source/Provers/SMTLib/SMTLib.csproj
+++ b/Source/Provers/SMTLib/SMTLib.csproj
@@ -97,6 +97,8 @@
     <ErrorReport>prompt</ErrorReport>

     <CodeAnalysisRuleSet>Migrated rules for SMTLib.ruleset</CodeAnalysisRuleSet>

     <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>

+    <WarningLevel>4</WarningLevel>

+    <Optimize>false</Optimize>

   </PropertyGroup>

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

     <DebugSymbols>true</DebugSymbols>

@@ -137,6 +139,8 @@
     <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>

     <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>

     <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>

+    <WarningLevel>4</WarningLevel>

+    <Optimize>false</Optimize>

   </PropertyGroup>

   <ItemGroup>

     <Reference Include="System" />

@@ -157,6 +161,7 @@
     <Compile Include="TypeDeclCollector.cs" />

     <Compile Include="..\..\version.cs" />

     <Compile Include="Z3.cs" />

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

   </ItemGroup>

   <ItemGroup>

     <ProjectReference Include="..\..\Basetypes\Basetypes.csproj">

@@ -172,7 +177,7 @@
       <Name>Core</Name>

     </ProjectReference>

     <ProjectReference Include="..\..\Graph\Graph.csproj">

-      <Project>{69a2b0b8-bcac-4101-ae7a-556fcc58c06e}</Project>

+      <Project>{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}</Project>

       <Name>Graph</Name>

     </ProjectReference>

     <ProjectReference Include="..\..\Model\Model.csproj">

diff --git a/Source/Provers/SMTLib/SMTLibProverOptions.cs b/Source/Provers/SMTLib/SMTLibProverOptions.cs
index d336252e..3f4ef5ac 100644
--- a/Source/Provers/SMTLib/SMTLibProverOptions.cs
+++ b/Source/Provers/SMTLib/SMTLibProverOptions.cs
@@ -27,7 +27,7 @@ namespace Microsoft.Boogie.SMTLib
     }

   }

 

-  public enum SolverKind { Z3, CVC3, CVC4 };

+  public enum SolverKind { Z3, CVC4 };

 

   public class SMTLibProverOptions : ProverOptions

   {

@@ -43,6 +43,7 @@ namespace Microsoft.Boogie.SMTLib
     // Z3 specific (at the moment; some of them make sense also for other provers)

     public string Inspector = null;

     public bool OptimizeForBv = false;

+	public bool SMTLib2Model = false;

 

     public bool ProduceModel() {

       return !CommandLineOptions.Clo.UseLabels || CommandLineOptions.Clo.ExplainHoudini || CommandLineOptions.Clo.UseProverEvaluate ||

@@ -89,16 +90,12 @@ namespace Microsoft.Boogie.SMTLib
           case "z3":

             Solver = SolverKind.Z3;

             break;

-          case "cvc3":

-            Solver = SolverKind.CVC3;

-            Logic = "ALL";

-            break;

           case "cvc4":

             Solver = SolverKind.CVC4;

-            Logic = "ALL_SUPPORTED";

+			if (Logic.Equals("")) Logic = "ALL_SUPPORTED";

             break;

           default:

-            ReportError("Invalid SOLVER value; must be 'z3', 'cvc3' or 'cvc4'");

+            ReportError("Invalid SOLVER value; must be 'z3' or 'cvc4'");

             return false;

         }

         return true;

@@ -119,6 +116,7 @@ namespace Microsoft.Boogie.SMTLib
         ParseBool(opt, "USE_WEIGHTS", ref UseWeights) ||

         ParseString(opt, "INSPECTOR", ref Inspector) ||

         ParseBool(opt, "OPTIMIZE_FOR_BV", ref OptimizeForBv) ||

+		ParseBool(opt, "SMTLIB2_MODEL", ref SMTLib2Model) ||

         ParseString(opt, "LOGIC", ref Logic) ||

         base.Parse(opt);

     }

@@ -138,18 +136,19 @@ namespace Microsoft.Boogie.SMTLib
 @"

 SMT-specific options:

 ~~~~~~~~~~~~~~~~~~~~~

-SOLVER=<string>           Use the given SMT solver (z3, cvc3, cvc4; default: z3)

+SOLVER=<string>           Use the given SMT solver (z3 or cvc4; default: z3)

 USE_WEIGHTS=<bool>        Pass :weight annotations on quantified formulas (default: true)

 VERBOSITY=<int>           1 - print prover output (default: 0)

 O:<name>=<value>          Pass (set-option :<name> <value>) to the SMT solver.

 C:<string>                Pass <string> to the SMT on the command line. 

-LOGIC=<string>            Pass (set-logic <string>) to the prover (default: empty, 'ALL' for CVC3 or 'ALL_SUPPORTED' for CVC4)

+LOGIC=<string>            Pass (set-logic <string>) to the prover (default: empty, 'ALL_SUPPORTED' for CVC4)

 

 Z3-specific options:

 ~~~~~~~~~~~~~~~~~~~~

 MULTI_TRACES=<bool>       Report errors with multiple paths leading to the same assertion.

 INSPECTOR=<string>        Use the specified Z3Inspector binary.

 OPTIMIZE_FOR_BV=<bool>    Optimize Z3 options for bitvector reasoning, and not quantifier instantiation. Defaults to false.

+SMTLIB2_MODEL=<bool>      Use the SMTLIB2 output model. Defaults to false.

 " + base.Help;

       }

     }

diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs
index 24071457..d2e06168 100644
--- a/Source/Provers/SMTLib/Z3.cs
+++ b/Source/Provers/SMTLib/Z3.cs
@@ -283,9 +283,14 @@ namespace Microsoft.Boogie.SMTLib
                 //options.AddWeakSmtOption("MODEL_PARTIAL", "true");

                 //options.WeakAddSmtOption("MODEL_VALUE_COMPLETION", "false");

                 options.AddWeakSmtOption("MODEL_HIDE_UNUSED_PARTITIONS", "false");

-                options.AddWeakSmtOption("MODEL_V2", "true");

                 options.AddWeakSmtOption("ASYNC_COMMANDS", "false");

 

+				if (CommandLineOptions.Clo.UseSmtOutputFormat) {

+					options.AddWeakSmtOption("pp-bv-literals", "false");;

+				} else {

+					options.AddWeakSmtOption("MODEL_V2", "true");

+				}

+

                 if (!options.OptimizeForBv)

                 {

                     // Phase selection means to always try the negative literal polarity first, seems to be good for Boogie.

diff --git a/Source/VCExpr/VCExpr.csproj b/Source/VCExpr/VCExpr.csproj
index bd426125..19873dbc 100644
--- a/Source/VCExpr/VCExpr.csproj
+++ b/Source/VCExpr/VCExpr.csproj
@@ -97,6 +97,8 @@
     <ErrorReport>prompt</ErrorReport>

     <CodeAnalysisRuleSet>Migrated rules for VCExpr.ruleset</CodeAnalysisRuleSet>

     <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>

+    <WarningLevel>4</WarningLevel>

+    <Optimize>false</Optimize>

   </PropertyGroup>

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

     <DebugSymbols>true</DebugSymbols>

@@ -137,6 +139,8 @@
     <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>

     <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>

     <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>

+    <WarningLevel>4</WarningLevel>

+    <Optimize>false</Optimize>

   </PropertyGroup>

   <ItemGroup>

     <Reference Include="System" />

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 202557ff..dbe20415 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -237,7 +237,7 @@ namespace Microsoft.Boogie {
       Model m = Model;

       ApplyRedirections(m); 

 

-      var mvstates = m.TryGetFunc("@MV_state");

+      var mvstates = m.TryGetFunc("$mv_state");

       if (MvInfo == null || mvstates == null)

         return;

 

@@ -1702,11 +1702,11 @@ namespace VC {
   {

     public readonly List<Variable> AllVariables = new List<Variable>();

     public readonly List<Mapping> CapturePoints = new List<Mapping>();

-    public static readonly Function MVState_FunctionDef = new Function(Token.NoToken, "@MV_state",

+    public static readonly Function MVState_FunctionDef = new Function(Token.NoToken, "$mv_state",

       new VariableSeq(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, TypedIdent.NoName, Bpl.Type.Int), true),

                       new Formal(Token.NoToken, new TypedIdent(Token.NoToken, TypedIdent.NoName, Bpl.Type.Int), true)),

       new Formal(Token.NoToken, new TypedIdent(Token.NoToken, TypedIdent.NoName, Bpl.Type.Bool), false));

-    public static readonly Constant MVState_ConstantDef = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, "@MV_state_const", Bpl.Type.Int));

+    public static readonly Constant MVState_ConstantDef = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, "$mv_state_const", Bpl.Type.Int));

 

     public ModelViewInfo(Program program, Implementation impl) {

       Contract.Requires(program != null);

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index 01b34504..da413984 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -2444,7 +2444,7 @@ namespace VC {
       private void GetModelWithStates(Model m) {

         if (m == null) return;

         var mvInfo = mainInfo.mvInfo;

-        var mvstates = m.TryGetFunc("@MV_state");

+        var mvstates = m.TryGetFunc("$mv_state");

         if (mvstates == null)

           return;

 

diff --git a/Source/VCGeneration/VCGeneration.csproj b/Source/VCGeneration/VCGeneration.csproj
index f724307b..a7be5827 100644
--- a/Source/VCGeneration/VCGeneration.csproj
+++ b/Source/VCGeneration/VCGeneration.csproj
@@ -97,6 +97,8 @@
     <ErrorReport>prompt</ErrorReport>

     <CodeAnalysisRuleSet>Migrated rules for VCGeneration.ruleset</CodeAnalysisRuleSet>

     <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>

+    <WarningLevel>4</WarningLevel>

+    <Optimize>false</Optimize>

   </PropertyGroup>

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

     <DebugSymbols>true</DebugSymbols>

@@ -137,6 +139,8 @@
     <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>

     <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>

     <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>

+    <WarningLevel>4</WarningLevel>

+    <Optimize>false</Optimize>

   </PropertyGroup>

   <ItemGroup>

     <Reference Include="System" />