diff options
| author |  rustanleino <unknown> | 2009-11-19 18:51:13 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2009-11-19 18:51:13 +0000 |
| commit | 8a3d35545386c74864db0662faa5c1d68cd71f01 (patch) | |
| tree | f8a033f8b7cac985a5b7f25ee6e7ddee728e679d /Test/inline/Answer | |
| parent | eaf052fa512f87a16d16cbb6b4c78e7fbaaf85b8 (diff) | |
Fixed bug in inlining (procedure *definitions* had been traversed by StandardVisitor while visiting commands).
This solves Issue #6266.
Diffstat (limited to 'Test/inline/Answer')
| -rw-r--r-- | Test/inline/Answer | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/inline/Answer b/Test/inline/Answer index 8f2c34e4..854ac558 100644 --- a/Test/inline/Answer +++ b/Test/inline/Answer @@ -893,7 +893,7 @@ Execution trace: test5.bpl(25,23): inline$P$1$Return
test5.bpl(34,10): anon0$2
-Boogie program verifier finished with 3 verified, 1 error
+Boogie program verifier finished with 4 verified, 1 error
-------------------- test6.bpl --------------------
test6.bpl(1,22): Error: the inlined procedure is recursive, call stack: foo -> foo
test6.bpl(15,22): Error: the inlined procedure is recursive, call stack: foo2 -> foo3 -> foo1 -> foo2
|