diff options
| author |  Unknown <scmalte@PM-STUD01.d.ethz.ch> | 2011-07-05 14:31:28 +0200 |
|---|---|---|
| committer | Unknown <scmalte@PM-STUD01.d.ethz.ch> | 2011-07-05 14:31:28 +0200 |
| commit | 426d05ebd07ce6eff0605ba3600b4cfa85ed7427 (patch) | |
| tree | 6161c2eb0598b3f43126b46d150b5830c6d25c36 | |
| parent | ac4bedcd7ff6765b996c7c76b34231871eb19973 (diff) | |
Boogie: New cli option -z3exe:"path-to-z3.exe" allowing specifying path to the Z3 version to use
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.csproj | 6 | ||||
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 9 | ||||
| -rw-r--r-- | Source/Provers/Simplify/ProverInterface.cs | 4 | ||||
| -rw-r--r-- | Source/version.cs | 18 | ||||
| -rw-r--r-- | Source/version.ssc | 18 |
5 files changed, 38 insertions, 17 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.csproj b/Source/BoogieDriver/BoogieDriver.csproj index af0926fe..95078433 100644 --- a/Source/BoogieDriver/BoogieDriver.csproj +++ b/Source/BoogieDriver/BoogieDriver.csproj @@ -19,6 +19,8 @@ </FileUpgradeFlags>
<OldToolsVersion>3.5</OldToolsVersion>
<UpgradeBackupLocation />
+ <IsWebBootstrapper>false</IsWebBootstrapper>
+ <TargetFrameworkProfile />
<PublishUrl>publish\</PublishUrl>
<Install>true</Install>
<InstallFrom>Disk</InstallFrom>
@@ -31,17 +33,15 @@ <MapFileExtensions>true</MapFileExtensions>
<ApplicationRevision>0</ApplicationRevision>
<ApplicationVersion>1.0.0.%2a</ApplicationVersion>
- <IsWebBootstrapper>false</IsWebBootstrapper>
<UseApplicationTrust>false</UseApplicationTrust>
<BootstrapperEnabled>true</BootstrapperEnabled>
- <TargetFrameworkProfile />
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
<DebugSymbols>true</DebugSymbols>
<DebugType>full</DebugType>
<Optimize>false</Optimize>
<OutputPath>..\..\Binaries\</OutputPath>
- <DefineConstants>DEBUG;TRACE</DefineConstants>
+ <DefineConstants>TRACE;DEBUG</DefineConstants>
<ErrorReport>prompt</ErrorReport>
<WarningLevel>4</WarningLevel>
<CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 7c26943e..4a9c531b 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -144,6 +144,7 @@ namespace Microsoft.Boogie { public bool UseUncheckedContracts = false;
public bool SimplifyLogFileAppend = false;
public bool SoundnessSmokeTest = false;
+ public string Z3ExecutablePath = null;
private bool noConsistencyChecks = false;
public bool NoConsistencyChecks {
@@ -1388,6 +1389,13 @@ namespace Microsoft.Boogie { }
break;
+ case "-z3exe":
+ case "/z3exe":
+ if (ps.ConfirmArgumentCount(1)) {
+ Z3ExecutablePath = args[ps.i];
+ }
+ break;
+
default:
Contract.Assume(true);
bool option = false;
@@ -2335,6 +2343,7 @@ namespace Microsoft.Boogie { /z3types : generate multi-sorted VC that make use of Z3 types
/z3lets:<n> : 0 - no LETs, 1 - only LET TERM, 2 - only LET FORMULA,
3 - (default) any
+ /z3exe:<path> : path to Z3 executable
");
}
}
diff --git a/Source/Provers/Simplify/ProverInterface.cs b/Source/Provers/Simplify/ProverInterface.cs index 95d8950a..497911ab 100644 --- a/Source/Provers/Simplify/ProverInterface.cs +++ b/Source/Provers/Simplify/ProverInterface.cs @@ -239,6 +239,10 @@ namespace Microsoft.Boogie.Simplify { Contract.Requires(proverExe != null);
Contract.Ensures(_proverPath != null);
+ if (CommandLineOptions.Clo.Z3ExecutablePath != null) {
+ _proverPath = CommandLineOptions.Clo.Z3ExecutablePath;
+ }
+
if (_proverPath == null) {
// Initialize '_proverPath'
_proverPath = Path.Combine(CodebaseString(), proverExe);
diff --git a/Source/version.cs b/Source/version.cs index 2804c330..fd211b1c 100644 --- a/Source/version.cs +++ b/Source/version.cs @@ -1,8 +1,12 @@ -//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
+// ==++==
+//
+//
+//
+// ==--==
+// Warning: Automatically generated file. DO NOT EDIT
+// Generated at Dienstag, 5. Juli 2011 11:26:45
+
using System.Reflection;
-[assembly: AssemblyVersion("2.0.0.0")]
-[assembly: AssemblyFileVersion("2.0.0.0")]
+[assembly: AssemblyVersion("2.2.30705.1126")]
+[assembly: AssemblyFileVersion("2.2.30705.1126")]
+
diff --git a/Source/version.ssc b/Source/version.ssc index 2804c330..fd211b1c 100644 --- a/Source/version.ssc +++ b/Source/version.ssc @@ -1,8 +1,12 @@ -//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
+// ==++==
+//
+//
+//
+// ==--==
+// Warning: Automatically generated file. DO NOT EDIT
+// Generated at Dienstag, 5. Juli 2011 11:26:45
+
using System.Reflection;
-[assembly: AssemblyVersion("2.0.0.0")]
-[assembly: AssemblyFileVersion("2.0.0.0")]
+[assembly: AssemblyVersion("2.2.30705.1126")]
+[assembly: AssemblyFileVersion("2.2.30705.1126")]
+
|