From 8d7686cd88736d117e37eb9bf9dd17404a294ff4 Mon Sep 17 00:00:00 2001 From: Unknown Date: Wed, 3 Oct 2012 12:32:19 -0700 Subject: bunch of refactorings - moved doomed and predication code into separate projects; for doomed there is a static dependency from BoogieDriver but for predication even that dependency has been eliminated - deleted Provers\Simplify and Provers\Z3 - removed Provers\Z3api from the solution - consolidated Core\GraphAlgorithms.cs VCGeneration\GraphAlgorithms.cs into Graph\Graph.cs --- Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) (limited to 'Util') 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; } -- cgit v1.2.3