summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar pantazis <pdeligia@me.com>2013-06-12 03:19:31 +0100
committerGravatar pantazis <pdeligia@me.com>2013-06-12 03:19:31 +0100
commit5e70254714df8e3a7db1532f283a89a515a96f12 (patch)
treec4baa2454dac22d1d3a99ee56d43e35c7bebfa94
parentff340131dc847849f81c28575c0add5598095cb3 (diff)
CVC4 Parser
Diffstat
-rw-r--r--Source/AbsInt/AbsInt.csproj11
-rw-r--r--Source/Basetypes/Basetypes.csproj4
-rw-r--r--Source/Boogie.sln480
-rw-r--r--Source/BoogieDriver/BoogieDriver.csproj31
-rw-r--r--Source/CodeContractsExtender/CodeContractsExtender.csproj4
-rw-r--r--Source/Core/Core.csproj4
-rw-r--r--Source/Doomed/Doomed.csproj18
-rw-r--r--Source/ExecutionEngine/ExecutionEngine.csproj24
-rw-r--r--Source/Graph/Graph.csproj4
-rw-r--r--Source/Houdini/Houdini.csproj4
-rw-r--r--Source/Model/Model.csproj5
-rw-r--r--Source/Model/ModelParser.cs1178
-rw-r--r--Source/ModelViewer/ModelViewer.csproj3
-rw-r--r--Source/ParserHelper/ParserHelper.csproj2
-rw-r--r--Source/Predication/Predication.csproj12
-rw-r--r--Source/Provers/SMTLib/ProverInterface.cs66
-rw-r--r--Source/VCExpr/VCExpr.csproj4
-rw-r--r--Source/VCGeneration/VCGeneration.csproj4
18 files changed, 1567 insertions, 291 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..b6859a4a 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,56 @@ 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
+ 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/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.csproj b/Source/Model/Model.csproj
index a14dde8e..a7255433 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..cf0ea45f
--- /dev/null
+++ b/Source/Model/ModelParser.cs
@@ -0,0 +1,1178 @@
+//-----------------------------------------------------------------------------
+//
+// 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_2 : 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);
+
+ Console.WriteLine("");
+ for (int i = 0; i < words.Count; i++)
+ {
+ Console.Write(words[i] + " ");
+ }
+
+ 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());
+
+ Console.WriteLine("");
+ for (int i = 0; i < tuple.Count; i++)
+ {
+ Console.Write(tuple[i] + " ");
+ }
+
+ 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");
+ }
+ }
+ }
+ }
+
+ abstract class ParserSMT : ModelParser
+ {
+ protected string[] tokens;
+ protected List<string> output;
+
+ protected 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;
+ }
+
+ abstract protected void ParseLeftParenthesis(ref int i);
+ abstract protected void ParseITE(ref int i);
+ abstract protected void ParseArray(ref int i);
+
+ void ParseEqual(ref int i)
+ {
+ i += 3;
+ output.Add(GetValue(i));
+ output.Add("->");
+ i += 2;
+ output.Add(GetValue(i));
+ output.Add(" ");
+ output.Add("else");
+ output.Add("->");
+ i++;
+ }
+
+ protected void ParseBitVector(ref int i)
+ {
+ i++;
+
+ if (tokens[i] == "BitVec")
+ {
+ output.Add("->");
+ i += 3;
+ }
+
+ if (tokens[i].Contains("bv"))
+ {
+ output.Add(GetValue(i + 1));
+ i += 2;
+ }
+ }
+
+ void ParseDefineFun(ref int i)
+ {
+ i++;
+
+ output.Add(GetValue(i));
+ output.Add("->");
+
+ i++;
+ }
+
+ void ParseRightParenthesis(ref int i)
+ {
+ i++;
+
+ if (i == tokens.Length && output.Count == 2)
+ {
+ i += -2;
+
+ if (tokens[i] == ")")
+ {
+ i += -1;
+ output.Add(GetValue(i));
+ }
+ else
+ {
+ output.Add(GetValue(i));
+ }
+ }
+
+ if (i == tokens.Length && output.Contains("{"))
+ {
+ output.Add(" ");
+ output.Add("}");
+ }
+ }
+
+ void ParseTokens()
+ {
+ var i = 0;
+ bool doneParsing = false;
+
+ while(!doneParsing)
+ {
+ switch (tokens[i])
+ {
+ case ")":
+ ParseRightParenthesis(ref i);
+ break;
+
+ case "(":
+ ParseLeftParenthesis(ref i);
+ break;
+
+ case "declare-sort":
+ doneParsing = true;
+ break;
+
+ case "define-fun":
+ ParseDefineFun(ref i);
+ break;
+
+ default:
+ i++;
+ break;
+ }
+
+ if (i == tokens.Length)
+ doneParsing = true;
+ }
+ }
+
+ protected 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>();
+ ParseTokens();
+
+ return output;
+ }
+ }
+
+ internal class ParserZ3 : ParserSMT
+ {
+ protected override void ParseITE(ref int i)
+ {
+ for (; ; )
+ {
+ if (tokens[i] == "ite")
+ {
+ i++;
+
+ for (; ; )
+ {
+ if (tokens[i] == "(" && tokens[i + 1] == "and")
+ i += 2;
+
+ if (tokens[i] == "(" && tokens[i + 1] == "=")
+ {
+ if (tokens[i + 3] == "(" && tokens[i + 4] == "-")
+ {
+ i += 7;
+ output.Add(GetValue(i - 2));
+ }
+ if (tokens[i + 3] == "(" && tokens[i + 4] == "_")
+ {
+ i += 8;
+ output.Add(GetValue(i - 2));
+ }
+ else
+ {
+ i += 4;
+ output.Add(GetValue(i - 1));
+ }
+
+ i++;
+ continue;
+ }
+
+ output.Add("->");
+
+ if (tokens[i] == ")") i++;
+
+ if (tokens[i] == "(" && tokens[i + 1] == "-")
+ {
+ i += 3;
+ output.Add(GetValue(i - 1));
+ }
+ else if (tokens[i] == "(" && tokens[i + 1] == "_")
+ {
+ i += 4;
+ output.Add(GetValue(i - 1));
+ }
+ else
+ {
+ i++;
+ output.Add(GetValue(i - 1));
+ }
+
+ output.Add(" ");
+ break;
+ }
+ }
+
+ if (tokens[i] == "(" && tokens[i + 1] == "-")
+ {
+ i += 2;
+ output.Add("else");
+ output.Add("->");
+ output.Add(GetValue(i));
+ break;
+ }
+ else if (tokens[i] == "(" && tokens[i + 1] == "_")
+ {
+ i += 3;
+ output.Add("else");
+ output.Add("->");
+ output.Add(GetValue(i));
+ break;
+ }
+ else if (tokens[i] == ")" && tokens[i - 2] == "-")
+ {
+ i++;
+ continue;
+ }
+ else if (tokens[i] == ")" && tokens[i - 3] == "_")
+ {
+ i++;
+ continue;
+ }
+ else if (tokens[i] != "(")
+ {
+ output.Add("else");
+ output.Add("->");
+ output.Add(GetValue(i));
+ break;
+ }
+ else i++;
+ }
+ }
+
+ void ParseArgument(ref int i)
+ {
+ output.Add("{");
+ output.Add(" ");
+
+ i++;
+ }
+
+
+ protected override void ParseArray(ref int i)
+ {
+ while (tokens[i] != "as-array")
+ i++;
+
+ output.Add("as-array[" + tokens[i + 1] + "]");
+ }
+
+ protected override void ParseLeftParenthesis(ref int i)
+ {
+ i++;
+
+ switch (tokens[i])
+ {
+ case "ite":
+ ParseITE(ref i);
+ break;
+
+ case "Array":
+ ParseArray(ref i);
+ break;
+
+ case "x!1":
+ ParseArgument(ref i);
+ break;
+
+ case "_":
+ ParseBitVector(ref i);
+ break;
+
+ default:
+ break;
+ }
+ }
+
+ 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 = GetParsedTokens(line);
+
+ Console.WriteLine("");
+ for (int i = 0; i < words.Count; i++)
+ {
+ Console.Write(words[i] + " ");
+ }
+
+ if (words.Count == 0) continue;
+ var lastToken = words[words.Count - 1];
+ if (currModel == null)
+ BadModel("model begin marker not found");
+
+ if (words.Count > 3 && words[1] == "->")
+ {
+ var funName = (string) words[0];
+ Model.Func fn = null;
+
+ if (words[2] != "{")
+ BadModel("unidentified function definition 5");
+
+ fn = currModel.TryGetFunc(funName);
+
+ int i = 4;
+ for (; ; )
+ {
+ if (words[i] == "}")
+ {
+ if (i == words.Count - 1)
+ {
+ if (fn == null)
+ fn = currModel.MkFunc(funName, 1);
+ break;
+ }
+ else
+ {
+ i++;
+ continue;
+ }
+ }
+
+ for (; ; )
+ {
+ if (words[i] == " ")
+ {
+ i++;
+ break;
+ }
+
+ if (i == 4 && words[3] == " " && words[5] == " ") {
+ if (fn == null)
+ fn = currModel.MkFunc(funName, 1);
+ if (fn.Else == null)
+ fn.Else = GetElt(words[i]);
+ i++;
+ continue;
+ }
+
+ if (words[i] == "else")
+ {
+ if (words[i + 1] == "->")
+ {
+ i += 2;
+
+ if (words[i] == "}")
+ BadModel("unidentified function definition 1");
+
+ if (words[i] == "{")
+ {
+ i++;
+ continue;
+ }
+ else
+ {
+ if (fn != null && !(words[i] == "#unspecified") && fn.Else == null)
+ fn.Else = GetElt(words[i]);
+ i++;
+ continue;
+ }
+ }
+ else
+ BadModel("unidentified function definition 2");
+ }
+
+ int arity = 0;
+ for (; ; )
+ {
+ arity++;
+ if (words[arity + i] == " ")
+ {
+ arity -= 2;
+ break;
+ }
+ }
+
+ if (words[i + arity] == "->")
+ {
+ i += arity + 1;
+
+ if (words[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(words[idx + i - arity - 1]);
+
+ fn.AddApp(GetElt(words[i]), args);
+
+ i++;
+ break;
+ }
+ }
+ }
+ else if (words.Count == 3 && words[1] == "->")
+ {
+ var funName = (string) words[0];
+ Model.Func fn = null;
+
+ fn = currModel.MkFunc(funName, 0);
+ fn.SetConstant(GetElt(lastToken));
+ }
+ else
+ BadModel("unidentified line");
+ }
+ }
+ }
+
+ internal class ParserCVC4 : ParserSMT
+ {
+ int arrayNum;
+ int arity;
+
+ 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++;
+ }
+ }
+ /*
+ protected override void ParseITE(ref int i)
+ {
+ List<string> args = new List<string>();
+ List<string> results = new List<string>();
+
+ FindArity();
+
+ output.Add("{");
+ output.Add(" ");
+
+ for (; ; )
+ {
+ if (tokens[i] == ")")
+ {
+ if ((tokens[i + 1] == ")" || tokens[i + 2] == ")") &&
+ (tokens[i + 2] != "ite" || tokens[i + 3] != "ite") &&
+ (tokens[i - 3] == "_" || tokens[i - 2] == "-"))
+ {
+ results.Add(GetValue(i - 1));
+ break;
+ }
+ else
+ {
+ args.Add(GetValue(i - 1));
+
+ if (tokens[i + 1] == "(" && tokens[i + 2] == "-")
+ {
+ results.Add(GetValue(i + 3));
+ i += 5;
+ }
+ else if (tokens[i + 2] != "ite")
+ {
+ results.Add(GetValue(i + 1));
+ i += 2;
+ }
+ else i++;
+ }
+ }
+ else i++;
+ }
+
+ int idx = 0;
+ for (int j = 0; j < results.Count - 1; j++)
+ {
+ if (arity == 1)
+ {
+ output.Add(args[idx]);
+ idx++;
+ }
+ else
+ {
+ output.Add(args[0]);
+
+ for (int r = 1; r < arity; r++)
+ {
+ idx++;
+ output.Add(args[idx]);
+ }
+ }
+
+ output.Add("->");
+ output.Add(results[j]);
+ output.Add(" ");
+ }
+
+ output.Add("else");
+ output.Add("->");
+ output.Add(results[results.Count - 1]);
+ }
+ */
+ protected override void ParseITE(ref int i)
+ {
+ List<string> args = new List<string>();
+ List<string> results = new List<string>();
+
+ FindArity();
+
+ output.Add("{");
+ output.Add(" ");
+
+ for (; ; )
+ {
+ i++;
+
+ if (tokens[i] == ")")
+ {
+ if (((tokens[i + 1] == ")" && tokens[i + 3] != "ite") ||
+ (tokens[i + 2] == ")" && tokens[i + 4] != "ite")) &&
+ args.Count % arity == 0)
+ {
+ Console.WriteLine("Res(*): " + GetValue(i - 1));
+ results.Add(GetValue(i - 1));
+ break;
+ }
+
+ if (tokens[i - 3] == "=" || tokens[i - 5] == "=" || tokens[i - 6] == "=")
+ {
+ Console.WriteLine("Arg: " + GetValue(i - 1));
+ args.Add(GetValue(i - 1));
+ }
+
+ if (tokens [i + 1] == ")") i += 2;
+ else i++;
+
+ if (tokens[i] == "(" && tokens[i + 1] == "-")
+ {
+ Console.WriteLine("Res: " + GetValue(i + 2));
+ results.Add(GetValue(i + 2));
+ i += 4;
+ }
+ else if (tokens[i] == "(" && tokens[i + 1] == "_")
+ {
+ Console.WriteLine("Res: " + GetValue(i + 3));
+ results.Add(GetValue(i + 3));
+ i += 5;
+ }
+ else if (tokens[i] != "(")
+ {
+ Console.WriteLine("Res: " + GetValue(i));
+ results.Add(GetValue(i));
+ i++;
+ }
+ }
+ }
+
+ int idx = 0;
+ for (int j = 0; j < results.Count - 1; j++)
+ {
+ for (int r = 0; r < arity; r++)
+ {
+ output.Add(args[idx]);
+ idx++;
+ }
+
+ output.Add("->");
+ output.Add(results[j]);
+ output.Add(" ");
+ }
+
+ output.Add("else");
+ output.Add("->");
+ }
+
+ protected override void ParseArray(ref int i)
+ {
+ output.Add("as-array[k!" + arrayNum + "]");
+ output.Add("@SPLIT");
+ output.Add("k!" + arrayNum);
+ output.Add("->");
+ output.Add("{");
+ output.Add(" ");
+
+ for (; ; )
+ {
+ i++;
+
+ if (tokens[i] == "store")
+ {
+ while (tokens[i] != ",")
+ i++;
+
+ output.Add(GetValue(i + 10));
+ output.Add("->");
+ output.Add(GetValue(i + 15));
+ output.Add(" ");
+ output.Add("else");
+ output.Add("->");
+ output.Add(GetValue(i + 4));
+
+ i += 15;
+
+ break;
+ }
+ else if (tokens[i] == ",")
+ {
+ i += 2;
+ ParseBitVector(ref i);
+ break;
+ }
+ }
+ }
+
+ protected override void ParseLeftParenthesis(ref int i)
+ {
+ i++;
+
+ switch (tokens[i])
+ {
+ case "ite":
+ ParseITE(ref i);
+ break;
+
+ case "Array":
+ ParseArray(ref i);
+ break;
+
+ case "_":
+ ParseBitVector(ref i);
+ break;
+
+ default:
+ break;
+ }
+ }
+
+ 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;
+
+ var words = GetParsedTokens(line);
+
+ Console.WriteLine("");
+ for (int i = 0; i < words.Count; i++)
+ {
+ Console.Write(words[i] + " ");
+ }
+
+ if (words.Count == 0) continue;
+ var lastToken = words[words.Count - 1];
+ if (currModel == null)
+ BadModel("model begin marker not found");
+
+ if (words.Count > 3 && words[1] == "->")
+ {
+ var funName = (string) words[0];
+ Model.Func fn = null;
+ int i = 4;
+
+ if (words.Contains("@SPLIT"))
+ {
+ arrayNum++;
+
+ fn = currModel.MkFunc(funName, 0);
+ fn.SetConstant(GetElt(words[2]));
+
+ i = 8;
+
+ funName = (string) words[4];
+ fn = null;
+ }
+
+ if (words[2] != "{" && words[6] != "{")
+ BadModel("unidentified function definition 5");
+
+ fn = currModel.TryGetFunc(funName);
+
+ for (; ; )
+ {
+ if (words[i] == "}")
+ {
+ if (i == words.Count - 1)
+ {
+ if (fn == null)
+ fn = currModel.MkFunc(funName, 1);
+ break;
+ }
+ else
+ {
+ i++;
+ continue;
+ }
+ }
+
+ for (; ; )
+ {
+ if (words[i] == " ")
+ {
+ i++;
+ break;
+ }
+
+ if ((i == 4 || i == 8) && words[i - 1] == " " && words[i + 1] == " ") {
+ if (fn.Else == null)
+ fn.Else = GetElt(words[i]);
+ i++;
+ continue;
+ }
+
+ if (words[i] == "else")
+ {
+ if (words[i + 1] == "->")
+ {
+ i += 2;
+
+ if (words[i] == "}")
+ BadModel("unidentified function definition 1");
+
+ if (words[i] == "{")
+ {
+ i++;
+ continue;
+ }
+ else
+ {
+ if (fn != null && !(words[i] == "#unspecified") && fn.Else == null)
+ fn.Else = GetElt(words[i]);
+ i++;
+ continue;
+ }
+ }
+ else
+ BadModel("unidentified function definition 2");
+ }
+
+ int arity = 0;
+ for (; ; )
+ {
+ arity++;
+ if (words[arity + i] == " ")
+ {
+ arity -= 2;
+ break;
+ }
+ }
+
+ if (words[i + arity] == "->")
+ {
+ i += arity + 1;
+
+ if (words[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(words[idx + i - arity - 1]);
+
+ fn.AddApp(GetElt(words[i]), args);
+
+ i++;
+ break;
+ }
+ }
+ }
+ else if (words.Count == 3 && words[1] == "->")
+ {
+ var funName = (string) words[0];
+ Model.Func fn = null;
+
+ fn = currModel.MkFunc(funName, 0);
+ fn.SetConstant(GetElt(lastToken));
+ }
+ else
+ BadModel("unidentified line");
+ }
+ }
+ }
+}
diff --git a/Source/ModelViewer/ModelViewer.csproj b/Source/ModelViewer/ModelViewer.csproj
index ae46767b..46f80673 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/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/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 8f6c4503..eaa42b38 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -97,27 +97,27 @@ namespace Microsoft.Boogie.SMTLib
}
}
- 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;
- }
- }
+ ProcessStartInfo ComputeProcessStartInfo()
+ {
+ var path = this.options.ProverPath;
+ var solverOptions = "";
+
+ switch (options.Solver) {
+ case SolverKind.Z3:
+ solverOptions = "AUTO_CONFIG=false -smt2 -in";
+ if (path == null)
+ path = Z3.ExecutablePath();
+ return SMTLibProcess.ComputerProcessStartInfo(path, solverOptions);
+ case SolverKind.CVC4:
+ solverOptions = "--lang=smt --no-strict-parsing --no-condense-function-values --incremental";
+ if (path == null)
+ path = CVC4.ExecutablePath();
+ return SMTLibProcess.ComputerProcessStartInfo(path, solverOptions);
+ default:
+ Debug.Assert(false);
+ return null;
+ }
+ }
void SetupProcess()
{
@@ -873,18 +873,34 @@ 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"))
+ modelStr += resp.Arguments[i] + "\n";
+ }
+ //Console.WriteLine(modelStr);
}
else if (resp.ArgCount == 0 && resp.Name.Contains("->")) {
modelStr = resp.Name;
+ //Console.WriteLine(modelStr);
}
else {
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:
+ models = Model.ParseModels(new StringReader("Error model: \n" + modelStr), "Z3");
+ break;
+ case SolverKind.CVC4:
+ models = Model.ParseModels(new StringReader("Error model: \n" + modelStr), "CVC4");
+ break;
+ default:
+ Debug.Assert(false);
+ return null;
+ }
+ }
catch (ArgumentException exn) {
HandleProverError("Model parsing error: " + exn.Message);
}
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/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" />
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 16:07:14 +0000