1 files changed, 0 insertions, 115 deletions
diff --git a/Test/og/Answer b/Test/og/Answer
deleted file mode 100644
index 4b1bceae..00000000
--- a/Test/og/Answer
+++ /dev/null
@@ -1,115 +0,0 @@
-
--------------------- foo.bpl --------------------
-foo.bpl(30,3): Error: Non-interference check failed
-Execution trace:
-    foo.bpl(7,3): anon0
-    foo.bpl(7,3): anon0$1
-    foo.bpl(14,3): inline$Incr_1$0$this_A
-    (0,0): inline$Impl_YieldChecker_PC_1$1$L0
-
-Boogie program verifier finished with 9 verified, 1 error
-
--------------------- bar.bpl --------------------
-bar.bpl(28,3): Error: Non-interference check failed
-Execution trace:
-    bar.bpl(7,3): anon0
-    bar.bpl(7,3): anon0$1
-    bar.bpl(14,3): inline$Incr_1$0$this_A
-    (0,0): inline$Impl_YieldChecker_PC_1$1$L0
-bar.bpl(28,3): Error: Non-interference check failed
-Execution trace:
-    bar.bpl(38,3): anon0
-    bar.bpl(38,3): anon0$1
-    (0,0): inline$Impl_YieldChecker_PC_1$1$L0
-
-Boogie program verifier finished with 8 verified, 2 errors
-
--------------------- one.bpl --------------------
-
-Boogie program verifier finished with 3 verified, 0 errors
-
--------------------- parallel1.bpl --------------------
-parallel1.bpl(30,3): Error: Non-interference check failed
-Execution trace:
-    parallel1.bpl(7,3): anon0
-    parallel1.bpl(7,3): anon0$1
-    parallel1.bpl(14,3): inline$Incr_1$0$this_A
-    (0,0): inline$Impl_YieldChecker_PC_1$1$L0
-
-Boogie program verifier finished with 7 verified, 1 error
-
--------------------- linear-set.bpl --------------------
-
-Boogie program verifier finished with 4 verified, 0 errors
-
--------------------- linear-set2.bpl --------------------
-
-Boogie program verifier finished with 4 verified, 0 errors
-
--------------------- FlanaganQadeer.bpl --------------------
-
-Boogie program verifier finished with 6 verified, 0 errors
-
--------------------- parallel2.bpl --------------------
-
-Boogie program verifier finished with 8 verified, 0 errors
-
--------------------- parallel4.bpl --------------------
-parallel4.bpl(26,3): Error BP5001: This assertion might not hold.
-Execution trace:
-    (0,0): og_init
-    parallel4.bpl(24,5): anon0$1
-
-Boogie program verifier finished with 5 verified, 1 error
-
--------------------- parallel5.bpl --------------------
-
-Boogie program verifier finished with 8 verified, 0 errors
-
--------------------- akash.bpl --------------------
-
-Boogie program verifier finished with 6 verified, 0 errors
-
--------------------- t1.bpl --------------------
-t1.bpl(60,5): Error: Non-interference check failed
-Execution trace:
-    (0,0): og_init
-    t1.bpl(80,13): anon0
-    t1.bpl(80,13): anon0$1
-    (0,0): inline$SetG_1$0$Entry
-    t1.bpl(80,13): anon0$2
-    (0,0): inline$Impl_YieldChecker_A_1$1$L2
-
-Boogie program verifier finished with 5 verified, 1 error
-
--------------------- new1.bpl --------------------
-
-Boogie program verifier finished with 4 verified, 0 errors
-
--------------------- perm.bpl --------------------
-
-Boogie program verifier finished with 4 verified, 0 errors
-
--------------------- DeviceCache.bpl --------------------
-
-Boogie program verifier finished with 35 verified, 0 errors
-
--------------------- ticket.bpl --------------------
-
-Boogie program verifier finished with 28 verified, 0 errors
-
--------------------- lock.bpl --------------------
-
-Boogie program verifier finished with 8 verified, 0 errors
-
--------------------- lock2.bpl --------------------
-
-Boogie program verifier finished with 8 verified, 0 errors
-
--------------------- multiset.bpl --------------------
-
-Boogie program verifier finished with 85 verified, 0 errors
-
--------------------- civl-paper.bpl --------------------
-
-Boogie program verifier finished with 28 verified, 0 errors