updated test

1 files changed, 5 insertions, 9 deletions

diff --git a/Test/extractloops/t2.bpl b/Test/extractloops/t2.bpl
index d0011929..93f80f20 100644
--- a/Test/extractloops/t2.bpl
+++ b/Test/extractloops/t2.bpl
@@ -1,22 +1,20 @@
 var g: int;

 

-procedure A();

-  requires g == 0;

-  modifies g;

 

-procedure {:inline 1} {:verify false} foo(); 

-

-implementation foo() {

+procedure foo()

+{

   var t: int;

   t := 0;

 }

 

-implementation A()

+procedure {:entrypoint} A()

+modifies g;

 {

   var x: int;

   var y: int;

 

   anon0:

+    assume g == 0;

     x := 4;

     goto anon3_LoopHead;

 

@@ -48,8 +46,6 @@ implementation A()
     goto anon2;

 

   anon2:

-    assert false;

-    assert x == 1;

     return;

 }