diff options
| author |  Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2013-05-18 21:15:20 -0700 |
|---|---|---|
| committer | Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2013-05-18 21:15:20 -0700 |
| commit | 64d8963508ce048d00db3766f4ca597b792c1b95 (patch) | |
| tree | 67801fe71cd2ceb7eb851833dd489751baa21ce2 /Test/og/Answer | |
| parent | 89b20adf23750478098578895fef9ca3b9170927 (diff) | |
reworked the linear and og implementation based on available variables theory
Diffstat (limited to 'Test/og/Answer')
| -rw-r--r-- | Test/og/Answer | 24 |
1 files changed, 14 insertions, 10 deletions
diff --git a/Test/og/Answer b/Test/og/Answer index 9df32aee..c29d38dc 100644 --- a/Test/og/Answer +++ b/Test/og/Answer @@ -60,11 +60,10 @@ Boogie program verifier finished with 5 verified, 0 errors Boogie program verifier finished with 4 verified, 0 errors
-------------------- parallel4.bpl --------------------
-parallel4.bpl(14,3): Error BP5001: This assertion might not hold.
+parallel4.bpl(18,3): Error BP5001: This assertion might not hold.
Execution trace:
- parallel4.bpl(12,3): anon0
- (0,0): inline$og_yield$0$Return
- parallel4.bpl(12,3): anon0$1
+ parallel4.bpl(16,5): anon0
+ parallel4.bpl(16,5): anon0$1
Boogie program verifier finished with 2 verified, 1 error
@@ -85,12 +84,17 @@ Boogie program verifier finished with 1 verified, 0 errors Boogie program verifier finished with 3 verified, 0 errors
-------------------- t1.bpl --------------------
-t1.bpl(25,5): Error BP5001: This assertion might not hold.
+t1.bpl(35,5): Error BP5001: This assertion might not hold.
Execution trace:
- t1.bpl(11,5): anon0
- (0,0): inline$Proc_YieldChecker_B$0$Return
- (0,0): inline$og_yield$0$L_0$1
- (0,0): inline$og_yield$0$Return
- t1.bpl(11,5): anon0$1
+ t1.bpl(53,13): anon0
+ (0,0): inline$Impl_YieldChecker_A$0$L1
Boogie program verifier finished with 2 verified, 1 error
+
+-------------------- new1.bpl --------------------
+
+Boogie program verifier finished with 2 verified, 0 errors
+
+-------------------- perm.bpl --------------------
+
+Boogie program verifier finished with 2 verified, 0 errors
|