fixed some tests in og

added another test in linear (based on bug reported by Chris)
removed the QED build configuration

1 files changed, 5 insertions, 7 deletions

diff --git a/Test/og/termination.bpl b/Test/og/termination.bpl
index 26ff030d..35064f77 100644
--- a/Test/og/termination.bpl
+++ b/Test/og/termination.bpl
@@ -1,17 +1,15 @@
 // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

 // RUN: %diff "%s.expect" "%t"

-// XFAIL: *

-procedure {:yields} X();

-ensures {:atomic 0} |{ A: return true; }|;

+procedure {:yields} {:phase 0} X();

+ensures {:atomic} |{ A: return true; }|;

 

-procedure {:yields} Y();

-ensures {:left 0} |{ A: return true; }|;

+procedure {:yields} {:phase 0} Y();

+ensures {:left} |{ A: return true; }|;

 

-procedure {:yields} main() {

+procedure {:yields} {:phase 1} main() {

   yield;

   call X();

   while (*)

-//  invariant {:terminates} true;

   {

     call Y();

   }