diff options
Diffstat (limited to 'Test/inline/test5.bpl.expect')
| -rw-r--r-- | Test/inline/test5.bpl.expect | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/Test/inline/test5.bpl.expect b/Test/inline/test5.bpl.expect new file mode 100644 index 00000000..cd0530dd --- /dev/null +++ b/Test/inline/test5.bpl.expect @@ -0,0 +1,8 @@ +test5.bpl(39,3): Error BP5001: This assertion might not hold. +Execution trace: + test5.bpl(36,10): anon0 + test5.bpl(30,10): inline$P$0$anon0 + test5.bpl(30,10): inline$P$1$anon0 + test5.bpl(36,10): anon0$2 + +Boogie program verifier finished with 4 verified, 1 error |