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 /Test/test2 | |
| 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 'Test/test2')
| -rw-r--r-- | Test/test2/Answer | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/Test/test2/Answer b/Test/test2/Answer index 5c5fb9e0..e75d69f1 100644 --- a/Test/test2/Answer +++ b/Test/test2/Answer @@ -225,7 +225,6 @@ Execution trace: Structured.bpl(246,5): anon6_LoopBody
Structured.bpl(247,7): anon7_LoopBody
Structured.bpl(248,11): anon8_Then
- Structured.bpl(252,5): anon4
Structured.bpl(252,14): anon9_Then
Structured.bpl(303,3): Error BP5001: This assertion might not hold.
Execution trace:
|