diff options
| -rw-r--r-- | Source/BVD/BVD.csproj | 2 | ||||
| -rw-r--r-- | Source/Core/Absy.cs | 2 | ||||
| -rw-r--r-- | Source/Doomed/Doomed.csproj | 35 | ||||
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.csproj | 37 | ||||
| -rw-r--r-- | Source/Model/Model.csproj | 6 | ||||
| -rw-r--r-- | Source/ModelViewer/Main.cs | 12 | ||||
| -rw-r--r-- | Source/ModelViewer/ModelViewer.csproj | 4 | ||||
| -rw-r--r-- | Source/Predication/Predication.csproj | 35 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/Z3.cs | 268 | ||||
| -rw-r--r-- | Source/VCGeneration/Check.cs | 12 | ||||
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 2 | ||||
| -rw-r--r-- | Source/VCGeneration/StratifiedVC.cs | 2 | ||||
| -rw-r--r-- | Source/VCGeneration/VC.cs | 2 |
13 files changed, 270 insertions, 149 deletions
diff --git a/Source/BVD/BVD.csproj b/Source/BVD/BVD.csproj index 448adff7..687e83fb 100644 --- a/Source/BVD/BVD.csproj +++ b/Source/BVD/BVD.csproj @@ -42,7 +42,7 @@ <PlatformTarget>AnyCPU</PlatformTarget>
<DebugType>pdbonly</DebugType>
<Optimize>true</Optimize>
- <OutputPath>bin\Release\</OutputPath>
+ <OutputPath>..\..\Binaries\</OutputPath>
<DefineConstants>TRACE</DefineConstants>
<ErrorReport>prompt</ErrorReport>
<WarningLevel>4</WarningLevel>
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 2817acdc..7b3f6fc5 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -2924,7 +2924,7 @@ namespace Microsoft.Boogie { this.formalMap = null;
}
public Dictionary<Variable, Expr>/*!*/ GetImplFormalMap() {
- Contract.Ensures(Contract.Result<Hashtable>() != null);
+ Contract.Ensures(Contract.Result<Dictionary<Variable, Expr>>() != null);
if (this.formalMap != null)
return this.formalMap;
diff --git a/Source/Doomed/Doomed.csproj b/Source/Doomed/Doomed.csproj index a2390a39..e83c8f30 100644 --- a/Source/Doomed/Doomed.csproj +++ b/Source/Doomed/Doomed.csproj @@ -14,6 +14,7 @@ <TargetFrameworkProfile>Client</TargetFrameworkProfile>
<ProductVersion>12.0.0</ProductVersion>
<SchemaVersion>2.0</SchemaVersion>
+ <CodeContractsAssemblyMode>0</CodeContractsAssemblyMode>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
<DebugSymbols>true</DebugSymbols>
@@ -31,6 +32,40 @@ <DefineConstants>TRACE</DefineConstants>
<ErrorReport>prompt</ErrorReport>
<WarningLevel>4</WarningLevel>
+ <CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>
+ <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
+ <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
+ <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
+ <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
+ <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
+ <CodeContractsNonNullObligations>True</CodeContractsNonNullObligations>
+ <CodeContractsBoundsObligations>True</CodeContractsBoundsObligations>
+ <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
+ <CodeContractsEnumObligations>False</CodeContractsEnumObligations>
+ <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
+ <CodeContractsMissingPublicRequiresAsWarnings>True</CodeContractsMissingPublicRequiresAsWarnings>
+ <CodeContractsInferRequires>True</CodeContractsInferRequires>
+ <CodeContractsInferEnsures>False</CodeContractsInferEnsures>
+ <CodeContractsInferObjectInvariants>False</CodeContractsInferObjectInvariants>
+ <CodeContractsSuggestAssumptions>False</CodeContractsSuggestAssumptions>
+ <CodeContractsSuggestRequires>True</CodeContractsSuggestRequires>
+ <CodeContractsSuggestObjectInvariants>False</CodeContractsSuggestObjectInvariants>
+ <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
+ <CodeContractsShowSquigglies>True</CodeContractsShowSquigglies>
+ <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
+ <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
+ <CodeContractsCustomRewriterAssembly />
+ <CodeContractsCustomRewriterClass />
+ <CodeContractsLibPaths />
+ <CodeContractsExtraRewriteOptions />
+ <CodeContractsExtraAnalysisOptions />
+ <CodeContractsSQLServerOption />
+ <CodeContractsBaseLineFile />
+ <CodeContractsCacheAnalysisResults>True</CodeContractsCacheAnalysisResults>
+ <CodeContractsFailBuildOnWarnings>False</CodeContractsFailBuildOnWarnings>
+ <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
+ <CodeContractsReferenceAssembly>DoNotBuild</CodeContractsReferenceAssembly>
+ <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
</PropertyGroup>
<PropertyGroup>
<SignAssembly>true</SignAssembly>
diff --git a/Source/ExecutionEngine/ExecutionEngine.csproj b/Source/ExecutionEngine/ExecutionEngine.csproj index bebe686d..3c50afae 100644 --- a/Source/ExecutionEngine/ExecutionEngine.csproj +++ b/Source/ExecutionEngine/ExecutionEngine.csproj @@ -16,6 +16,7 @@ <AssemblyOriginatorKeyFile>..\InterimKey.snk</AssemblyOriginatorKeyFile>
<ProductVersion>12.0.0</ProductVersion>
<SchemaVersion>2.0</SchemaVersion>
+ <CodeContractsAssemblyMode>0</CodeContractsAssemblyMode>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
<DebugSymbols>true</DebugSymbols>
@@ -29,10 +30,44 @@ <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
<DebugType>pdbonly</DebugType>
<Optimize>true</Optimize>
- <OutputPath>bin\Release\</OutputPath>
+ <OutputPath>..\..\Binaries\</OutputPath>
<DefineConstants>TRACE</DefineConstants>
<ErrorReport>prompt</ErrorReport>
<WarningLevel>4</WarningLevel>
+ <CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>
+ <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
+ <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
+ <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
+ <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
+ <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
+ <CodeContractsNonNullObligations>True</CodeContractsNonNullObligations>
+ <CodeContractsBoundsObligations>True</CodeContractsBoundsObligations>
+ <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
+ <CodeContractsEnumObligations>False</CodeContractsEnumObligations>
+ <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
+ <CodeContractsMissingPublicRequiresAsWarnings>True</CodeContractsMissingPublicRequiresAsWarnings>
+ <CodeContractsInferRequires>True</CodeContractsInferRequires>
+ <CodeContractsInferEnsures>False</CodeContractsInferEnsures>
+ <CodeContractsInferObjectInvariants>False</CodeContractsInferObjectInvariants>
+ <CodeContractsSuggestAssumptions>False</CodeContractsSuggestAssumptions>
+ <CodeContractsSuggestRequires>True</CodeContractsSuggestRequires>
+ <CodeContractsSuggestObjectInvariants>False</CodeContractsSuggestObjectInvariants>
+ <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
+ <CodeContractsShowSquigglies>True</CodeContractsShowSquigglies>
+ <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
+ <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
+ <CodeContractsCustomRewriterAssembly />
+ <CodeContractsCustomRewriterClass />
+ <CodeContractsLibPaths />
+ <CodeContractsExtraRewriteOptions />
+ <CodeContractsExtraAnalysisOptions />
+ <CodeContractsSQLServerOption />
+ <CodeContractsBaseLineFile />
+ <CodeContractsCacheAnalysisResults>True</CodeContractsCacheAnalysisResults>
+ <CodeContractsFailBuildOnWarnings>False</CodeContractsFailBuildOnWarnings>
+ <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
+ <CodeContractsReferenceAssembly>DoNotBuild</CodeContractsReferenceAssembly>
+ <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
</PropertyGroup>
<ItemGroup>
<Reference Include="System" />
diff --git a/Source/Model/Model.csproj b/Source/Model/Model.csproj index cfd5f852..b307a799 100644 --- a/Source/Model/Model.csproj +++ b/Source/Model/Model.csproj @@ -19,7 +19,7 @@ <DebugSymbols>true</DebugSymbols>
<DebugType>full</DebugType>
<Optimize>false</Optimize>
- <OutputPath>bin\Debug\</OutputPath>
+ <OutputPath>..\..\Binaries\</OutputPath>
<DefineConstants>DEBUG;TRACE</DefineConstants>
<ErrorReport>prompt</ErrorReport>
<WarningLevel>4</WarningLevel>
@@ -27,7 +27,7 @@ <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
<DebugType>pdbonly</DebugType>
<Optimize>true</Optimize>
- <OutputPath>bin\Release\</OutputPath>
+ <OutputPath>..\..\Binaries\</OutputPath>
<DefineConstants>TRACE</DefineConstants>
<ErrorReport>prompt</ErrorReport>
<WarningLevel>4</WarningLevel>
@@ -40,7 +40,7 @@ </PropertyGroup>
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|AnyCPU'">
<DebugSymbols>true</DebugSymbols>
- <OutputPath>bin\Checked\</OutputPath>
+ <OutputPath>..\..\Binaries\</OutputPath>
<DefineConstants>DEBUG;TRACE</DefineConstants>
<DebugType>full</DebugType>
<PlatformTarget>AnyCPU</PlatformTarget>
diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs index fde1971b..c15ea167 100644 --- a/Source/ModelViewer/Main.cs +++ b/Source/ModelViewer/Main.cs @@ -725,15 +725,19 @@ namespace Microsoft.Boogie.ModelViewer largeFont = new Font(smallFont.FontFamily, smallFont.Size * 2, smallFont.Unit);
}
- var font = largeFontToolStripMenuItem.Checked ? largeFont : smallFont;
- stateList.Font = font;
- currentStateView.Font = font;
- matchesList.Font = font;
+ SetFont(largeFontToolStripMenuItem.Checked ? largeFont : smallFont);
//textBox1.Font = font;
//linkLabel1.Font = font;
//label1.Font = font;
}
+ public void SetFont(System.Drawing.Font font)
+ {
+ stateList.Font = font;
+ currentStateView.Font = font;
+ matchesList.Font = font;
+ }
+
private void Main_Load(object sender, EventArgs e)
{
diff --git a/Source/ModelViewer/ModelViewer.csproj b/Source/ModelViewer/ModelViewer.csproj index 30f444c6..f86e4d4f 100644 --- a/Source/ModelViewer/ModelViewer.csproj +++ b/Source/ModelViewer/ModelViewer.csproj @@ -44,7 +44,7 @@ <PlatformTarget>AnyCPU</PlatformTarget>
<DebugType>pdbonly</DebugType>
<Optimize>true</Optimize>
- <OutputPath>bin\Release\</OutputPath>
+ <OutputPath>..\..\Binaries\</OutputPath>
<DefineConstants>TRACE</DefineConstants>
<ErrorReport>prompt</ErrorReport>
<WarningLevel>4</WarningLevel>
@@ -60,7 +60,7 @@ </PropertyGroup>
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|x86'">
<DebugSymbols>true</DebugSymbols>
- <OutputPath>bin\x86\Checked\</OutputPath>
+ <OutputPath>..\..\Binaries\</OutputPath>
<DefineConstants>DEBUG;TRACE</DefineConstants>
<DebugType>full</DebugType>
<PlatformTarget>AnyCPU</PlatformTarget>
diff --git a/Source/Predication/Predication.csproj b/Source/Predication/Predication.csproj index 663de263..9ed46bc6 100644 --- a/Source/Predication/Predication.csproj +++ b/Source/Predication/Predication.csproj @@ -14,6 +14,7 @@ <TargetFrameworkProfile>Client</TargetFrameworkProfile>
<ProductVersion>12.0.0</ProductVersion>
<SchemaVersion>2.0</SchemaVersion>
+ <CodeContractsAssemblyMode>0</CodeContractsAssemblyMode>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
<DebugSymbols>true</DebugSymbols>
@@ -31,6 +32,40 @@ <DefineConstants>TRACE</DefineConstants>
<ErrorReport>prompt</ErrorReport>
<WarningLevel>4</WarningLevel>
+ <CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>
+ <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
+ <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
+ <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
+ <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
+ <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
+ <CodeContractsNonNullObligations>True</CodeContractsNonNullObligations>
+ <CodeContractsBoundsObligations>True</CodeContractsBoundsObligations>
+ <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
+ <CodeContractsEnumObligations>False</CodeContractsEnumObligations>
+ <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
+ <CodeContractsMissingPublicRequiresAsWarnings>True</CodeContractsMissingPublicRequiresAsWarnings>
+ <CodeContractsInferRequires>True</CodeContractsInferRequires>
+ <CodeContractsInferEnsures>False</CodeContractsInferEnsures>
+ <CodeContractsInferObjectInvariants>False</CodeContractsInferObjectInvariants>
+ <CodeContractsSuggestAssumptions>False</CodeContractsSuggestAssumptions>
+ <CodeContractsSuggestRequires>True</CodeContractsSuggestRequires>
+ <CodeContractsSuggestObjectInvariants>False</CodeContractsSuggestObjectInvariants>
+ <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
+ <CodeContractsShowSquigglies>True</CodeContractsShowSquigglies>
+ <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
+ <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
+ <CodeContractsCustomRewriterAssembly />
+ <CodeContractsCustomRewriterClass />
+ <CodeContractsLibPaths />
+ <CodeContractsExtraRewriteOptions />
+ <CodeContractsExtraAnalysisOptions />
+ <CodeContractsSQLServerOption />
+ <CodeContractsBaseLineFile />
+ <CodeContractsCacheAnalysisResults>True</CodeContractsCacheAnalysisResults>
+ <CodeContractsFailBuildOnWarnings>False</CodeContractsFailBuildOnWarnings>
+ <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
+ <CodeContractsReferenceAssembly>DoNotBuild</CodeContractsReferenceAssembly>
+ <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
</PropertyGroup>
<PropertyGroup>
<SignAssembly>true</SignAssembly>
diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs index d2e06168..a2bf80ba 100644 --- a/Source/Provers/SMTLib/Z3.cs +++ b/Source/Provers/SMTLib/Z3.cs @@ -202,171 +202,175 @@ namespace Microsoft.Boogie.SMTLib public static void SetupOptions(SMTLibProverOptions options)
{
- FindExecutable();
- int major, minor;
- GetVersion(out major, out minor);
- if (major > 4 || major == 4 && minor >= 3)
- {
+ FindExecutable();
+ int major, minor;
+ GetVersion(out major, out minor);
+ if (major > 4 || major == 4 && minor >= 3)
+ {
- // don't bother with auto-config - it would disable explicit settings for eager threshold and so on
- options.AddWeakSmtOption("AUTO_CONFIG", "false");
+ // don't bother with auto-config - it would disable explicit settings for eager threshold and so on
+ options.AddWeakSmtOption("AUTO_CONFIG", "false");
- //options.AddWeakSmtOption("MODEL_PARTIAL", "true");
- //options.WeakAddSmtOption("MODEL_VALUE_COMPLETION", "false");
+ //options.AddWeakSmtOption("MODEL_PARTIAL", "true");
+ //options.WeakAddSmtOption("MODEL_VALUE_COMPLETION", "false");
- // options.AddWeakSmtOption("MODEL_HIDE_UNUSED_PARTITIONS", "false"); TODO: what does this do?
+ // options.AddWeakSmtOption("MODEL_HIDE_UNUSED_PARTITIONS", "false"); TODO: what does this do?
- options.AddWeakSmtOption("MODEL.V2", "true");
- //options.AddWeakSmtOption("ASYNC_COMMANDS", "false"); TODO: is this needed?
+ options.AddWeakSmtOption("MODEL.V2", "true");
+ //options.AddWeakSmtOption("ASYNC_COMMANDS", "false"); TODO: is this needed?
- if (!options.OptimizeForBv)
- {
- // Phase selection means to always try the negative literal polarity first, seems to be good for Boogie.
- // The restart parameters change the restart behavior to match Z3 v1, which also seems to be good.
- options.AddWeakSmtOption("smt.PHASE_SELECTION", "0");
- options.AddWeakSmtOption("smt.RESTART_STRATEGY", "0");
- options.AddWeakSmtOption("smt.RESTART_FACTOR", "|1.5|");
-
- // Make the integer model more diverse by default, speeds up some benchmarks a lot.
- options.AddWeakSmtOption("smt.ARITH.RANDOM_INITIAL_VALUE", "true");
-
- // The left-to-right structural case-splitting strategy.
- //options.AddWeakSmtOption("SORT_AND_OR", "false"); // always false now
- options.AddWeakSmtOption("smt.CASE_SPLIT", "3");
-
- // In addition delay adding unit conflicts.
- options.AddWeakSmtOption("smt.DELAY_UNITS", "true");
- //options.AddWeakSmtOption("DELAY_UNITS_THRESHOLD", "16"); TODO: what?
- }
+ if (!options.OptimizeForBv)
+ {
+ // Phase selection means to always try the negative literal polarity first, seems to be good for Boogie.
+ // The restart parameters change the restart behavior to match Z3 v1, which also seems to be good.
+ options.AddWeakSmtOption("smt.PHASE_SELECTION", "0");
+ options.AddWeakSmtOption("smt.RESTART_STRATEGY", "0");
+ options.AddWeakSmtOption("smt.RESTART_FACTOR", "|1.5|");
+
+ // Make the integer model more diverse by default, speeds up some benchmarks a lot.
+ options.AddWeakSmtOption("smt.ARITH.RANDOM_INITIAL_VALUE", "true");
+
+ // The left-to-right structural case-splitting strategy.
+ //options.AddWeakSmtOption("SORT_AND_OR", "false"); // always false now
+ options.AddWeakSmtOption("smt.CASE_SPLIT", "3");
+
+ // In addition delay adding unit conflicts.
+ options.AddWeakSmtOption("smt.DELAY_UNITS", "true");
+ //options.AddWeakSmtOption("DELAY_UNITS_THRESHOLD", "16"); TODO: what?
+ }
- // This is used by VCC, but could be also useful for others, if sk_hack(foo(x)) is included as trigger,
- // the foo(x0) will be activated for e-matching when x is skolemized to x0.
- options.AddWeakSmtOption("NNF.SK_HACK", "true");
+ // This is used by VCC, but could be also useful for others, if sk_hack(foo(x)) is included as trigger,
+ // the foo(x0) will be activated for e-matching when x is skolemized to x0.
+ options.AddWeakSmtOption("NNF.SK_HACK", "true");
- // don't use model-based quantifier instantiation; it never finishes on non-trivial Boogie problems
- options.AddWeakSmtOption("smt.MBQI", "false");
+ // don't use model-based quantifier instantiation; it never finishes on non-trivial Boogie problems
+ options.AddWeakSmtOption("smt.MBQI", "false");
- // More or less like MAM=0.
- options.AddWeakSmtOption("smt.QI.EAGER_THRESHOLD", "100");
- // Complex proof attempts in VCC (and likely elsewhere) require matching depth of 20 or more.
+ // More or less like MAM=0.
+ options.AddWeakSmtOption("smt.QI.EAGER_THRESHOLD", "100");
+ // Complex proof attempts in VCC (and likely elsewhere) require matching depth of 20 or more.
- // the following will make the :weight option more usable
- options.AddWeakSmtOption("smt.QI.COST", "|\"(+ weight generation)\"|"); // TODO: this doesn't seem to work
+ // the following will make the :weight option more usable
+ options.AddWeakSmtOption("smt.QI.COST", "|\"(+ weight generation)\"|"); // TODO: this doesn't seem to work
- //if (options.Inspector != null)
- // options.WeakAddSmtOption("PROGRESS_SAMPLING_FREQ", "100");
+ //if (options.Inspector != null)
+ // options.WeakAddSmtOption("PROGRESS_SAMPLING_FREQ", "100");
- options.AddWeakSmtOption("TYPE_CHECK", "true");
- options.AddWeakSmtOption("smt.BV.REFLECT", "true");
+ options.AddWeakSmtOption("TYPE_CHECK", "true");
+ options.AddWeakSmtOption("smt.BV.REFLECT", "true");
- if (options.TimeLimit > 0)
- {
- options.AddWeakSmtOption("TIMEOUT", options.TimeLimit.ToString());
- // This kills the Z3 *instance* after the specified time, not a particular query, so we cannot use it.
- // options.AddSolverArgument("/T:" + (options.TimeLimit + 1000) / 1000);
- }
+ if (options.TimeLimit > 0)
+ {
+ options.AddWeakSmtOption("TIMEOUT", options.TimeLimit.ToString());
+ // This kills the Z3 *instance* after the specified time, not a particular query, so we cannot use it.
+ // options.AddSolverArgument("/T:" + (options.TimeLimit + 1000) / 1000);
+ }
- if (options.Inspector != null)
- options.AddWeakSmtOption("PROGRESS_SAMPLING_FREQ", "200");
+ if (options.Inspector != null)
+ options.AddWeakSmtOption("PROGRESS_SAMPLING_FREQ", "200");
- if (CommandLineOptions.Clo.WeakArrayTheory)
- {
- options.AddWeakSmtOption("smt.array.weak", "true");
- options.AddWeakSmtOption("smt.array.extensional", "false");
- }
+ if (CommandLineOptions.Clo.WeakArrayTheory)
+ {
+ options.AddWeakSmtOption("smt.array.weak", "true");
+ options.AddWeakSmtOption("smt.array.extensional", "false");
+ }
+ }
+ else
+ {
+ // don't bother with auto-config - it would disable explicit settings for eager threshold and so on
+ options.AddWeakSmtOption("AUTO_CONFIG", "false");
+
+ //options.AddWeakSmtOption("MODEL_PARTIAL", "true");
+ //options.WeakAddSmtOption("MODEL_VALUE_COMPLETION", "false");
+ options.AddWeakSmtOption("MODEL_HIDE_UNUSED_PARTITIONS", "false");
+ options.AddWeakSmtOption("ASYNC_COMMANDS", "false");
+
+ if (CommandLineOptions.Clo.UseSmtOutputFormat)
+ {
+ options.AddWeakSmtOption("pp-bv-literals", "false"); ;
}
else
{
- // don't bother with auto-config - it would disable explicit settings for eager threshold and so on
- options.AddWeakSmtOption("AUTO_CONFIG", "false");
-
- //options.AddWeakSmtOption("MODEL_PARTIAL", "true");
- //options.WeakAddSmtOption("MODEL_VALUE_COMPLETION", "false");
- options.AddWeakSmtOption("MODEL_HIDE_UNUSED_PARTITIONS", "false");
- options.AddWeakSmtOption("ASYNC_COMMANDS", "false");
+ options.AddWeakSmtOption("MODEL_V2", "true");
+ }
- if (CommandLineOptions.Clo.UseSmtOutputFormat) {
- options.AddWeakSmtOption("pp-bv-literals", "false");;
- } else {
- options.AddWeakSmtOption("MODEL_V2", "true");
- }
+ if (!options.OptimizeForBv)
+ {
+ // Phase selection means to always try the negative literal polarity first, seems to be good for Boogie.
+ // The restart parameters change the restart behavior to match Z3 v1, which also seems to be good.
+ options.AddWeakSmtOption("PHASE_SELECTION", "0");
+ options.AddWeakSmtOption("RESTART_STRATEGY", "0");
+ options.AddWeakSmtOption("RESTART_FACTOR", "|1.5|");
+
+ // Make the integer model more diverse by default, speeds up some benchmarks a lot.
+ options.AddWeakSmtOption("ARITH_RANDOM_INITIAL_VALUE", "true");
+
+ // The left-to-right structural case-splitting strategy.
+ //options.AddWeakSmtOption("SORT_AND_OR", "false"); // always false now
+ options.AddWeakSmtOption("CASE_SPLIT", "3");
+
+ // In addition delay adding unit conflicts.
+ options.AddWeakSmtOption("DELAY_UNITS", "true");
+ options.AddWeakSmtOption("DELAY_UNITS_THRESHOLD", "16");
+ }
- if (!options.OptimizeForBv)
- {
- // Phase selection means to always try the negative literal polarity first, seems to be good for Boogie.
- // The restart parameters change the restart behavior to match Z3 v1, which also seems to be good.
- options.AddWeakSmtOption("PHASE_SELECTION", "0");
- options.AddWeakSmtOption("RESTART_STRATEGY", "0");
- options.AddWeakSmtOption("RESTART_FACTOR", "|1.5|");
-
- // Make the integer model more diverse by default, speeds up some benchmarks a lot.
- options.AddWeakSmtOption("ARITH_RANDOM_INITIAL_VALUE", "true");
-
- // The left-to-right structural case-splitting strategy.
- //options.AddWeakSmtOption("SORT_AND_OR", "false"); // always false now
- options.AddWeakSmtOption("CASE_SPLIT", "3");
-
- // In addition delay adding unit conflicts.
- options.AddWeakSmtOption("DELAY_UNITS", "true");
- options.AddWeakSmtOption("DELAY_UNITS_THRESHOLD", "16");
- }
+ // This is used by VCC, but could be also useful for others, if sk_hack(foo(x)) is included as trigger,
+ // the foo(x0) will be activated for e-matching when x is skolemized to x0.
+ options.AddWeakSmtOption("NNF_SK_HACK", "true");
- // This is used by VCC, but could be also useful for others, if sk_hack(foo(x)) is included as trigger,
- // the foo(x0) will be activated for e-matching when x is skolemized to x0.
- options.AddWeakSmtOption("NNF_SK_HACK", "true");
+ // don't use model-based quantifier instantiation; it never finishes on non-trivial Boogie problems
+ options.AddWeakSmtOption("MBQI", "false");
- // don't use model-based quantifier instantiation; it never finishes on non-trivial Boogie problems
- options.AddWeakSmtOption("MBQI", "false");
+ // More or less like MAM=0.
+ options.AddWeakSmtOption("QI_EAGER_THRESHOLD", "100");
+ // Complex proof attempts in VCC (and likely elsewhere) require matching depth of 20 or more.
- // More or less like MAM=0.
- options.AddWeakSmtOption("QI_EAGER_THRESHOLD", "100");
- // Complex proof attempts in VCC (and likely elsewhere) require matching depth of 20 or more.
+ // the following will make the :weight option more usable
+ options.AddWeakSmtOption("QI_COST", "|\"(+ weight generation)\"|");
- // the following will make the :weight option more usable
- options.AddWeakSmtOption("QI_COST", "|\"(+ weight generation)\"|");
+ //if (options.Inspector != null)
+ // options.WeakAddSmtOption("PROGRESS_SAMPLING_FREQ", "100");
- //if (options.Inspector != null)
- // options.WeakAddSmtOption("PROGRESS_SAMPLING_FREQ", "100");
+ options.AddWeakSmtOption("TYPE_CHECK", "true");
+ options.AddWeakSmtOption("BV_REFLECT", "true");
- options.AddWeakSmtOption("TYPE_CHECK", "true");
- options.AddWeakSmtOption("BV_REFLECT", "true");
+ if (options.TimeLimit > 0)
+ {
+ options.AddWeakSmtOption("SOFT_TIMEOUT", options.TimeLimit.ToString());
+ // This kills the Z3 *instance* after the specified time, not a particular query, so we cannot use it.
+ // options.AddSolverArgument("/T:" + (options.TimeLimit + 1000) / 1000);
+ }
- if (options.TimeLimit > 0)
- {
- options.AddWeakSmtOption("SOFT_TIMEOUT", options.TimeLimit.ToString());
- // This kills the Z3 *instance* after the specified time, not a particular query, so we cannot use it.
- // options.AddSolverArgument("/T:" + (options.TimeLimit + 1000) / 1000);
- }
+ if (options.Inspector != null)
+ options.AddWeakSmtOption("PROGRESS_SAMPLING_FREQ", "200");
- if (options.Inspector != null)
- options.AddWeakSmtOption("PROGRESS_SAMPLING_FREQ", "200");
-
- if (CommandLineOptions.Clo.WeakArrayTheory)
- {
- options.AddWeakSmtOption("ARRAY_WEAK", "true");
- options.AddWeakSmtOption("ARRAY_EXTENSIONAL", "false");
- }
-
+ if (CommandLineOptions.Clo.WeakArrayTheory)
+ {
+ options.AddWeakSmtOption("ARRAY_WEAK", "true");
+ options.AddWeakSmtOption("ARRAY_EXTENSIONAL", "false");
}
+ }
+
+ options.AddWeakSmtOption("MODEL_ON_TIMEOUT", "true");
- // legacy option handling
- if (!CommandLineOptions.Clo.z3AtFlag)
- options.MultiTraces = true;
+ // legacy option handling
+ if (!CommandLineOptions.Clo.z3AtFlag)
+ options.MultiTraces = true;
- foreach (string opt in CommandLineOptions.Clo.Z3Options)
+ foreach (string opt in CommandLineOptions.Clo.Z3Options)
+ {
+ Contract.Assert(opt != null);
+ int eq = opt.IndexOf("=");
+ if (eq > 0 && 'A' <= opt[0] && opt[0] <= 'Z' && !commandLineOnly.Contains(opt.Substring(0, eq)))
{
- Contract.Assert(opt != null);
- int eq = opt.IndexOf("=");
- if (eq > 0 && 'A' <= opt[0] && opt[0] <= 'Z' && !commandLineOnly.Contains(opt.Substring(0, eq)))
- {
- options.AddSmtOption(opt.Substring(0, eq), opt.Substring(eq + 1));
- }
- else
- {
- options.AddSolverArgument(opt);
- }
+ options.AddSmtOption(opt.Substring(0, eq), opt.Substring(eq + 1));
+ }
+ else
+ {
+ options.AddSolverArgument(opt);
}
+ }
}
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index 62451caa..2237c2fc 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -57,7 +57,7 @@ namespace Microsoft.Boogie { public void GetReady()
{
- Contract.Requires(status == CheckerStatus.Idle);
+ Contract.Requires(IsIdle);
status = CheckerStatus.Ready;
}
@@ -268,6 +268,14 @@ namespace Microsoft.Boogie { }
}
+ public bool IsReady
+ {
+ get
+ {
+ return status == CheckerStatus.Ready;
+ }
+ }
+
public bool IsClosed {
get {
return status == CheckerStatus.Closed;
@@ -334,7 +342,7 @@ namespace Microsoft.Boogie { Contract.Requires(descriptiveName != null);
Contract.Requires(vc != null);
Contract.Requires(handler != null);
- Contract.Requires(status == CheckerStatus.Ready);
+ Contract.Requires(IsReady);
status = CheckerStatus.Busy;
hasOutput = false;
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 36b8fbe5..0ea08356 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -1191,7 +1191,7 @@ namespace VC { protected Dictionary<Variable, Expr> ComputeIncarnationMap(Block b, Dictionary<Block, Dictionary<Variable, Expr>> block2Incarnation) {
Contract.Requires(b != null);
Contract.Requires(block2Incarnation != null);
- Contract.Ensures(Contract.Result<Hashtable>() != null);
+ Contract.Ensures(Contract.Result<Dictionary<Variable, Expr>>() != null);
if (b.Predecessors.Count == 0) {
return new Dictionary<Variable, Expr>();
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index 7f5b3779..ceea2477 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -2117,7 +2117,7 @@ namespace VC { }
public Dictionary<int, Absy> getLabel2absy() {
- Contract.Ensures(Contract.Result<Hashtable>() != null);
+ Contract.Ensures(Contract.Result<Dictionary<int, Absy>>() != null);
Contract.Assert(currProc != null);
if (currProc == "") {
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index fd7a4f72..4806318a 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -2121,7 +2121,7 @@ namespace VC { {
Contract.Requires(impl != null);
Contract.Requires(program != null);
- Contract.Ensures(Contract.Result<Hashtable>() != null);
+ Contract.Ensures(Contract.Result<Dictionary<TransferCmd, ReturnCmd>>() != null);
Dictionary<TransferCmd, ReturnCmd> gotoCmdOrigins = new Dictionary<TransferCmd, ReturnCmd>();
Block exitBlock = GenerateUnifiedExit(impl, gotoCmdOrigins);
|