diff options
| author |  qadeer <unknown> | 2013-12-07 12:58:21 -0800 |
|---|---|---|
| committer | qadeer <unknown> | 2013-12-07 12:58:21 -0800 |
| commit | c3ee2495b6c696c07e4ddb917ac3d520229bced7 (patch) | |
| tree | 17ac652bd969d96dedfd08b50d537fd73e85a9ba /Test/og/Answer | |
| parent | ba2a4e6f8b6191386000521306136b88b07525fc (diff) | |
fixed a bug regarding invocation of modsetanalysis w.r.t. OG desugaring
Diffstat (limited to 'Test/og/Answer')
| -rw-r--r-- | Test/og/Answer | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Test/og/Answer b/Test/og/Answer index 1d516066..d4111927 100644 --- a/Test/og/Answer +++ b/Test/og/Answer @@ -62,7 +62,7 @@ Boogie program verifier finished with 4 verified, 0 errors -------------------- parallel4.bpl --------------------
parallel4.bpl(18,3): Error BP5001: This assertion might not hold.
Execution trace:
- parallel4.bpl(16,5): anon0
+ (0,0): og_init
parallel4.bpl(16,5): anon0$1
Boogie program verifier finished with 2 verified, 1 error
@@ -86,7 +86,7 @@ Boogie program verifier finished with 3 verified, 0 errors -------------------- t1.bpl --------------------
t1.bpl(35,5): Error BP5001: This assertion might not hold.
Execution trace:
- t1.bpl(53,13): anon0
+ (0,0): og_init
(0,0): inline$Impl_YieldChecker_A$0$L1
Boogie program verifier finished with 2 verified, 1 error
|