diff options
| author |  Unknown <shuvendu@SHUVENDU-Z400.redmond.corp.microsoft.com> | 2012-06-01 01:36:11 -0700 |
|---|---|---|
| committer | Unknown <shuvendu@SHUVENDU-Z400.redmond.corp.microsoft.com> | 2012-06-01 01:36:11 -0700 |
| commit | 7552293514e40a6dcd9749d3668519d7d32049d5 (patch) | |
| tree | 2ae7fec112e8228b808d652e07b6bd19d4722a4a /Test/extractloops/Answer | |
| parent | 622c64cbbba5d3619eaf4de03458111ff6589027 (diff) | |
1. Fix for free ensures in inlined procedures. Becomes a skip instead of an assume.
2. Fix for deterministic loop extraction, and a new regression.
3. All regressions (including Dafny) except houdini pass, it is most likely related to the free ensures change.
Diffstat (limited to 'Test/extractloops/Answer')
| -rw-r--r-- | Test/extractloops/Answer | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/Test/extractloops/Answer b/Test/extractloops/Answer index b9083fae..48ca65e9 100644 --- a/Test/extractloops/Answer +++ b/Test/extractloops/Answer @@ -88,3 +88,8 @@ Stratified Inlining: Reached recursion bound of 4 Boogie program verifier finished with 1 verified, 0 errors
-----
+----- Running regression test detLoopExtract1.bpl with deterministicExtractLoops
+Stratified Inlining: Reached recursion bound of 4
+
+Boogie program verifier finished with 1 verified, 0 errors
+-----
|