summaryrefslogtreecommitdiff
path: root/Source/Core
diff options
context:
space:
mode:
authorGravatar Pantazis Deligiannis <pdeligia@me.com>2013-07-15 12:21:57 +0100
committerGravatar Pantazis Deligiannis <pdeligia@me.com>2013-07-15 12:21:57 +0100
commit578382b6bd2ace4926e9ed97cf59ec38c7b07797 (patch)
tree5ea634e0c5c2881f674c38c5d3b1307c83db8916 /Source/Core
parentad34aee0bb9e9090418fd1cb2e2fced7ddb625d8 (diff)
parentee4be4f6280d39c31d95e50ac3ac039c6d2ba5f5 (diff)
Merge
Diffstat (limited to 'Source/Core')
-rw-r--r--Source/Core/CommandLineOptions.cs11
-rw-r--r--Source/Core/Core.csproj4
2 files changed, 15 insertions, 0 deletions
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index a9bd25ee..a1a4d740 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -411,6 +411,7 @@ namespace Microsoft.Boogie {
public bool SimplifyLogFileAppend = false;
public bool SoundnessSmokeTest = false;
public string Z3ExecutablePath = null;
+ public string CVC4ExecutablePath = null;
public enum ProverWarnings {
None,
@@ -1268,6 +1269,12 @@ namespace Microsoft.Boogie {
}
return true;
+ case "cvc4exe":
+ if (ps.ConfirmArgumentCount(1)) {
+ CVC4ExecutablePath = args[ps.i];
+ }
+ return true;
+
case "doBitVectorAnalysis":
DoBitVectorAnalysis = true;
if (ps.ConfirmArgumentCount(1)) {
@@ -1843,6 +1850,10 @@ namespace Microsoft.Boogie {
3 - (default) any
/z3exe:<path>
path to Z3 executable
+
+ CVC4 specific options:
+ /cvc4exe:<path>
+ path to CVC4 executable
");
}
}
diff --git a/Source/Core/Core.csproj b/Source/Core/Core.csproj
index d41fb40b..f3db4f9a 100644
--- a/Source/Core/Core.csproj
+++ b/Source/Core/Core.csproj
@@ -97,6 +97,8 @@
<ErrorReport>prompt</ErrorReport>
<CodeAnalysisRuleSet>Migrated rules for Core.ruleset</CodeAnalysisRuleSet>
<CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
+ <WarningLevel>4</WarningLevel>
+ <Optimize>false</Optimize>
</PropertyGroup>
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|AnyCPU'">
<DebugSymbols>true</DebugSymbols>
@@ -139,6 +141,8 @@
<CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
<CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>
<CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
+ <WarningLevel>4</WarningLevel>
+ <Optimize>false</Optimize>
</PropertyGroup>
<ItemGroup>
<Reference Include="System" />