diff options
| author |  Ally Donaldson <unknown> | 2013-12-02 20:58:30 +0000 |
|---|---|---|
| committer | Ally Donaldson <unknown> | 2013-12-02 20:58:30 +0000 |
| commit | 05b5c647f0ee561a67f3dcfabb1e12e5d018083f (patch) | |
| tree | 0ed7c48ca7eceb145de38a88e0f6fd602cc474a7 /Source/Core | |
| parent | d8e2a6ac4b1607bb2ba3746c97587495af9938e7 (diff) | |
Patch by Nathan Chong: iterative version of remove empty blocks algorithm. This appears to fix a small deficiency in the original recursive implementation, so now a larger number of empty blocks are removed. As a result, various tests produce slightly different counterexamples and have been updated to reflect this. Also, default VC generation strategy has been changed to DAGIterative, to avoid stack overflow problems.
Diffstat (limited to 'Source/Core')
| -rw-r--r-- | Source/Core/VCExp.cs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/Core/VCExp.cs b/Source/Core/VCExp.cs index 32336aac..5a8100a7 100644 --- a/Source/Core/VCExp.cs +++ b/Source/Core/VCExp.cs @@ -197,7 +197,7 @@ The generic options may or may not be used by the prover plugin. public virtual CommandLineOptions.VCVariety DefaultVCVariety {
get {
Contract.Ensures(Contract.Result<CommandLineOptions.VCVariety>() != CommandLineOptions.VCVariety.Unspecified);
- return CommandLineOptions.VCVariety.Dag;
+ return CommandLineOptions.VCVariety.DagIterative;
}
}
|