summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--DafnyDriver/DafnyDriver.cs8
-rw-r--r--Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs6
2 files changed, 2 insertions, 12 deletions
diff --git a/DafnyDriver/DafnyDriver.cs b/DafnyDriver/DafnyDriver.cs
index 39733c8e..80f78d16 100644
--- a/DafnyDriver/DafnyDriver.cs
+++ b/DafnyDriver/DafnyDriver.cs
@@ -571,13 +571,7 @@ namespace Microsoft.Dafny
ConditionGeneration vcgen = null;
try
{
- if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed)
- {
- vcgen = new DCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
- } else
- {
- vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
- }
+ vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
}
catch (ProverException e)
{
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs
index c691d9da..39829bb0 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs
@@ -255,11 +255,7 @@ namespace DafnyLanguage
ConditionGeneration vcgen = null;
try {
- if (Bpl.CommandLineOptions.Clo.vcVariety == Bpl.CommandLineOptions.VCVariety.Doomed) {
- vcgen = new DCGen(program, Bpl.CommandLineOptions.Clo.SimplifyLogFilePath, Bpl.CommandLineOptions.Clo.SimplifyLogFileAppend);
- } else {
- vcgen = new VCGen(program, Bpl.CommandLineOptions.Clo.SimplifyLogFilePath, Bpl.CommandLineOptions.Clo.SimplifyLogFileAppend);
- }
+ vcgen = new VCGen(program, Bpl.CommandLineOptions.Clo.SimplifyLogFilePath, Bpl.CommandLineOptions.Clo.SimplifyLogFileAppend);
} catch (Bpl.ProverException) {
return PipelineOutcome.FatalError;
}