diff options
| author |  qadeer <unknown> | 2012-02-23 23:32:00 -0800 |
|---|---|---|
| committer | qadeer <unknown> | 2012-02-23 23:32:00 -0800 |
| commit | 44cc8ee3486a320aae809bc4755f4da8c4de4b79 (patch) | |
| tree | 8955f708bb69f407640ca7ccf85e5dbff98abcfb /Source/BoogieDriver | |
| parent | 88a325c862048ab6d487fc8f5d6fcba3602960df (diff) | |
bug fixes related to using ControlFlowFunction instead of labels
Diffstat (limited to 'Source/BoogieDriver')
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index d5a98913..c2c09ded 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -443,6 +443,11 @@ namespace Microsoft.Boogie { Contract.Ensures(0 <= Contract.ValueAtReturn(out inconclusives) && 0 <= Contract.ValueAtReturn(out timeOuts));
errorCount = verified = inconclusives = timeOuts = outOfMemories = 0;
+ CommandLineOptions.Clo.UseLabels =
+ CommandLineOptions.Clo.UseLabels ||
+ CommandLineOptions.Clo.SoundnessSmokeTest ||
+ !(CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Dag ||
+ CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.DagIterative);
// ---------- Infer invariants --------------------------------------------------------
|