diff options
| author |  qadeer <qadeer@microsoft.com> | 2011-11-16 11:40:16 -0800 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2011-11-16 11:40:16 -0800 |
| commit | f99b8c0a6af826c2b74f1b4143520e080453e033 (patch) | |
| tree | 9e3aad9a2ce558f88a4bc064faa31c55cbe94427 | |
| parent | 1fc8bd36cc4320fa6a7796c05f6805ecb3594fc8 (diff) | |
Eliminated unused argument in the constructor for Checker
| -rw-r--r-- | Source/Houdini/Checker.cs | 2 | ||||
| -rw-r--r-- | Source/VCGeneration/Check.cs | 2 | ||||
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs index 97c22cc9..519a01af 100644 --- a/Source/Houdini/Checker.cs +++ b/Source/Houdini/Checker.cs @@ -50,7 +50,7 @@ namespace Microsoft.Boogie.Houdini { ModelViewInfo mvInfo;
Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = PassifyImpl(impl, program, out mvInfo);
Hashtable/*<int, Absy!>*/ label2absy;
- checker = new Checker(this, program, logFilePath, appendLogFile, impl, CommandLineOptions.Clo.ProverKillTime);
+ checker = new Checker(this, program, logFilePath, appendLogFile, CommandLineOptions.Clo.ProverKillTime);
if (!(checker.TheoremProver is Z3ProcessTheoremProver || checker.TheoremProver is SMTLibProcessTheoremProver)) {
throw new Exception("HdnChecker only works with z3");
}
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index 7b623bce..8e92c239 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -101,7 +101,7 @@ namespace Microsoft.Boogie { /// <summary>
/// Constructor. Initialize a checker with the program and log file.
/// </summary>
- public Checker(VC.ConditionGeneration vcgen, Program prog, string/*?*/ logFilePath, bool appendLogFile, Implementation impl, int timeout) {
+ public Checker(VC.ConditionGeneration vcgen, Program prog, string/*?*/ logFilePath, bool appendLogFile, int timeout) {
Contract.Requires(vcgen != null);
Contract.Requires(prog != null);
this.timeout = timeout;
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index a52a7087..b8645cb0 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -894,7 +894,7 @@ namespace VC { string log = logFilePath;
if (log != null && !log.Contains("@PROC@") && checkers.Count > 0)
log = log + "." + checkers.Count;
- Checker ch = new Checker(this, program, log, appendLogFile, impl, timeout);
+ Checker ch = new Checker(this, program, log, appendLogFile, timeout);
Contract.Assert(ch != null);
checkers.Add(ch);
return ch;
|