diff options
| author |  Pantazis Deligiannis <pdeligia@me.com> | 2013-07-15 12:21:57 +0100 |
|---|---|---|
| committer | Pantazis Deligiannis <pdeligia@me.com> | 2013-07-15 12:21:57 +0100 |
| commit | 578382b6bd2ace4926e9ed97cf59ec38c7b07797 (patch) | |
| tree | 5ea634e0c5c2881f674c38c5d3b1307c83db8916 /Source | |
| parent | ad34aee0bb9e9090418fd1cb2e2fced7ddb625d8 (diff) | |
| parent | ee4be4f6280d39c31d95e50ac3ac039c6d2ba5f5 (diff) | |
Merge
Diffstat (limited to 'Source')
28 files changed, 1962 insertions, 1337 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/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/Boogie.sln b/Source/Boogie.sln index b93bc31f..c83c8770 100644 --- a/Source/Boogie.sln +++ b/Source/Boogie.sln @@ -3,12 +3,12 @@ Microsoft Visual Studio Solution File, Format Version 12.00 # Visual Studio 2012
Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = "Provers", "Provers", "{B758C1E3-824A-439F-AA2F-0BA1143E8C8D}"
EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "SMTLib", "Provers\SMTLib\SMTLib.csproj", "{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}"
+EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "BoogieDriver", "BoogieDriver\BoogieDriver.csproj", "{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}"
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "AbsInt", "AbsInt\AbsInt.csproj", "{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}"
EndProject
-Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "SMTLib", "Provers\SMTLib\SMTLib.csproj", "{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}"
-EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "VCGeneration", "VCGeneration\VCGeneration.csproj", "{E1F10180-C7B9-4147-B51F-FA1B701966DC}"
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "VCExpr", "VCExpr\VCExpr.csproj", "{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}"
@@ -55,32 +55,6 @@ Global z3apidebug|x86 = z3apidebug|x86
EndGlobalSection
GlobalSection(ProjectConfigurationPlatforms) = postSolution
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Checked|.NET.ActiveCfg = Checked|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Checked|Any CPU.ActiveCfg = Checked|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Checked|Any CPU.Build.0 = Checked|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Checked|Mixed Platforms.Build.0 = Checked|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Checked|x86.ActiveCfg = Checked|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Debug|.NET.ActiveCfg = Debug|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Debug|.NET.Build.0 = Debug|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Debug|Any CPU.Build.0 = Debug|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Debug|x86.ActiveCfg = Debug|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Release|.NET.ActiveCfg = Release|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Release|Any CPU.ActiveCfg = Release|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Release|Any CPU.Build.0 = Release|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Release|Mixed Platforms.Build.0 = Release|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Release|x86.ActiveCfg = Release|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.z3apidebug|.NET.ActiveCfg = z3apidebug|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.z3apidebug|Any CPU.ActiveCfg = z3apidebug|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.z3apidebug|Any CPU.Build.0 = z3apidebug|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.z3apidebug|Mixed Platforms.ActiveCfg = Debug|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.z3apidebug|x86.ActiveCfg = z3apidebug|x86
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.z3apidebug|x86.Build.0 = z3apidebug|x86
{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
@@ -107,58 +81,31 @@ Global {0EFA3E43-690B-48DC-A72C-384A3EA7F31F}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU
{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}.z3apidebug|x86.ActiveCfg = z3apidebug|x86
{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}.z3apidebug|x86.Build.0 = z3apidebug|x86
- {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
- {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU
- {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Checked|Mixed Platforms.Build.0 = Checked|Any CPU
- {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Checked|x86.ActiveCfg = Checked|Any CPU
- {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Debug|.NET.ActiveCfg = Debug|Any CPU
- {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Debug|.NET.Build.0 = Debug|Any CPU
- {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
- {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Debug|Any CPU.Build.0 = Debug|Any CPU
- {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
- {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
- {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Debug|x86.ActiveCfg = Debug|Any CPU
- {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Release|.NET.ActiveCfg = Release|Any CPU
- {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Release|Any CPU.ActiveCfg = Release|Any CPU
- {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Release|Any CPU.Build.0 = Release|Any CPU
- {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
- {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Release|Mixed Platforms.Build.0 = Release|Any CPU
- {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Release|x86.ActiveCfg = Release|Any CPU
- {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.z3apidebug|.NET.ActiveCfg = z3apidebug|Any CPU
- {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.z3apidebug|Any CPU.ActiveCfg = z3apidebug|Any CPU
- {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.z3apidebug|Any CPU.Build.0 = z3apidebug|Any CPU
- {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.z3apidebug|Mixed Platforms.ActiveCfg = Debug|Any CPU
- {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU
- {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU
- {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.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
- {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU
- {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Checked|Mixed Platforms.Build.0 = Checked|Any CPU
- {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Checked|x86.ActiveCfg = Checked|Any CPU
- {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Debug|.NET.ActiveCfg = Debug|Any CPU
- {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Debug|.NET.Build.0 = Debug|Any CPU
- {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
- {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Debug|Any CPU.Build.0 = Debug|Any CPU
- {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
- {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
- {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Debug|x86.ActiveCfg = Debug|Any CPU
- {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Release|.NET.ActiveCfg = Release|Any CPU
- {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Release|Any CPU.ActiveCfg = Release|Any CPU
- {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Release|Any CPU.Build.0 = Release|Any CPU
- {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
- {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Release|Mixed Platforms.Build.0 = Release|Any CPU
- {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Release|x86.ActiveCfg = Release|Any CPU
- {E1F10180-C7B9-4147-B51F-FA1B701966DC}.z3apidebug|.NET.ActiveCfg = z3apidebug|Any CPU
- {E1F10180-C7B9-4147-B51F-FA1B701966DC}.z3apidebug|Any CPU.ActiveCfg = z3apidebug|Any CPU
- {E1F10180-C7B9-4147-B51F-FA1B701966DC}.z3apidebug|Any CPU.Build.0 = z3apidebug|Any CPU
- {E1F10180-C7B9-4147-B51F-FA1B701966DC}.z3apidebug|Mixed Platforms.ActiveCfg = Debug|Any CPU
- {E1F10180-C7B9-4147-B51F-FA1B701966DC}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU
- {E1F10180-C7B9-4147-B51F-FA1B701966DC}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU
- {E1F10180-C7B9-4147-B51F-FA1B701966DC}.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
+ {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU
+ {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Checked|Mixed Platforms.Build.0 = Checked|Any CPU
+ {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Checked|x86.ActiveCfg = Checked|Any CPU
+ {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Debug|.NET.ActiveCfg = Debug|Any CPU
+ {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Debug|Any CPU.Build.0 = Debug|Any CPU
+ {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
+ {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
+ {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Debug|x86.ActiveCfg = Debug|Any CPU
+ {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Release|.NET.ActiveCfg = Release|Any CPU
+ {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Release|Any CPU.Build.0 = Release|Any CPU
+ {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Release|Mixed Platforms.Build.0 = Release|Any CPU
+ {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Release|x86.ActiveCfg = Release|Any CPU
+ {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.z3apidebug|.NET.ActiveCfg = z3apidebug|Any CPU
+ {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.z3apidebug|Any CPU.ActiveCfg = z3apidebug|Any CPU
+ {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.z3apidebug|Any CPU.Build.0 = z3apidebug|Any CPU
+ {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.z3apidebug|Mixed Platforms.ActiveCfg = Debug|Any CPU
+ {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU
+ {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU
+ {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.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
@@ -184,31 +131,6 @@ Global {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
- {B230A69C-C466-4065-B9C1-84D80E76D802}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU
- {B230A69C-C466-4065-B9C1-84D80E76D802}.Checked|Mixed Platforms.Build.0 = Checked|Any CPU
- {B230A69C-C466-4065-B9C1-84D80E76D802}.Checked|x86.ActiveCfg = Checked|Any CPU
- {B230A69C-C466-4065-B9C1-84D80E76D802}.Debug|.NET.ActiveCfg = Debug|Any CPU
- {B230A69C-C466-4065-B9C1-84D80E76D802}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
- {B230A69C-C466-4065-B9C1-84D80E76D802}.Debug|Any CPU.Build.0 = Debug|Any CPU
- {B230A69C-C466-4065-B9C1-84D80E76D802}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
- {B230A69C-C466-4065-B9C1-84D80E76D802}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
- {B230A69C-C466-4065-B9C1-84D80E76D802}.Debug|x86.ActiveCfg = Debug|Any CPU
- {B230A69C-C466-4065-B9C1-84D80E76D802}.Release|.NET.ActiveCfg = Release|Any CPU
- {B230A69C-C466-4065-B9C1-84D80E76D802}.Release|Any CPU.ActiveCfg = Release|Any CPU
- {B230A69C-C466-4065-B9C1-84D80E76D802}.Release|Any CPU.Build.0 = Release|Any CPU
- {B230A69C-C466-4065-B9C1-84D80E76D802}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
- {B230A69C-C466-4065-B9C1-84D80E76D802}.Release|Mixed Platforms.Build.0 = Release|Any CPU
- {B230A69C-C466-4065-B9C1-84D80E76D802}.Release|x86.ActiveCfg = Release|Any CPU
- {B230A69C-C466-4065-B9C1-84D80E76D802}.z3apidebug|.NET.ActiveCfg = z3apidebug|Any CPU
- {B230A69C-C466-4065-B9C1-84D80E76D802}.z3apidebug|Any CPU.ActiveCfg = z3apidebug|Any CPU
- {B230A69C-C466-4065-B9C1-84D80E76D802}.z3apidebug|Any CPU.Build.0 = z3apidebug|Any CPU
- {B230A69C-C466-4065-B9C1-84D80E76D802}.z3apidebug|Mixed Platforms.ActiveCfg = Debug|Any CPU
- {B230A69C-C466-4065-B9C1-84D80E76D802}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU
- {B230A69C-C466-4065-B9C1-84D80E76D802}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU
- {B230A69C-C466-4065-B9C1-84D80E76D802}.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
@@ -234,31 +156,80 @@ Global {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
- {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU
- {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Checked|Mixed Platforms.Build.0 = Checked|Any CPU
- {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Checked|x86.ActiveCfg = Checked|Any CPU
- {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Debug|.NET.ActiveCfg = Debug|Any CPU
- {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
- {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Debug|Any CPU.Build.0 = Debug|Any CPU
- {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
- {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
- {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Debug|x86.ActiveCfg = Debug|Any CPU
- {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Release|.NET.ActiveCfg = Release|Any CPU
- {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Release|Any CPU.ActiveCfg = Release|Any CPU
- {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Release|Any CPU.Build.0 = Release|Any CPU
- {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
- {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Release|Mixed Platforms.Build.0 = Release|Any CPU
- {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Release|x86.ActiveCfg = Release|Any CPU
- {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.z3apidebug|.NET.ActiveCfg = z3apidebug|Any CPU
- {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.z3apidebug|Any CPU.ActiveCfg = z3apidebug|Any CPU
- {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.z3apidebug|Any CPU.Build.0 = z3apidebug|Any CPU
- {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.z3apidebug|Mixed Platforms.ActiveCfg = Debug|Any CPU
- {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU
- {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU
- {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.z3apidebug|x86.Build.0 = z3apidebug|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Checked|.NET.ActiveCfg = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Checked|Any CPU.ActiveCfg = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Checked|Any CPU.Build.0 = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Checked|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Checked|Mixed Platforms.Build.0 = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Checked|x86.ActiveCfg = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Debug|.NET.ActiveCfg = Debug|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Debug|Any CPU.Build.0 = Debug|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Debug|x86.ActiveCfg = Debug|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Release|.NET.ActiveCfg = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Release|Any CPU.Build.0 = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Release|Mixed Platforms.Build.0 = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Release|x86.ActiveCfg = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.z3apidebug|.NET.ActiveCfg = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.z3apidebug|Any CPU.ActiveCfg = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.z3apidebug|Any CPU.Build.0 = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.z3apidebug|x86.ActiveCfg = Release|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
+ {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU
+ {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Checked|Mixed Platforms.Build.0 = Checked|Any CPU
+ {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Checked|x86.ActiveCfg = Checked|Any CPU
+ {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Debug|.NET.ActiveCfg = Debug|Any CPU
+ {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Debug|.NET.Build.0 = Debug|Any CPU
+ {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Debug|Any CPU.Build.0 = Debug|Any CPU
+ {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
+ {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
+ {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Debug|x86.ActiveCfg = Debug|Any CPU
+ {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Release|.NET.ActiveCfg = Release|Any CPU
+ {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Release|Any CPU.Build.0 = Release|Any CPU
+ {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Release|Mixed Platforms.Build.0 = Release|Any CPU
+ {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Release|x86.ActiveCfg = Release|Any CPU
+ {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.z3apidebug|.NET.ActiveCfg = z3apidebug|Any CPU
+ {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.z3apidebug|Any CPU.ActiveCfg = z3apidebug|Any CPU
+ {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.z3apidebug|Any CPU.Build.0 = z3apidebug|Any CPU
+ {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.z3apidebug|Mixed Platforms.ActiveCfg = Debug|Any CPU
+ {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU
+ {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU
+ {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.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
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Checked|Mixed Platforms.Build.0 = Checked|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Checked|x86.ActiveCfg = Checked|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Checked|x86.Build.0 = Checked|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Debug|.NET.ActiveCfg = Debug|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Debug|Any CPU.ActiveCfg = Debug|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Debug|Mixed Platforms.ActiveCfg = Debug|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Debug|Mixed Platforms.Build.0 = Debug|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Debug|x86.ActiveCfg = Debug|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Debug|x86.Build.0 = Debug|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Release|.NET.ActiveCfg = Release|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Release|Any CPU.ActiveCfg = Release|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Release|Mixed Platforms.ActiveCfg = Release|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Release|Mixed Platforms.Build.0 = Release|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Release|x86.ActiveCfg = Release|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Release|x86.Build.0 = Release|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.z3apidebug|.NET.ActiveCfg = Release|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.z3apidebug|Any CPU.ActiveCfg = Release|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.z3apidebug|Mixed Platforms.ActiveCfg = Release|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.z3apidebug|Mixed Platforms.Build.0 = Release|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.z3apidebug|x86.ActiveCfg = Release|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.z3apidebug|x86.Build.0 = Release|x86
{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
@@ -284,30 +255,6 @@ Global {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
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Checked|Mixed Platforms.Build.0 = Checked|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Checked|x86.ActiveCfg = Checked|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Checked|x86.Build.0 = Checked|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Debug|.NET.ActiveCfg = Debug|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Debug|Any CPU.ActiveCfg = Debug|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Debug|Mixed Platforms.ActiveCfg = Debug|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Debug|Mixed Platforms.Build.0 = Debug|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Debug|x86.ActiveCfg = Debug|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Debug|x86.Build.0 = Debug|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Release|.NET.ActiveCfg = Release|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Release|Any CPU.ActiveCfg = Release|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Release|Mixed Platforms.ActiveCfg = Release|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Release|Mixed Platforms.Build.0 = Release|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Release|x86.ActiveCfg = Release|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Release|x86.Build.0 = Release|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.z3apidebug|.NET.ActiveCfg = Release|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.z3apidebug|Any CPU.ActiveCfg = Release|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.z3apidebug|Mixed Platforms.ActiveCfg = Release|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.z3apidebug|Mixed Platforms.Build.0 = Release|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.z3apidebug|x86.ActiveCfg = Release|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.z3apidebug|x86.Build.0 = Release|x86
{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.Checked|.NET.ActiveCfg = Checked|Any CPU
{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.Checked|Any CPU.ActiveCfg = Checked|Any CPU
{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.Checked|Any CPU.Build.0 = Checked|Any CPU
@@ -333,31 +280,55 @@ Global {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
- {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU
- {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Checked|Mixed Platforms.Build.0 = Checked|Any CPU
- {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Checked|x86.ActiveCfg = Checked|Any CPU
- {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Debug|.NET.ActiveCfg = Debug|Any CPU
- {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
- {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Debug|Any CPU.Build.0 = Debug|Any CPU
- {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
- {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
- {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Debug|x86.ActiveCfg = Debug|Any CPU
- {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Release|.NET.ActiveCfg = Release|Any CPU
- {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Release|Any CPU.ActiveCfg = Release|Any CPU
- {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Release|Any CPU.Build.0 = Release|Any CPU
- {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
- {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Release|Mixed Platforms.Build.0 = Release|Any CPU
- {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Release|x86.ActiveCfg = Release|Any CPU
- {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|.NET.ActiveCfg = Release|Any CPU
- {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|Any CPU.ActiveCfg = Release|Any CPU
- {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|Any CPU.Build.0 = Release|Any CPU
- {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
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Checked|.NET.ActiveCfg = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Checked|Any CPU.ActiveCfg = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Checked|Any CPU.Build.0 = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Checked|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Checked|Mixed Platforms.Build.0 = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Checked|x86.ActiveCfg = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Debug|.NET.ActiveCfg = Debug|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Debug|Any CPU.Build.0 = Debug|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Debug|x86.ActiveCfg = Debug|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Release|.NET.ActiveCfg = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Release|Any CPU.Build.0 = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Release|Mixed Platforms.Build.0 = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Release|x86.ActiveCfg = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.z3apidebug|.NET.ActiveCfg = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.z3apidebug|Any CPU.ActiveCfg = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.z3apidebug|Any CPU.Build.0 = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.z3apidebug|x86.ActiveCfg = Release|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
+ {B230A69C-C466-4065-B9C1-84D80E76D802}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU
+ {B230A69C-C466-4065-B9C1-84D80E76D802}.Checked|Mixed Platforms.Build.0 = Checked|Any CPU
+ {B230A69C-C466-4065-B9C1-84D80E76D802}.Checked|x86.ActiveCfg = Checked|Any CPU
+ {B230A69C-C466-4065-B9C1-84D80E76D802}.Debug|.NET.ActiveCfg = Debug|Any CPU
+ {B230A69C-C466-4065-B9C1-84D80E76D802}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {B230A69C-C466-4065-B9C1-84D80E76D802}.Debug|Any CPU.Build.0 = Debug|Any CPU
+ {B230A69C-C466-4065-B9C1-84D80E76D802}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
+ {B230A69C-C466-4065-B9C1-84D80E76D802}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
+ {B230A69C-C466-4065-B9C1-84D80E76D802}.Debug|x86.ActiveCfg = Debug|Any CPU
+ {B230A69C-C466-4065-B9C1-84D80E76D802}.Release|.NET.ActiveCfg = Release|Any CPU
+ {B230A69C-C466-4065-B9C1-84D80E76D802}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {B230A69C-C466-4065-B9C1-84D80E76D802}.Release|Any CPU.Build.0 = Release|Any CPU
+ {B230A69C-C466-4065-B9C1-84D80E76D802}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {B230A69C-C466-4065-B9C1-84D80E76D802}.Release|Mixed Platforms.Build.0 = Release|Any CPU
+ {B230A69C-C466-4065-B9C1-84D80E76D802}.Release|x86.ActiveCfg = Release|Any CPU
+ {B230A69C-C466-4065-B9C1-84D80E76D802}.z3apidebug|.NET.ActiveCfg = z3apidebug|Any CPU
+ {B230A69C-C466-4065-B9C1-84D80E76D802}.z3apidebug|Any CPU.ActiveCfg = z3apidebug|Any CPU
+ {B230A69C-C466-4065-B9C1-84D80E76D802}.z3apidebug|Any CPU.Build.0 = z3apidebug|Any CPU
+ {B230A69C-C466-4065-B9C1-84D80E76D802}.z3apidebug|Mixed Platforms.ActiveCfg = Debug|Any CPU
+ {B230A69C-C466-4065-B9C1-84D80E76D802}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU
+ {B230A69C-C466-4065-B9C1-84D80E76D802}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU
+ {B230A69C-C466-4065-B9C1-84D80E76D802}.z3apidebug|x86.Build.0 = z3apidebug|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
@@ -383,54 +354,58 @@ Global {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
- {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Checked|.NET.ActiveCfg = Release|Any CPU
- {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Checked|Any CPU.ActiveCfg = Release|Any CPU
- {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Checked|Any CPU.Build.0 = Release|Any CPU
- {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Checked|Mixed Platforms.ActiveCfg = Release|Any CPU
- {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Checked|Mixed Platforms.Build.0 = Release|Any CPU
- {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Checked|x86.ActiveCfg = Release|Any CPU
- {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Debug|.NET.ActiveCfg = Debug|Any CPU
- {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
- {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Debug|Any CPU.Build.0 = Debug|Any CPU
- {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
- {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
- {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Debug|x86.ActiveCfg = Debug|Any CPU
- {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Release|.NET.ActiveCfg = Release|Any CPU
- {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Release|Any CPU.ActiveCfg = Release|Any CPU
- {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Release|Any CPU.Build.0 = Release|Any CPU
- {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
- {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Release|Mixed Platforms.Build.0 = Release|Any CPU
- {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Release|x86.ActiveCfg = Release|Any CPU
- {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.z3apidebug|.NET.ActiveCfg = Release|Any CPU
- {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.z3apidebug|Any CPU.ActiveCfg = Release|Any CPU
- {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.z3apidebug|Any CPU.Build.0 = Release|Any CPU
- {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU
- {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU
- {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.z3apidebug|x86.ActiveCfg = Release|Any CPU
- {884386A3-58E9-40BB-A273-B24976775553}.Checked|.NET.ActiveCfg = Release|Any CPU
- {884386A3-58E9-40BB-A273-B24976775553}.Checked|Any CPU.ActiveCfg = Release|Any CPU
- {884386A3-58E9-40BB-A273-B24976775553}.Checked|Any CPU.Build.0 = Release|Any CPU
- {884386A3-58E9-40BB-A273-B24976775553}.Checked|Mixed Platforms.ActiveCfg = Release|Any CPU
- {884386A3-58E9-40BB-A273-B24976775553}.Checked|Mixed Platforms.Build.0 = Release|Any CPU
- {884386A3-58E9-40BB-A273-B24976775553}.Checked|x86.ActiveCfg = Release|Any CPU
- {884386A3-58E9-40BB-A273-B24976775553}.Debug|.NET.ActiveCfg = Debug|Any CPU
- {884386A3-58E9-40BB-A273-B24976775553}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
- {884386A3-58E9-40BB-A273-B24976775553}.Debug|Any CPU.Build.0 = Debug|Any CPU
- {884386A3-58E9-40BB-A273-B24976775553}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
- {884386A3-58E9-40BB-A273-B24976775553}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
- {884386A3-58E9-40BB-A273-B24976775553}.Debug|x86.ActiveCfg = Debug|Any CPU
- {884386A3-58E9-40BB-A273-B24976775553}.Release|.NET.ActiveCfg = Release|Any CPU
- {884386A3-58E9-40BB-A273-B24976775553}.Release|Any CPU.ActiveCfg = Release|Any CPU
- {884386A3-58E9-40BB-A273-B24976775553}.Release|Any CPU.Build.0 = Release|Any CPU
- {884386A3-58E9-40BB-A273-B24976775553}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
- {884386A3-58E9-40BB-A273-B24976775553}.Release|Mixed Platforms.Build.0 = Release|Any CPU
- {884386A3-58E9-40BB-A273-B24976775553}.Release|x86.ActiveCfg = Release|Any CPU
- {884386A3-58E9-40BB-A273-B24976775553}.z3apidebug|.NET.ActiveCfg = Release|Any CPU
- {884386A3-58E9-40BB-A273-B24976775553}.z3apidebug|Any CPU.ActiveCfg = Release|Any CPU
- {884386A3-58E9-40BB-A273-B24976775553}.z3apidebug|Any CPU.Build.0 = Release|Any CPU
- {884386A3-58E9-40BB-A273-B24976775553}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU
- {884386A3-58E9-40BB-A273-B24976775553}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU
- {884386A3-58E9-40BB-A273-B24976775553}.z3apidebug|x86.ActiveCfg = Release|Any CPU
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Checked|.NET.ActiveCfg = Checked|Any CPU
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Checked|Any CPU.ActiveCfg = Checked|Any CPU
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Checked|Any CPU.Build.0 = Checked|Any CPU
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Checked|Mixed Platforms.Build.0 = Checked|Any CPU
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Checked|x86.ActiveCfg = Checked|Any CPU
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Debug|.NET.ActiveCfg = Debug|Any CPU
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Debug|.NET.Build.0 = Debug|Any CPU
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Debug|Any CPU.Build.0 = Debug|Any CPU
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Debug|x86.ActiveCfg = Debug|Any CPU
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Release|.NET.ActiveCfg = Release|Any CPU
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Release|Any CPU.Build.0 = Release|Any CPU
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Release|Mixed Platforms.Build.0 = Release|Any CPU
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Release|x86.ActiveCfg = Release|Any CPU
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.z3apidebug|.NET.ActiveCfg = z3apidebug|Any CPU
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.z3apidebug|Any CPU.ActiveCfg = z3apidebug|Any CPU
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.z3apidebug|Any CPU.Build.0 = z3apidebug|Any CPU
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.z3apidebug|Mixed Platforms.ActiveCfg = Debug|Any CPU
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.z3apidebug|x86.ActiveCfg = z3apidebug|x86
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.z3apidebug|x86.Build.0 = z3apidebug|x86
+ {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
+ {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU
+ {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Checked|Mixed Platforms.Build.0 = Checked|Any CPU
+ {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Checked|x86.ActiveCfg = Checked|Any CPU
+ {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Debug|.NET.ActiveCfg = Debug|Any CPU
+ {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Debug|.NET.Build.0 = Debug|Any CPU
+ {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Debug|Any CPU.Build.0 = Debug|Any CPU
+ {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
+ {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
+ {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Debug|x86.ActiveCfg = Debug|Any CPU
+ {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Release|.NET.ActiveCfg = Release|Any CPU
+ {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Release|Any CPU.Build.0 = Release|Any CPU
+ {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Release|Mixed Platforms.Build.0 = Release|Any CPU
+ {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Release|x86.ActiveCfg = Release|Any CPU
+ {E1F10180-C7B9-4147-B51F-FA1B701966DC}.z3apidebug|.NET.ActiveCfg = z3apidebug|Any CPU
+ {E1F10180-C7B9-4147-B51F-FA1B701966DC}.z3apidebug|Any CPU.ActiveCfg = z3apidebug|Any CPU
+ {E1F10180-C7B9-4147-B51F-FA1B701966DC}.z3apidebug|Any CPU.Build.0 = z3apidebug|Any CPU
+ {E1F10180-C7B9-4147-B51F-FA1B701966DC}.z3apidebug|Mixed Platforms.ActiveCfg = Debug|Any CPU
+ {E1F10180-C7B9-4147-B51F-FA1B701966DC}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU
+ {E1F10180-C7B9-4147-B51F-FA1B701966DC}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU
+ {E1F10180-C7B9-4147-B51F-FA1B701966DC}.z3apidebug|x86.Build.0 = z3apidebug|Any CPU
{EAA5EB79-D475-4601-A59B-825C191CD25F}.Checked|.NET.ActiveCfg = Release|Any CPU
{EAA5EB79-D475-4601-A59B-825C191CD25F}.Checked|Any CPU.ActiveCfg = Release|Any CPU
{EAA5EB79-D475-4601-A59B-825C191CD25F}.Checked|Any CPU.Build.0 = Release|Any CPU
@@ -455,11 +430,66 @@ Global {EAA5EB79-D475-4601-A59B-825C191CD25F}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU
{EAA5EB79-D475-4601-A59B-825C191CD25F}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU
{EAA5EB79-D475-4601-A59B-825C191CD25F}.z3apidebug|x86.ActiveCfg = Release|Any CPU
- EndGlobalSection
- GlobalSection(SolutionProperties) = preSolution
- HideSolutionNode = FALSE
+ {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
+ {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU
+ {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Checked|Mixed Platforms.Build.0 = Checked|Any CPU
+ {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Checked|x86.ActiveCfg = Checked|Any CPU
+ {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Debug|.NET.ActiveCfg = Debug|Any CPU
+ {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Debug|Any CPU.Build.0 = Debug|Any CPU
+ {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
+ {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
+ {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Debug|x86.ActiveCfg = Debug|Any CPU
+ {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Release|.NET.ActiveCfg = Release|Any CPU
+ {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Release|Any CPU.Build.0 = Release|Any CPU
+ {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Release|Mixed Platforms.Build.0 = Release|Any CPU
+ {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Release|x86.ActiveCfg = Release|Any CPU
+ {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|.NET.ActiveCfg = Release|Any CPU
+ {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|Any CPU.ActiveCfg = Release|Any CPU
+ {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|Any CPU.Build.0 = Release|Any CPU
+ {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
EndGlobalSection
GlobalSection(NestedProjects) = preSolution
{9B163AA3-36BC-4AFB-88AB-79BC9E97E401} = {B758C1E3-824A-439F-AA2F-0BA1143E8C8D}
EndGlobalSection
+ GlobalSection(MonoDevelopProperties) = preSolution
+ StartupItem = Provers\SMTLib\SMTLib.csproj
+ Policies = $0
+ $0.DotNetNamingPolicy = $1
+ $1.DirectoryNamespaceAssociation = None
+ $1.ResourceNamePolicy = FileFormatDefault
+ $0.TextStylePolicy = $2
+ $2.FileWidth = 120
+ $2.TabWidth = 2
+ $2.IndentWidth = 2
+ $2.inheritsSet = Mono
+ $2.inheritsScope = text/plain
+ $2.scope = text/x-csharp
+ $0.CSharpFormattingPolicy = $3
+ $3.ElseIfNewLinePlacement = SameLine
+ $3.AfterDelegateDeclarationParameterComma = True
+ $3.inheritsSet = Mono
+ $3.inheritsScope = text/x-csharp
+ $3.scope = text/x-csharp
+ $0.TextStylePolicy = $4
+ $4.FileWidth = 120
+ $4.TabWidth = 2
+ $4.IndentWidth = 2
+ $4.inheritsSet = Mono
+ $4.inheritsScope = text/plain
+ $4.scope = text/plain
+ $0.StandardHeader = $5
+ $5.Text =
+ $5.IncludeInNewFiles = True
+ EndGlobalSection
+ GlobalSection(SolutionProperties) = preSolution
+ HideSolutionNode = FALSE
+ EndGlobalSection
EndGlobal
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 a9bd25ee..a1a4d740 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -411,6 +411,7 @@ namespace Microsoft.Boogie { public bool SimplifyLogFileAppend = false;
public bool SoundnessSmokeTest = false;
public string Z3ExecutablePath = null;
+ public string CVC4ExecutablePath = null;
public enum ProverWarnings {
None,
@@ -1268,6 +1269,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)) {
@@ -1843,6 +1850,10 @@ namespace Microsoft.Boogie { 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 06d68dba..e4840d1d 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" />
@@ -101,7 +103,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..b9a2dfcf 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..40fd3c9a --- /dev/null +++ b/Source/Model/ModelParser.cs @@ -0,0 +1,755 @@ +//----------------------------------------------------------------------------- +// +// 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; + } + + 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 (); + + int occurrences = 0; + + foreach (string tok in tokens) { + if (tok == "_ufmt_1") + occurrences++; + } + + for (; ;) { + index++; + + if (tokens [index] == "=") { + index += 2; + + if (tokens [index] == "(") { + while (tokens [index] != ")") + index++; + args.Add (GetValue (index - 1)); + } else { + args.Add (GetValue (index)); + } + } + + if ((args.Count > 0 && args.Count % arity == 0) || + (results.Count > 0 && occurrences <= 2 && occurrences > 0)) { + index += 2; + + 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++) { + if (occurrences > 2) { + for (int r = 0; r < arity; r++) { + output.Add (args [i]); + i++; + } + } else if (occurrences > 0) { + if (arity == 1) { + output.Add (args [i]); + i++; + } else { + output.Add (args [0]); + + for (int r = 1; r < arity; r++) { + i++; + output.Add (args [i]); + } + } + } else { + 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>[] 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; + } + + 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 "Array": + ParseArrayExpr (); + break; + + case "ite": + ParseIteExpr (); + break; + + case "_ufmt_1": + case "x!1": + output.Add ("{"); + output.Add (" "); + index++; + 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 2e612aa1..09dce05f 100644 --- a/Source/ModelViewer/Main.cs +++ b/Source/ModelViewer/Main.cs @@ -99,7 +99,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();
}
modelId = setModelIdTo;
diff --git a/Source/ModelViewer/ModelViewer.csproj b/Source/ModelViewer/ModelViewer.csproj index ae46767b..49965d5e 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>
<ItemGroup>
<Reference Include="System" />
@@ -123,6 +125,7 @@ <DependentUpon>Main.cs</DependentUpon>
</Compile>
<Compile Include="..\Model\Model.cs" />
+ <Compile Include="..\Model\ModelParser.cs" />
<Compile Include="Namer.cs" />
<Compile Include="Program.cs" />
<Compile Include="Properties\AssemblyInfo.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..815e5a45 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -8,6 +8,7 @@ using System.Collections; using System.Collections.Generic;
using System.Threading;
using System.IO;
+
//using ExternalProver;
using System.Linq;
using System.Diagnostics;
@@ -18,555 +19,509 @@ using Microsoft.Boogie.VCExprAST; using Microsoft.Boogie.Clustering;
using Microsoft.Boogie.TypeErasure;
using System.Text;
-
using RPFP = Microsoft.Boogie.RPFP;
namespace Microsoft.Boogie.SMTLib
{
- public class SMTLibProcessTheoremProver : ProverInterface
- {
- private readonly SMTLibProverContext ctx;
- private readonly VCExpressionGenerator gen;
- private readonly SMTLibProverOptions options;
- private bool usingUnsatCore;
- private RPFP rpfp = null;
-
- [ContractInvariantMethod]
- void ObjectInvariant()
- {
- Contract.Invariant(ctx != null);
- Contract.Invariant(AxBuilder != null);
- Contract.Invariant(Namer != null);
- Contract.Invariant(DeclCollector != null);
- Contract.Invariant(cce.NonNullElements(Axioms));
- Contract.Invariant(cce.NonNullElements(TypeDecls));
- Contract.Invariant(_backgroundPredicates != null);
-
- }
-
-
- [NotDelayed]
- public SMTLibProcessTheoremProver(ProverOptions options, VCExpressionGenerator gen,
- SMTLibProverContext ctx)
- {
- Contract.Requires(options != null);
- Contract.Requires(gen != null);
- Contract.Requires(ctx != null);
- InitializeGlobalInformation("UnivBackPred2.smt2");
-
- this.options = (SMTLibProverOptions)options;
- this.ctx = ctx;
- this.gen = gen;
- this.usingUnsatCore = false;
-
- SetupAxiomBuilder(gen);
-
- Namer = new SMTLibNamer();
- ctx.parent = this;
- this.DeclCollector = new TypeDeclCollector((SMTLibProverOptions)options, Namer);
-
- SetupProcess();
-
- if (CommandLineOptions.Clo.StratifiedInlining > 0 || CommandLineOptions.Clo.ContractInfer)
- {
- // Prepare for ApiChecker usage
- if (options.LogFilename != null && currentLogFile == null)
- {
- currentLogFile = OpenOutputFile("");
- }
- if (CommandLineOptions.Clo.ContractInfer)
- {
- SendThisVC("(set-option :produce-unsat-cores true)");
- this.usingUnsatCore = true;
- }
- PrepareCommon();
- }
- }
-
- private void SetupAxiomBuilder(VCExpressionGenerator gen)
- {
- switch (CommandLineOptions.Clo.TypeEncodingMethod)
- {
- case CommandLineOptions.TypeEncoding.Arguments:
- AxBuilder = new TypeAxiomBuilderArguments(gen);
- AxBuilder.Setup();
- break;
- case CommandLineOptions.TypeEncoding.Monomorphic:
- AxBuilder = new TypeAxiomBuilderPremisses(gen);
- break;
- default:
- AxBuilder = new TypeAxiomBuilderPremisses(gen);
- AxBuilder.Setup();
- break;
- }
- }
-
- ProcessStartInfo ComputeProcessStartInfo()
- {
- var path = this.options.ProverPath;
- switch (options.Solver) {
- case SolverKind.Z3:
- 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");
- default:
- Debug.Assert(false);
- return null;
- }
- }
-
- void SetupProcess()
- {
- if (Process != null) return;
-
- var psi = ComputeProcessStartInfo();
- Process = new SMTLibProcess(psi, this.options);
- Process.ErrorHandler += this.HandleProverError;
- }
-
-
- void PossiblyRestart()
- {
- if (Process != null && Process.NeedsRestart) {
- Process.Close();
- Process = null;
- SetupProcess();
- Process.Send(common.ToString());
- }
- }
-
- public override ProverContext Context
- {
- get
- {
- Contract.Ensures(Contract.Result<ProverContext>() != null);
-
- return ctx;
- }
- }
-
- internal TypeAxiomBuilder AxBuilder { get; private set; }
- internal readonly UniqueNamer Namer;
- readonly TypeDeclCollector DeclCollector;
- SMTLibProcess Process;
- readonly List<string> proverErrors = new List<string>();
- readonly List<string> proverWarnings = new List<string>();
- readonly StringBuilder common = new StringBuilder();
- TextWriter currentLogFile;
- volatile ErrorHandler currentErrorHandler;
-
- private void FeedTypeDeclsToProver()
- {
- foreach (string s in DeclCollector.GetNewDeclarations()) {
- Contract.Assert(s != null);
- AddTypeDecl(s);
- }
- }
-
- private string Sanitize(string msg)
- {
- var idx = msg.IndexOf('\n');
- if (idx > 0)
- msg = msg.Replace("\r", "").Replace("\n", "\r\n");
- return msg;
- }
-
- private void SendCommon(string s)
- {
- Send(s, true);
- }
-
- private void SendThisVC(string s)
- {
- Send(s, false);
- }
-
- private void Send(string s, bool isCommon)
- {
- s = Sanitize(s);
-
- if (isCommon)
- common.Append(s).Append("\r\n");
-
- if (Process != null)
- Process.Send(s);
- if (currentLogFile != null)
- currentLogFile.WriteLine(s);
- }
-
- private void FindDependentTypes(Type type, List<CtorType> dependentTypes)
- {
- MapType mapType = type as MapType;
- if (mapType != null)
- {
- foreach (Type t in mapType.Arguments)
- {
- FindDependentTypes(t, dependentTypes);
- }
- FindDependentTypes(mapType.Result, dependentTypes);
- }
- CtorType ctorType = type as CtorType;
- if (ctorType != null && ctx.KnownDatatypeConstructors.ContainsKey(ctorType))
- {
- dependentTypes.Add(ctorType);
- }
- }
-
- private void PrepareCommon()
- {
- if (common.Length == 0)
- {
- SendCommon("(set-option :print-success false)");
- SendCommon("(set-info :smt-lib-version 2.0)");
- if (options.ProduceModel())
- SendCommon("(set-option :produce-models true)");
- foreach (var opt in options.SmtOptions)
- {
- SendCommon("(set-option :" + opt.Option + " " + opt.Value + ")");
- }
-
- if (!string.IsNullOrEmpty(options.Logic))
- {
- SendCommon("(set-logic " + options.Logic + ")");
- }
-
- SendCommon("; done setting options\n");
- SendCommon(_backgroundPredicates);
-
- if (options.UseTickleBool)
- {
- SendCommon("(declare-fun tickleBool (Bool) Bool)");
- SendCommon("(assert (and (tickleBool true) (tickleBool false)))");
- }
-
- if (ctx.KnownDatatypeConstructors.Count > 0)
- {
- GraphUtil.Graph<CtorType> dependencyGraph = new GraphUtil.Graph<CtorType>();
- foreach (CtorType datatype in ctx.KnownDatatypeConstructors.Keys)
- {
- dependencyGraph.AddSource(datatype);
- foreach (Function f in ctx.KnownDatatypeConstructors[datatype])
- {
- List<CtorType> dependentTypes = new List<CtorType>();
- foreach (Variable v in f.InParams)
- {
- FindDependentTypes(v.TypedIdent.Type, dependentTypes);
- }
- foreach (CtorType result in dependentTypes)
- {
- dependencyGraph.AddEdge(datatype, result);
- }
- }
- }
- GraphUtil.StronglyConnectedComponents<CtorType> sccs = new GraphUtil.StronglyConnectedComponents<CtorType>(dependencyGraph.Nodes, dependencyGraph.Predecessors, dependencyGraph.Successors);
- sccs.Compute();
- foreach (GraphUtil.SCC<CtorType> scc in sccs)
- {
- string datatypeString = "";
- foreach (CtorType datatype in scc)
- {
- datatypeString += "(" + SMTLibExprLineariser.TypeToString(datatype) + " ";
- foreach (Function f in ctx.KnownDatatypeConstructors[datatype])
- {
- string quotedConstructorName = Namer.GetQuotedName(f, f.Name);
- if (f.InParams.Length == 0)
- {
- datatypeString += quotedConstructorName + " ";
- }
- else
- {
- datatypeString += "(" + quotedConstructorName + " ";
- foreach (Variable v in f.InParams)
- {
- string quotedSelectorName = Namer.GetQuotedName(v, v.Name + "#" + f.Name);
- datatypeString += "(" + quotedSelectorName + " " + DeclCollector.TypeToStringReg(v.TypedIdent.Type) + ") ";
- }
- datatypeString += ") ";
- }
- }
- datatypeString += ") ";
- }
- List<string> decls = DeclCollector.GetNewDeclarations();
- foreach (string decl in decls)
- {
- SendCommon(decl);
- }
- SendCommon("(declare-datatypes () (" + datatypeString + "))");
- }
- }
- }
-
- if (!AxiomsAreSetup)
- {
- var axioms = ctx.Axioms;
- var nary = axioms as VCExprNAry;
- if (nary != null && nary.Op == VCExpressionGenerator.AndOp)
- foreach (var expr in nary.UniformArguments)
- {
- var str = VCExpr2String(expr, -1);
- if (str != "true")
- AddAxiom(str);
- }
- else
- AddAxiom(VCExpr2String(axioms, -1));
- AxiomsAreSetup = true;
- }
- }
-
- public override int FlushAxiomsToTheoremProver()
- {
- // we feed the axioms when begincheck is called.
- return 0;
- }
-
- private void FlushAxioms()
- {
- TypeDecls.Iter(SendCommon);
- TypeDecls.Clear();
- foreach (string s in Axioms) {
- Contract.Assert(s != null);
- if (s != "true")
- SendCommon("(assert " + s + ")");
- }
- Axioms.Clear();
- //FlushPushedAssertions();
- }
-
- private void CloseLogFile()
- {
- if (currentLogFile != null) {
- currentLogFile.Close();
- currentLogFile = null;
- }
- }
-
- private void FlushLogFile()
- {
- if (currentLogFile != null) {
- currentLogFile.Flush();
- }
- }
-
- public override void Close()
- {
- base.Close();
- CloseLogFile();
- if (Process != null)
- Process.Close();
- }
-
- public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler)
- {
- //Contract.Requires(descriptiveName != null);
- //Contract.Requires(vc != null);
- //Contract.Requires(handler != null);
- rpfp = null;
-
- if (options.SeparateLogFiles) CloseLogFile(); // shouldn't really happen
-
- if (options.LogFilename != null && currentLogFile == null)
- {
- currentLogFile = OpenOutputFile(descriptiveName);
- currentLogFile.Write(common.ToString());
- }
-
- PrepareCommon();
- string vcString = "(assert (not\n" + VCExpr2String(vc, 1) + "\n))";
- FlushAxioms();
-
- PossiblyRestart();
-
- SendThisVC("(push 1)");
- SendThisVC("(set-info :boogie-vc-id " + SMTLibNamer.QuoteId(descriptiveName) + ")");
- SendThisVC(vcString);
- FlushLogFile();
-
- if (Process != null) {
- Process.PingPong(); // flush any errors
-
- if (Process.Inspector != null)
- Process.Inspector.NewProblem(descriptiveName, vc, handler);
- }
-
- SendThisVC("(check-sat)");
- FlushLogFile();
- }
-
- public override void Reset()
- {
- SendThisVC("(reset)");
+ public class SMTLibProcessTheoremProver : ProverInterface
+ {
+ private readonly SMTLibProverContext ctx;
+ private readonly VCExpressionGenerator gen;
+ private readonly SMTLibProverOptions options;
+ private bool usingUnsatCore;
+ private RPFP rpfp = null;
+
+ [ContractInvariantMethod]
+ void ObjectInvariant ()
+ {
+ Contract.Invariant (ctx != null);
+ Contract.Invariant (AxBuilder != null);
+ Contract.Invariant (Namer != null);
+ Contract.Invariant (DeclCollector != null);
+ Contract.Invariant (cce.NonNullElements (Axioms));
+ Contract.Invariant (cce.NonNullElements (TypeDecls));
+ Contract.Invariant (_backgroundPredicates != null);
+
+ }
+
+ [NotDelayed]
+ public SMTLibProcessTheoremProver (ProverOptions options, VCExpressionGenerator gen,
+ SMTLibProverContext ctx)
+ {
+ Contract.Requires (options != null);
+ Contract.Requires (gen != null);
+ Contract.Requires (ctx != null);
+ InitializeGlobalInformation ("UnivBackPred2.smt2");
+
+ this.options = (SMTLibProverOptions)options;
+ this.ctx = ctx;
+ this.gen = gen;
+ this.usingUnsatCore = false;
+
+ SetupAxiomBuilder (gen);
+
+ Namer = new SMTLibNamer ();
+ ctx.parent = this;
+ this.DeclCollector = new TypeDeclCollector ((SMTLibProverOptions)options, Namer);
+
+ SetupProcess ();
+
+ if (CommandLineOptions.Clo.StratifiedInlining > 0 || CommandLineOptions.Clo.ContractInfer) {
+ // Prepare for ApiChecker usage
+ if (options.LogFilename != null && currentLogFile == null) {
+ currentLogFile = OpenOutputFile ("");
+ }
+ if (CommandLineOptions.Clo.ContractInfer) {
+ SendThisVC ("(set-option :produce-unsat-cores true)");
+ this.usingUnsatCore = true;
+ }
+ PrepareCommon ();
+ }
+ }
+
+ private void SetupAxiomBuilder (VCExpressionGenerator gen)
+ {
+ switch (CommandLineOptions.Clo.TypeEncodingMethod) {
+ case CommandLineOptions.TypeEncoding.Arguments:
+ AxBuilder = new TypeAxiomBuilderArguments (gen);
+ AxBuilder.Setup ();
+ break;
+ case CommandLineOptions.TypeEncoding.Monomorphic:
+ AxBuilder = new TypeAxiomBuilderPremisses (gen);
+ break;
+ default:
+ AxBuilder = new TypeAxiomBuilderPremisses (gen);
+ AxBuilder.Setup ();
+ break;
+ }
+ }
+
+ ProcessStartInfo ComputeProcessStartInfo ()
+ {
+ var path = this.options.ProverPath;
+ switch (options.Solver) {
+ case SolverKind.Z3:
+ if (path == null)
+ path = Z3.ExecutablePath ();
+ return SMTLibProcess.ComputerProcessStartInfo (path, "AUTO_CONFIG=false -smt2 -in");
+ case SolverKind.CVC4:
+ if (path == null)
+ path = "cvc4";
+ return SMTLibProcess.ComputerProcessStartInfo (path, "--lang=smt --no-strict-parsing --no-condense-function-values --incremental");
+ default:
+ Debug.Assert (false);
+ return null;
+ }
+ }
+
+ void SetupProcess ()
+ {
+ if (Process != null)
+ return;
+
+ var psi = ComputeProcessStartInfo ();
+ Process = new SMTLibProcess (psi, this.options);
+ Process.ErrorHandler += this.HandleProverError;
+ }
+
+ void PossiblyRestart ()
+ {
+ if (Process != null && Process.NeedsRestart) {
+ Process.Close ();
+ Process = null;
+ SetupProcess ();
+ Process.Send (common.ToString ());
+ }
+ }
+
+ public override ProverContext Context {
+ get {
+ Contract.Ensures (Contract.Result<ProverContext> () != null);
+
+ return ctx;
+ }
+ }
+
+ internal TypeAxiomBuilder AxBuilder { get; private set; }
+
+ internal readonly UniqueNamer Namer;
+ readonly TypeDeclCollector DeclCollector;
+ SMTLibProcess Process;
+ readonly List<string> proverErrors = new List<string> ();
+ readonly List<string> proverWarnings = new List<string> ();
+ readonly StringBuilder common = new StringBuilder ();
+ TextWriter currentLogFile;
+ volatile ErrorHandler currentErrorHandler;
+
+ private void FeedTypeDeclsToProver ()
+ {
+ foreach (string s in DeclCollector.GetNewDeclarations()) {
+ Contract.Assert (s != null);
+ AddTypeDecl (s);
+ }
+ }
+
+ private string Sanitize (string msg)
+ {
+ var idx = msg.IndexOf ('\n');
+ if (idx > 0)
+ msg = msg.Replace ("\r", "").Replace ("\n", "\r\n");
+ return msg;
+ }
+
+ private void SendCommon (string s)
+ {
+ Send (s, true);
+ }
+
+ private void SendThisVC (string s)
+ {
+ Send (s, false);
+ }
+
+ private void Send (string s, bool isCommon)
+ {
+ s = Sanitize (s);
+
+ if (isCommon)
+ common.Append (s).Append ("\r\n");
+
+ if (Process != null)
+ Process.Send (s);
+ if (currentLogFile != null)
+ currentLogFile.WriteLine (s);
+ }
+
+ private void FindDependentTypes (Type type, List<CtorType> dependentTypes)
+ {
+ MapType mapType = type as MapType;
+ if (mapType != null) {
+ foreach (Type t in mapType.Arguments) {
+ FindDependentTypes (t, dependentTypes);
+ }
+ FindDependentTypes (mapType.Result, dependentTypes);
+ }
+ CtorType ctorType = type as CtorType;
+ if (ctorType != null && ctx.KnownDatatypeConstructors.ContainsKey (ctorType)) {
+ dependentTypes.Add (ctorType);
+ }
+ }
+
+ private void PrepareCommon ()
+ {
+ if (common.Length == 0) {
+ SendCommon ("(set-option :print-success false)");
+ SendCommon ("(set-info :smt-lib-version 2.0)");
+ if (options.ProduceModel ())
+ SendCommon ("(set-option :produce-models true)");
+ foreach (var opt in options.SmtOptions) {
+ SendCommon ("(set-option :" + opt.Option + " " + opt.Value + ")");
+ }
+
+ if (!string.IsNullOrEmpty (options.Logic)) {
+ SendCommon ("(set-logic " + options.Logic + ")");
+ }
+
+ SendCommon ("; done setting options\n");
+ SendCommon (_backgroundPredicates);
+
+ if (options.UseTickleBool) {
+ SendCommon ("(declare-fun tickleBool (Bool) Bool)");
+ SendCommon ("(assert (and (tickleBool true) (tickleBool false)))");
+ }
+
+ if (ctx.KnownDatatypeConstructors.Count > 0) {
+ GraphUtil.Graph<CtorType> dependencyGraph = new GraphUtil.Graph<CtorType> ();
+ foreach (CtorType datatype in ctx.KnownDatatypeConstructors.Keys) {
+ dependencyGraph.AddSource (datatype);
+ foreach (Function f in ctx.KnownDatatypeConstructors[datatype]) {
+ List<CtorType> dependentTypes = new List<CtorType> ();
+ foreach (Variable v in f.InParams) {
+ FindDependentTypes (v.TypedIdent.Type, dependentTypes);
+ }
+ foreach (CtorType result in dependentTypes) {
+ dependencyGraph.AddEdge (datatype, result);
+ }
+ }
+ }
+ GraphUtil.StronglyConnectedComponents<CtorType> sccs = new GraphUtil.StronglyConnectedComponents<CtorType> (dependencyGraph.Nodes, dependencyGraph.Predecessors, dependencyGraph.Successors);
+ sccs.Compute ();
+ foreach (GraphUtil.SCC<CtorType> scc in sccs) {
+ string datatypeString = "";
+ foreach (CtorType datatype in scc) {
+ datatypeString += "(" + SMTLibExprLineariser.TypeToString (datatype) + " ";
+ foreach (Function f in ctx.KnownDatatypeConstructors[datatype]) {
+ string quotedConstructorName = Namer.GetQuotedName (f, f.Name);
+ if (f.InParams.Length == 0) {
+ datatypeString += quotedConstructorName + " ";
+ } else {
+ datatypeString += "(" + quotedConstructorName + " ";
+ foreach (Variable v in f.InParams) {
+ string quotedSelectorName = Namer.GetQuotedName (v, v.Name + "#" + f.Name);
+ datatypeString += "(" + quotedSelectorName + " " + DeclCollector.TypeToStringReg (v.TypedIdent.Type) + ") ";
+ }
+ datatypeString += ") ";
+ }
+ }
+ datatypeString += ") ";
+ }
+ List<string> decls = DeclCollector.GetNewDeclarations ();
+ foreach (string decl in decls) {
+ SendCommon (decl);
+ }
+ SendCommon ("(declare-datatypes () (" + datatypeString + "))");
+ }
+ }
+ }
+
+ if (!AxiomsAreSetup) {
+ var axioms = ctx.Axioms;
+ var nary = axioms as VCExprNAry;
+ if (nary != null && nary.Op == VCExpressionGenerator.AndOp)
+ foreach (var expr in nary.UniformArguments) {
+ var str = VCExpr2String (expr, -1);
+ if (str != "true")
+ AddAxiom (str);
+ }
+ else
+ AddAxiom (VCExpr2String (axioms, -1));
+ AxiomsAreSetup = true;
+ }
+ }
+
+ public override int FlushAxiomsToTheoremProver ()
+ {
+ // we feed the axioms when begincheck is called.
+ return 0;
+ }
+
+ private void FlushAxioms ()
+ {
+ TypeDecls.Iter (SendCommon);
+ TypeDecls.Clear ();
+ foreach (string s in Axioms) {
+ Contract.Assert (s != null);
+ if (s != "true")
+ SendCommon ("(assert " + s + ")");
+ }
+ Axioms.Clear ();
+ //FlushPushedAssertions();
+ }
+
+ private void CloseLogFile ()
+ {
+ if (currentLogFile != null) {
+ currentLogFile.Close ();
+ currentLogFile = null;
+ }
+ }
+
+ private void FlushLogFile ()
+ {
+ if (currentLogFile != null) {
+ currentLogFile.Flush ();
+ }
+ }
+
+ public override void Close ()
+ {
+ base.Close ();
+ CloseLogFile ();
+ if (Process != null)
+ Process.Close ();
+ }
+
+ public override void BeginCheck (string descriptiveName, VCExpr vc, ErrorHandler handler)
+ {
+ //Contract.Requires(descriptiveName != null);
+ //Contract.Requires(vc != null);
+ //Contract.Requires(handler != null);
+ rpfp = null;
+
+ if (options.SeparateLogFiles)
+ CloseLogFile (); // shouldn't really happen
+
+ if (options.LogFilename != null && currentLogFile == null) {
+ currentLogFile = OpenOutputFile (descriptiveName);
+ currentLogFile.Write (common.ToString ());
+ }
+
+ PrepareCommon ();
+ string vcString = "(assert (not\n" + VCExpr2String (vc, 1) + "\n))";
+ FlushAxioms ();
+
+ PossiblyRestart ();
+
+ SendThisVC ("(push 1)");
+ SendThisVC ("(set-info :boogie-vc-id " + SMTLibNamer.QuoteId (descriptiveName) + ")");
+ SendThisVC (vcString);
+ FlushLogFile ();
+
+ if (Process != null) {
+ Process.PingPong (); // flush any errors
+
+ if (Process.Inspector != null)
+ Process.Inspector.NewProblem (descriptiveName, vc, handler);
+ }
+
+ SendThisVC ("(check-sat)");
+ FlushLogFile ();
+ }
+
+ public override void Reset ()
+ {
+ 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()
- {
- 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,
- Dictionary<int,Dictionary<string,string>> varSubst)
- {
- Dictionary<string, RPFP.Node> nmap = new Dictionary<string,RPFP.Node>();
- Dictionary<string, RPFP.Node> pmap = new Dictionary<string,RPFP.Node>();
-
- foreach(var node in rpfp.nodes)
- pmap.Add((node.Name as VCExprBoogieFunctionOp).Func.Name,node);
-
- RPFP.Node topnode = null;
- var lines = resp.Arguments;
-
- // last line of derivation is from query, skip it
- for (int i = 0; i < lines.Length-1; i++)
- {
- var line = lines[i];
- if (line.ArgCount != 6)
- {
- HandleProverError("bad derivation line from prover: " + line.ToString());
- return null;
- }
- var name = line[0];
- var conseq = line[1];
- var rule = line[2];
- var subst = line[3];
- var labs = line[4];
- var refs = line[5];
- var predName = conseq.Name;
- {
- string spacer = "@@"; // Hack! UniqueNamer is adding these and I can't stop it!
- int pos = predName.LastIndexOf(spacer);
- if (pos >= 0)
- predName = predName.Substring(0, pos);
- }
- RPFP.Node node = null;
- if (!pmap.TryGetValue(predName, out node))
- {
- HandleProverError("unknown predicate from prover: " + predName.ToString());
- return null;
- }
- RPFP.Node cexnode = rpfp.CloneNode(node);
- cexnode.map = node;
- nmap.Add(name.Name, cexnode);
- List<RPFP.Node> Chs = new List<RPFP.Node>();
-
- if (refs.Name != "ref")
- {
- HandleProverError("bad references from prover: " + refs.ToString());
- return null;
- }
- foreach (var c in refs.Arguments)
- {
- if (c.Name == "true")
- Chs.Add(null);
- else
- {
- RPFP.Node ch = null;
- if (!nmap.TryGetValue(c.Name, out ch))
- {
- HandleProverError("unknown reference from prover: " + c.ToString());
- return null;
- }
- Chs.Add(ch);
- }
- }
-
- if (!rule.Name.StartsWith("rule!"))
- {
- HandleProverError("bad rule name from prover: " + refs.ToString());
- return null;
- }
- int ruleNum = Convert.ToInt32(rule.Name.Substring(5)) - 1;
- if (ruleNum < 0 || ruleNum > rpfp.edges.Count)
- {
- HandleProverError("bad rule name from prover: " + refs.ToString());
- return null;
- }
- RPFP.Edge orig_edge = rpfp.edges[ruleNum];
- RPFP.Edge e = rpfp.CreateEdge(cexnode, orig_edge.F, Chs.ToArray());
- e.map = orig_edge;
- topnode = cexnode;
-
- if (labs.Name != "labels")
- {
- HandleProverError("bad labels from prover: " + labs.ToString());
- return null;
- }
- e.labels = new HashSet<string>();
- foreach (var l in labs.Arguments)
- e.labels.Add(l.Name);
-
- if (subst.Name != "subst")
- {
- HandleProverError("bad subst from prover: " + subst.ToString());
- return null;
- }
- Dictionary<string, string> dict = new Dictionary<string, string>();
- varSubst[e.number] = dict;
- foreach (var s in subst.Arguments)
- {
- if (s.Name != "=" || s.Arguments.Length != 2)
- {
- HandleProverError("bad equation from prover: " + s.ToString());
- return null;
- }
- string uniqueName = s.Arguments[0].Name;
- string spacer = "@@"; // Hack! UniqueNamer is adding these and I can't stop it!
- int pos = uniqueName.LastIndexOf(spacer);
- if (pos >= 0)
- uniqueName = uniqueName.Substring(0, pos);
- dict.Add(uniqueName, s.Arguments[1].ToString());
- }
-
- }
- if (topnode == null)
- {
- HandleProverError("empty derivation from prover: " + resp.ToString());
- }
- return topnode;
- }
-
- private Model SExprToModel(SExpr resp, ErrorHandler handler)
- {
- // 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));
- if (models == null || models.Count == 0)
- {
- HandleProverError("no model from prover: " + resp.ToString());
- }
- return models[0];
- }
-
- private string QuantifiedVCExpr2String(VCExpr x)
- {
- return VCExpr2String(x, 1);
+ if (0 < common.Length) {
+ var c = common.ToString ();
+ Process.Send (c);
+ if (currentLogFile != null) {
+ currentLogFile.WriteLine (c);
+ }
+ }
+ }
+ }
+
+ public override void FullReset ()
+ {
+ 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,
+ Dictionary<int,Dictionary<string,string>> varSubst)
+ {
+ Dictionary<string, RPFP.Node> nmap = new Dictionary<string,RPFP.Node> ();
+ Dictionary<string, RPFP.Node> pmap = new Dictionary<string,RPFP.Node> ();
+
+ foreach (var node in rpfp.nodes)
+ pmap.Add ((node.Name as VCExprBoogieFunctionOp).Func.Name, node);
+
+ RPFP.Node topnode = null;
+ var lines = resp.Arguments;
+
+ // last line of derivation is from query, skip it
+ for (int i = 0; i < lines.Length-1; i++) {
+ var line = lines [i];
+ if (line.ArgCount != 6) {
+ HandleProverError ("bad derivation line from prover: " + line.ToString ());
+ return null;
+ }
+ var name = line [0];
+ var conseq = line [1];
+ var rule = line [2];
+ var subst = line [3];
+ var labs = line [4];
+ var refs = line [5];
+ var predName = conseq.Name;
+ {
+ string spacer = "@@"; // Hack! UniqueNamer is adding these and I can't stop it!
+ int pos = predName.LastIndexOf (spacer);
+ if (pos >= 0)
+ predName = predName.Substring (0, pos);
+ }
+ RPFP.Node node = null;
+ if (!pmap.TryGetValue (predName, out node)) {
+ HandleProverError ("unknown predicate from prover: " + predName.ToString ());
+ return null;
+ }
+ RPFP.Node cexnode = rpfp.CloneNode (node);
+ cexnode.map = node;
+ nmap.Add (name.Name, cexnode);
+ List<RPFP.Node> Chs = new List<RPFP.Node> ();
+
+ if (refs.Name != "ref") {
+ HandleProverError ("bad references from prover: " + refs.ToString ());
+ return null;
+ }
+ foreach (var c in refs.Arguments) {
+ if (c.Name == "true")
+ Chs.Add (null);
+ else {
+ RPFP.Node ch = null;
+ if (!nmap.TryGetValue (c.Name, out ch)) {
+ HandleProverError ("unknown reference from prover: " + c.ToString ());
+ return null;
+ }
+ Chs.Add (ch);
+ }
+ }
+
+ if (!rule.Name.StartsWith ("rule!")) {
+ HandleProverError ("bad rule name from prover: " + refs.ToString ());
+ return null;
+ }
+ int ruleNum = Convert.ToInt32 (rule.Name.Substring (5)) - 1;
+ if (ruleNum < 0 || ruleNum > rpfp.edges.Count) {
+ HandleProverError ("bad rule name from prover: " + refs.ToString ());
+ return null;
+ }
+ RPFP.Edge orig_edge = rpfp.edges [ruleNum];
+ RPFP.Edge e = rpfp.CreateEdge (cexnode, orig_edge.F, Chs.ToArray ());
+ e.map = orig_edge;
+ topnode = cexnode;
+
+ if (labs.Name != "labels") {
+ HandleProverError ("bad labels from prover: " + labs.ToString ());
+ return null;
+ }
+ e.labels = new HashSet<string> ();
+ foreach (var l in labs.Arguments)
+ e.labels.Add (l.Name);
+
+ if (subst.Name != "subst") {
+ HandleProverError ("bad subst from prover: " + subst.ToString ());
+ return null;
+ }
+ Dictionary<string, string> dict = new Dictionary<string, string> ();
+ varSubst [e.number] = dict;
+ foreach (var s in subst.Arguments) {
+ if (s.Name != "=" || s.Arguments.Length != 2) {
+ HandleProverError ("bad equation from prover: " + s.ToString ());
+ return null;
+ }
+ string uniqueName = s.Arguments [0].Name;
+ string spacer = "@@"; // Hack! UniqueNamer is adding these and I can't stop it!
+ int pos = uniqueName.LastIndexOf (spacer);
+ if (pos >= 0)
+ uniqueName = uniqueName.Substring (0, pos);
+ dict.Add (uniqueName, s.Arguments [1].ToString ());
+ }
+
+ }
+ if (topnode == null) {
+ HandleProverError ("empty derivation from prover: " + resp.ToString ());
+ }
+ return topnode;
+ }
+
+ private Model SExprToModel (SExpr resp, ErrorHandler handler)
+ {
+ // 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), "");
+ if (models == null || models.Count == 0) {
+ HandleProverError ("no model from prover: " + resp.ToString ());
+ }
+ return models [0];
+ }
+
+ private string QuantifiedVCExpr2String (VCExpr x)
+ {
+ return VCExpr2String (x, 1);
#if false
if (!(x is VCExprQuantifier))
return VCExpr2String(x, 1);
@@ -594,122 +549,112 @@ namespace Microsoft.Boogie.SMTLib string res = wr.ToString();
return res;
#endif
- }
-
- public override Outcome CheckRPFP(string descriptiveName, RPFP _rpfp, ErrorHandler handler,
- out RPFP.Node cex,
- Dictionary<int,Dictionary<string,string>> varSubst)
- {
- //Contract.Requires(descriptiveName != null);
- //Contract.Requires(vc != null);
- //Contract.Requires(handler != null);
- rpfp = _rpfp;
- cex = null;
-
- if (options.SeparateLogFiles) CloseLogFile(); // shouldn't really happen
-
- if (options.LogFilename != null && currentLogFile == null)
- {
- currentLogFile = OpenOutputFile(descriptiveName);
- currentLogFile.Write(common.ToString());
- }
-
- Push();
- SendThisVC("(fixedpoint-push)");
- foreach (var node in rpfp.nodes)
- {
- DeclCollector.RegisterRelation((node.Name as VCExprBoogieFunctionOp).Func);
- }
-
- PrepareCommon();
-
- LineariserOptions.Default.LabelsBelowQuantifiers = true;
- List<string> ruleStrings = new List<string>();
- foreach (var edge in rpfp.edges)
- {
- string ruleString = "(rule " + QuantifiedVCExpr2String(rpfp.GetRule(edge)) + "\n)";
- ruleStrings.Add(ruleString);
- }
- string queryString = "(query " + QuantifiedVCExpr2String(rpfp.GetQuery()) + "\n :engine duality\n :print-certificate true\n";
+ }
+
+ public override Outcome CheckRPFP (string descriptiveName, RPFP _rpfp, ErrorHandler handler,
+ out RPFP.Node cex,
+ Dictionary<int,Dictionary<string,string>> varSubst)
+ {
+ //Contract.Requires(descriptiveName != null);
+ //Contract.Requires(vc != null);
+ //Contract.Requires(handler != null);
+ rpfp = _rpfp;
+ cex = null;
+
+ if (options.SeparateLogFiles)
+ CloseLogFile (); // shouldn't really happen
+
+ if (options.LogFilename != null && currentLogFile == null) {
+ currentLogFile = OpenOutputFile (descriptiveName);
+ currentLogFile.Write (common.ToString ());
+ }
+
+ Push ();
+ SendThisVC ("(fixedpoint-push)");
+ foreach (var node in rpfp.nodes) {
+ DeclCollector.RegisterRelation ((node.Name as VCExprBoogieFunctionOp).Func);
+ }
+
+ PrepareCommon ();
+
+ LineariserOptions.Default.LabelsBelowQuantifiers = true;
+ List<string> ruleStrings = new List<string> ();
+ foreach (var edge in rpfp.edges) {
+ string ruleString = "(rule " + QuantifiedVCExpr2String (rpfp.GetRule (edge)) + "\n)";
+ ruleStrings.Add (ruleString);
+ }
+ string queryString = "(query " + QuantifiedVCExpr2String (rpfp.GetQuery ()) + "\n :engine duality\n :print-certificate true\n";
#if true
- if (CommandLineOptions.Clo.StratifiedInlining != 0)
- queryString += " :stratified-inlining true\n";
- if (CommandLineOptions.Clo.RecursionBound > 0)
- queryString += " :recursion-bound " + Convert.ToString(CommandLineOptions.Clo.RecursionBound) + "\n";
+ if (CommandLineOptions.Clo.StratifiedInlining != 0)
+ queryString += " :stratified-inlining true\n";
+ if (CommandLineOptions.Clo.RecursionBound > 0)
+ queryString += " :recursion-bound " + Convert.ToString (CommandLineOptions.Clo.RecursionBound) + "\n";
#endif
- queryString += ")";
- LineariserOptions.Default.LabelsBelowQuantifiers = false;
- FlushAxioms();
+ queryString += ")";
+ LineariserOptions.Default.LabelsBelowQuantifiers = false;
+ FlushAxioms ();
- PossiblyRestart();
+ PossiblyRestart ();
- SendThisVC("(set-info :boogie-vc-id " + SMTLibNamer.QuoteId(descriptiveName) + ")");
- foreach(var rs in ruleStrings)
- SendThisVC(rs);
- FlushLogFile();
+ SendThisVC ("(set-info :boogie-vc-id " + SMTLibNamer.QuoteId (descriptiveName) + ")");
+ foreach (var rs in ruleStrings)
+ SendThisVC (rs);
+ FlushLogFile ();
- if (Process != null)
- {
- Process.PingPong(); // flush any errors
+ if (Process != null) {
+ Process.PingPong (); // flush any errors
#if false
// TODO: this is not going to work
if (Process.Inspector != null)
Process.Inspector.NewProblem(descriptiveName, vc, handler);
#endif
- }
+ }
- SendThisVC(queryString);
- FlushLogFile();
+ SendThisVC (queryString);
+ FlushLogFile ();
- var result = Outcome.Undetermined;
+ var result = Outcome.Undetermined;
- if (Process != null)
- {
+ if (Process != null) {
- var resp = Process.GetProverResponse();
+ var resp = Process.GetProverResponse ();
- switch (resp.Name)
- {
- case "unsat":
- result = Outcome.Valid;
- break;
- case "sat":
- result = Outcome.Invalid;
- break;
- case "unknown":
- result = Outcome.Invalid;
- break;
- default:
- HandleProverError("Unexpected prover response: " + resp.ToString());
- break;
- }
+ switch (resp.Name) {
+ case "unsat":
+ result = Outcome.Valid;
+ break;
+ case "sat":
+ result = Outcome.Invalid;
+ break;
+ case "unknown":
+ result = Outcome.Invalid;
+ break;
+ default:
+ HandleProverError ("Unexpected prover response: " + resp.ToString ());
+ break;
+ }
- switch (result)
- {
- case Outcome.Invalid:
- {
- resp = Process.GetProverResponse();
- if (resp.Name == "derivation")
- {
- cex = SExprToCex(resp, handler,varSubst);
- }
- else
- HandleProverError("Unexpected prover response: " + resp.ToString());
- resp = Process.GetProverResponse();
- if (resp.Name == "model")
- {
- var model = SExprToModel(resp, handler);
- cex.owner.SetBackgroundModel(model);
- }
- else
- HandleProverError("Unexpected prover response: " + resp.ToString());
- break;
- }
- default:
- break;
- }
+ switch (result) {
+ case Outcome.Invalid:
+ {
+ resp = Process.GetProverResponse ();
+ if (resp.Name == "derivation") {
+ cex = SExprToCex (resp, handler, varSubst);
+ } else
+ HandleProverError ("Unexpected prover response: " + resp.ToString ());
+ resp = Process.GetProverResponse ();
+ if (resp.Name == "model") {
+ var model = SExprToModel (resp, handler);
+ cex.owner.SetBackgroundModel (model);
+ } else
+ HandleProverError ("Unexpected prover response: " + resp.ToString ());
+ break;
+ }
+ default:
+ break;
+ }
#if false
while (true)
@@ -720,121 +665,121 @@ namespace Microsoft.Boogie.SMTLib HandleProverError("Unexpected prover response: " + resp.ToString());
}
#endif
- }
- SendThisVC("(fixedpoint-pop)");
- Pop();
- AxiomsAreSetup = false;
- return result;
- }
-
- private static HashSet<string> usedLogNames = new HashSet<string>();
-
- private TextWriter OpenOutputFile(string descriptiveName)
- {
- Contract.Requires(descriptiveName != null);
- Contract.Ensures(Contract.Result<TextWriter>() != null);
-
- string filename = options.LogFilename;
- filename = Helpers.SubstituteAtPROC(descriptiveName, cce.NonNull(filename));
- var curFilename = filename;
-
- lock (usedLogNames) {
- int n = 1;
- while (usedLogNames.Contains(curFilename)) {
- curFilename = filename + "." + n++;
- }
- usedLogNames.Add(curFilename);
- }
-
- return new StreamWriter(curFilename, false);
- }
-
- private void FlushProverWarnings()
- {
- var handler = currentErrorHandler;
- if (handler != null) {
- lock (proverWarnings) {
- proverWarnings.Iter(handler.OnProverWarning);
- proverWarnings.Clear();
- }
- }
- }
-
- private void HandleProverError(string s)
- {
- s = s.Replace("\r", "");
- lock (proverWarnings) {
- while (s.StartsWith("WARNING: ")) {
- var idx = s.IndexOf('\n');
- var warn = s;
- if (idx > 0) {
- warn = s.Substring(0, idx);
- s = s.Substring(idx + 1);
- } else {
- s = "";
- }
- warn = warn.Substring(9);
- proverWarnings.Add(warn);
- }
- }
-
- FlushProverWarnings();
-
- if (s == "") return;
-
- lock (proverErrors) {
- proverErrors.Add(s);
- Console.WriteLine("Prover error: " + s);
- }
- }
-
- [NoDefaultContract]
- public override Outcome CheckOutcome(ErrorHandler handler)
- {
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
-
- var result = CheckOutcomeCore(handler);
- SendThisVC("(pop 1)");
- FlushLogFile();
+ }
+ SendThisVC ("(fixedpoint-pop)");
+ Pop ();
+ AxiomsAreSetup = false;
+ return result;
+ }
+
+ private static HashSet<string> usedLogNames = new HashSet<string> ();
+
+ private TextWriter OpenOutputFile (string descriptiveName)
+ {
+ Contract.Requires (descriptiveName != null);
+ Contract.Ensures (Contract.Result<TextWriter> () != null);
+
+ string filename = options.LogFilename;
+ filename = Helpers.SubstituteAtPROC (descriptiveName, cce.NonNull (filename));
+ var curFilename = filename;
+
+ lock (usedLogNames) {
+ int n = 1;
+ while (usedLogNames.Contains(curFilename)) {
+ curFilename = filename + "." + n++;
+ }
+ usedLogNames.Add (curFilename);
+ }
+
+ return new StreamWriter (curFilename, false);
+ }
+
+ private void FlushProverWarnings ()
+ {
+ var handler = currentErrorHandler;
+ if (handler != null) {
+ lock (proverWarnings) {
+ proverWarnings.Iter (handler.OnProverWarning);
+ proverWarnings.Clear ();
+ }
+ }
+ }
+
+ private void HandleProverError (string s)
+ {
+ s = s.Replace ("\r", "");
+ lock (proverWarnings) {
+ while (s.StartsWith("WARNING: ")) {
+ var idx = s.IndexOf ('\n');
+ var warn = s;
+ if (idx > 0) {
+ warn = s.Substring (0, idx);
+ s = s.Substring (idx + 1);
+ } else {
+ s = "";
+ }
+ warn = warn.Substring (9);
+ proverWarnings.Add (warn);
+ }
+ }
+
+ FlushProverWarnings ();
+
+ if (s == "")
+ return;
+
+ lock (proverErrors) {
+ proverErrors.Add (s);
+ Console.WriteLine ("Prover error: " + s);
+ }
+ }
+
+ [NoDefaultContract]
+ public override Outcome CheckOutcome (ErrorHandler handler)
+ {
+ Contract.EnsuresOnThrow<UnexpectedProverOutputException> (true);
+
+ var result = CheckOutcomeCore (handler);
+ SendThisVC ("(pop 1)");
+ FlushLogFile ();
+
+ return result;
+ }
+
+ [NoDefaultContract]
+ public override Outcome CheckOutcomeCore (ErrorHandler handler)
+ {
+ Contract.EnsuresOnThrow<UnexpectedProverOutputException> (true);
+
+ var result = Outcome.Undetermined;
- return result;
- }
+ if (Process == null)
+ return result;
- [NoDefaultContract]
- public override Outcome CheckOutcomeCore(ErrorHandler handler)
- {
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
-
- var result = Outcome.Undetermined;
+ try {
+ currentErrorHandler = handler;
+ FlushProverWarnings ();
- if (Process == null)
- return result;
+ var errorsLeft = CommandLineOptions.Clo.ProverCCLimit;
+ if (errorsLeft < 1)
+ errorsLeft = 1;
- try {
- currentErrorHandler = handler;
- FlushProverWarnings();
+ var globalResult = Outcome.Undetermined;
- var errorsLeft = CommandLineOptions.Clo.ProverCCLimit;
- if (errorsLeft < 1)
- errorsLeft = 1;
+ while (true) {
+ errorsLeft--;
+ string[] labels = null;
- var globalResult = Outcome.Undetermined;
+ result = GetResponse ();
+ if (globalResult == Outcome.Undetermined)
+ globalResult = result;
- while (true) {
- errorsLeft--;
- string[] labels = null;
-
- result = GetResponse();
- if (globalResult == Outcome.Undetermined)
- globalResult = result;
-
- if (result == Outcome.Invalid || result == Outcome.TimeOut || result == Outcome.OutOfMemory) {
- IList<string> xlabels;
- if (CommandLineOptions.Clo.UseLabels) {
- labels = GetLabelsInfo();
- if (labels == null)
- {
- xlabels = new string[] { };
+ if (result == Outcome.Invalid || result == Outcome.TimeOut || result == Outcome.OutOfMemory) {
+ IList<string> xlabels;
+ if (CommandLineOptions.Clo.UseLabels) {
+ labels = GetLabelsInfo ();
+ if (labels == null) {
+ xlabels = new string[] { };
}
else
{
@@ -905,6 +850,8 @@ namespace Microsoft.Boogie.SMTLib else if (resp.ArgCount != 0)
break;
path.Add(v);
+ if (v.Equals("0"))
+ throw new UnexpectedProverOutputException("because of (get-value ((ControlFlow " + controlFlowConstant + " " + v + ")))");
SendThisVC("(get-value ((ControlFlow " + controlFlowConstant + " " + v + ")))");
}
return path.ToArray();
@@ -925,7 +872,11 @@ namespace Microsoft.Boogie.SMTLib 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;
@@ -934,9 +885,23 @@ namespace Microsoft.Boogie.SMTLib HandleProverError("Unexpected prover response getting model: " + resp.ToString());
}
List<Model> models = null;
- try {
- models = Model.ParseModels(new StringReader("Z3 error model: \n" + modelStr));
- }
+ try {
+ switch (options.Solver) {
+ case SolverKind.Z3:
+ if (options.SMTLib2Model) {
+ 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);
}
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..84d0ba47 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";
+ Logic = "QF_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..5865a333 100644 --- a/Source/Provers/SMTLib/Z3.cs +++ b/Source/Provers/SMTLib/Z3.cs @@ -283,9 +283,17 @@ 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 (options.SMTLib2Model)
+ {
+ 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 8afbf027..ad2b7e68 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -234,7 +234,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 m;
@@ -1700,11 +1700,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 b4db817f..f90788d7 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" />
|