more refactoring in stratified inlining

14 files changed, 139 insertions, 157 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index 61943cf0..0911cbd3 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -404,7 +404,7 @@ namespace Microsoft.Boogie {
             inline = true;

           }

         }

-        if (inline && CommandLineOptions.Clo.StratifiedInlining == 0) {

+        if (inline) {

           foreach (var d in TopLevelDeclarations) {

             var impl = d as Implementation;

             if (impl != null) {

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index bdc74152..06c63307 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -2438,6 +2438,10 @@ namespace Microsoft.Boogie {
           }

         }

 

+        if (CommandLineOptions.Clo.StratifiedInlining > 0) {

+          return !QKeyValue.FindBoolAttribute(Attributes, "entrypoint");

+        }

+

         return false;

       }

     }

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index 8f9f7498..e69c38b1 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -52,9 +52,7 @@ namespace VC
               Implementation impl = decl as Implementation;

               if (impl == null) continue;

               Contract.Assert(!impl.Name.StartsWith(recordProcName), "Not allowed to have an implementation for this guy");

-              if (impl.Proc.FindExprAttribute("inline") != null) {

-                implName2StratifiedInliningInfo[impl.Name] = new StratifiedInliningInfo(impl, this);

-              }

+              implName2StratifiedInliningInfo[impl.Name] = new StratifiedInliningInfo(impl, this);

             }

             this.GenerateRecordFunctions();

             PersistCallTree = false;

@@ -136,58 +134,63 @@ namespace VC
             return node;

           }

         }

-        

-        public class StratifiedVC {

-          private static int newVarCount = 0;

-          private static VCExprVar CreateNewVar(ProverInterface prover, Microsoft.Boogie.Type type) {

-            string newName = "StratifiedInlining@" + newVarCnt.ToString();

-            newVarCount++;

-            Constant newVar = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, newName, type));

-            prover.Context.DeclareConstant(newVar, false, null);

-            return prover.VCExprGen.Variable(newVar.Name, type);

-          }

-          private static int idCount = 0;

 

+        private int newVarCount = 0;

+        public VCExprVar CreateNewVar(Microsoft.Boogie.Type type) {

+          string newName = "StratifiedInlining@" + newVarCnt.ToString();

+          newVarCount++;

+          Constant newVar = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, newName, type));

+          prover.Context.DeclareConstant(newVar, false, null);

+          return prover.VCExprGen.Variable(newVar.Name, type);

+        }

+        private int idCount = 1; // 0 is reserved for the VC of main

+        public int CreateNewId() {

+          return idCount++;

+        }

+

+        public class StratifiedVC {

+          StratifiedInliningInfo info;

           int id;

-          Implementation impl;

           List<VCExprVar> interfaceExprVars;

           List<StratifiedCallSite> callSites;

           VCExpr vcexpr;

           public Dictionary<Block, VCExprVar> reachVars;

 

-          public StratifiedVC(StratifiedInliningInfo info, StratifiedVCGen vcgen) {

+          public StratifiedVC(StratifiedInliningInfo siInfo) {

+            info = siInfo;

             if (!info.initialized) {

-              info.GenerateVC(vcgen);

+              info.GenerateVC();

             }

 

-            impl = info.impl;

-            interfaceExprVars = new List<VCExprVar>();

             VCExpr expansion = info.vcexpr;

+            var vcgen = info.vcgen;

             var prover = vcgen.prover;

             VCExpressionGenerator gen = prover.VCExprGen;

             var bet = prover.Context.BoogieExprTranslator;

             VCExpr controlFlowVariableExpr = bet.LookupVariable(info.controlFlowVariable);

-            id = idCount++;

+            id = vcgen.CreateNewId();

             VCExpr eqExpr = gen.Eq(controlFlowVariableExpr, gen.Integer(BigNum.FromInt(id)));

             expansion = gen.And(eqExpr, expansion);

 

+            interfaceExprVars = new List<VCExprVar>();

             Dictionary<VCExprVar, VCExpr> substDict = new Dictionary<VCExprVar, VCExpr>();

             foreach (VCExprVar v in info.interfaceExprVars) {

-              VCExprVar newVar = CreateNewVar(prover, v.Type);

+              VCExprVar newVar = vcgen.CreateNewVar(v.Type);

               interfaceExprVars.Add(newVar);

               substDict.Add(v, newVar);

             }

             foreach (VCExprVar v in info.privateExprVars) {

-              substDict.Add(v, CreateNewVar(prover, v.Type));

+              substDict.Add(v, vcgen.CreateNewVar(v.Type));

             }

             VCExprSubstitution subst = new VCExprSubstitution(substDict, new Dictionary<TypeVariable, Microsoft.Boogie.Type>());

             SubstitutingVCExprVisitor substVisitor = new SubstitutingVCExprVisitor(prover.VCExprGen);

             expansion = substVisitor.Mutate(expansion, subst);

-            

+

+            var impl = info.impl;

             reachVars = new Dictionary<Block, VCExprVar>();

             Dictionary<Block, VCExpr> reachExprs = new Dictionary<Block, VCExpr>();

             foreach (Block b in impl.Blocks) {

-              reachVars[b] = CreateNewVar(prover, Bpl.Type.Bool);

+              reachVars[b] = vcgen.CreateNewVar(Bpl.Type.Bool);

               reachExprs[b] = VCExpressionGenerator.False;

             }

             foreach (Block b in impl.Blocks) {

@@ -209,7 +212,16 @@ namespace VC
             foreach (CallSite cs in info.callSites) {

               callSites.Add(new StratifiedCallSite(cs, substVisitor, subst, reachVars));

             }

+          }

 

+          public VCExpr Attach(StratifiedCallSite stratifiedCallSite) {

+            Contract.Assert(interfaceExprVars.Count == stratifiedCallSite.interfaceExprVars.Count);

+            VCExpressionGenerator gen = info.vcgen.prover.VCExprGen;

+            VCExpr ret = gen.Eq(stratifiedCallSite.reachVar, reachVars[info.impl.Blocks[0]]);

+            for (int i = 0; i < stratifiedCallSite.interfaceExprVars.Count; i++) {

+              ret = gen.And(ret, gen.Eq(stratifiedCallSite.interfaceExprVars[i], interfaceExprVars[i]));

+            }

+            return ret;

           }

         }

 

@@ -225,9 +237,9 @@ namespace VC
         }

 

         public class StratifiedCallSite {

-          CallSite callSite;

-          List<VCExpr> interfaceExprVars;

-          VCExprVar reachVar;

+          public CallSite callSite;

+          public List<VCExpr> interfaceExprVars;

+          public VCExprVar reachVar;

 

           public StratifiedCallSite(CallSite cs, SubstitutingVCExprVisitor substVisitor, VCExprSubstitution subst, Dictionary<Block, VCExprVar> reachVars) {

             callSite = cs;

@@ -240,6 +252,7 @@ namespace VC
         }

 

         public class StratifiedInliningInfo {

+          public StratifiedVCGen vcgen;

           public Implementation impl;

           public Function function;

           public Variable controlFlowVariable;

@@ -252,7 +265,8 @@ namespace VC
           public List<CallSite> callSites;

           public bool initialized;

 

-          public StratifiedInliningInfo(Implementation implementation, StratifiedVCGen vcgen) {

+          public StratifiedInliningInfo(Implementation implementation, StratifiedVCGen stratifiedVcGen) {

+            vcgen = stratifiedVcGen;

             impl = implementation;

 

             VariableSeq functionInterfaceVars = new VariableSeq();

@@ -298,7 +312,7 @@ namespace VC
             initialized = false;

           }

 

-          public void GenerateVC(StratifiedVCGen vcgen) {

+          public void GenerateVC() {

             List<Variable> outputVariables = new List<Variable>();

             assertExpr = new LiteralExpr(Token.NoToken, true);

             foreach (Variable v in impl.OutParams) {

@@ -1054,7 +1068,7 @@ namespace VC
             public ApiChecker checker2;

 

             public VerificationState(VCExpr vcMain, FCallHandler calls, ProverInterface prover, ProverInterface.ErrorHandler reporter) {

-              prover.Assert(vcMain, false); 

+              prover.Assert(vcMain, true); 

               this.calls = calls;

               this.checker = new ApiChecker(prover, reporter);

               vcSize = 0;

@@ -1087,7 +1101,7 @@ namespace VC
             foreach (StratifiedInliningInfo info in implName2StratifiedInliningInfo.Values)

             {

                 Contract.Assert(info != null);

-                info.GenerateVC(this);

+                info.GenerateVC();

             }

 

             // Get the VC of the current procedure

@@ -1285,8 +1299,10 @@ namespace VC
 

         public override Outcome VerifyImplementation(Implementation/*!*/ impl, Program/*!*/ program, VerifierCallback/*!*/ callback)

         {

-            Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

+            if (!QKeyValue.FindBoolAttribute(impl.Attributes, "entrypoint")) 

+              return Outcome.Correct;

             Debug.Assert(this.program == program);

+

             var computeUnderBound = true;

 

             #region stratified inlining options

@@ -1320,11 +1336,12 @@ namespace VC
             }

 

             // Get the VC of the current procedure

-            VCExpr vc;

-            Hashtable/*<int, Absy!>*/ mainLabel2absy;

-            StratifiedInliningErrorReporter reporter;

-            GetVC(impl, program, prover, callback, out vc, out mainLabel2absy, out reporter);

-      

+            StratifiedInliningInfo info = implName2StratifiedInliningInfo[impl.Name];

+            info.GenerateVC();

+            VCExpr vc = info.vcexpr;

+            Hashtable mainLabel2absy = info.label2absy;

+            var reporter = new StratifiedInliningErrorReporter(implName2StratifiedInliningInfo, prover, callback, info.mvInfo, prover.Context, program, impl);

+

             // Find all procedure calls in vc and put labels on them      

             FCallHandler calls = new FCallHandler(prover.VCExprGen, implName2StratifiedInliningInfo, impl.Name, mainLabel2absy);

             calls.setCurrProcAsMain();

@@ -1773,7 +1790,7 @@ namespace VC
                 StratifiedInliningInfo info = implName2StratifiedInliningInfo[procName];

                 if (!info.initialized)

                 {

-                    info.GenerateVC(this);

+                    info.GenerateVC();

                 }

                 //Console.WriteLine("Inlining {0}", procName);

                 VCExpr expansion = cce.NonNull(info.vcexpr);

@@ -1883,7 +1900,7 @@ namespace VC
             }

 

             reporter = new StratifiedInliningErrorReporter(

-               cce.NonNull(implName2StratifiedInliningInfo), prover, callback, mvInfo, prover.Context, gotoCmdOrigins, program, impl);

+               cce.NonNull(implName2StratifiedInliningInfo), prover, callback, mvInfo, prover.Context, program, impl);

         }

 

 

@@ -2467,7 +2484,6 @@ namespace VC
             Program/*!*/ program;

             Implementation/*!*/ mainImpl;

             ProverContext/*!*/ context;

-            Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins;

 

             public bool underapproximationMode;

             public List<int>/*!*/ candidatesToExpand;

@@ -2487,7 +2503,6 @@ namespace VC
 

             public StratifiedInliningErrorReporter(Dictionary<string/*!*/, StratifiedInliningInfo/*!*/>/*!*/ implName2StratifiedInliningInfo,

                                                    ProverInterface/*!*/ theoremProver, VerifierCallback/*!*/ callback, ModelViewInfo mvInfo, ProverContext/*!*/ context,

-                                                   Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins,

                                                    Program/*!*/ program, Implementation/*!*/ mainImpl)

             {

                 Contract.Requires(cce.NonNullDictionaryAndValues(implName2StratifiedInliningInfo));

@@ -2505,7 +2520,6 @@ namespace VC
                 this.underapproximationMode = false;

                 this.calls = null;

                 this.candidatesToExpand = new List<int>();

-                this.gotoCmdOrigins = gotoCmdOrigins;

             }

 

             public void SetCandidateHandler(FCallHandler calls)

@@ -2637,21 +2651,14 @@ namespace VC
               Contract.Assert(CommandLineOptions.Clo.StratifiedInliningWithoutModels || model != null);

 

               candidatesToExpand = new List<int>();

+              var cex = GenerateTraceMain(labels, model, mvInfo);

 

-              if (underapproximationMode) {

-                var cex = GenerateTraceMain(labels, model, mvInfo);

+              if (underapproximationMode && cex != null) {

                 Debug.Assert(candidatesToExpand.All(calls.isSkipped));

-                if (cex != null) {

-                  GetModelWithStates(model);

-                  callback.OnCounterexample(cex, null);

-                  this.PrintModel(model);

-                }

-                return;

+                GetModelWithStates(model);

+                callback.OnCounterexample(cex, null);

+                this.PrintModel(model);

               }

-

-              Contract.Assert(calls != null);

-

-              GenerateTraceMain(labels, model, mvInfo);

             }

 

             // Construct the interprocedural trace

@@ -2663,28 +2670,7 @@ namespace VC
               }

 

               orderedStateIds = new List<Tuple<int, int>>();

-              Counterexample newCounterexample =

-               GenerateTrace(labels, errModel, 0, mainImpl);

-

-              if (newCounterexample == null)

-                return null;

-

-              #region Map passive program errors back to original program errors

-              ReturnCounterexample returnExample = newCounterexample as ReturnCounterexample;

-              if (returnExample != null && gotoCmdOrigins != null) {

-                foreach (Block b in returnExample.Trace) {

-                  Contract.Assert(b != null);

-                  Contract.Assume(b.TransferCmd != null);

-                  ReturnCmd cmd = (ReturnCmd)gotoCmdOrigins[b.TransferCmd];

-                  if (cmd != null) {

-                    returnExample.FailingReturn = cmd;

-                    break;

-                  }

-                }

-              }

-              #endregion

-

-              return newCounterexample;

+              return GenerateTrace(labels, errModel, 0, mainImpl);

             }

 

             private Counterexample GenerateTrace(IList<string/*!*/>/*!*/ labels, Model/*!*/ errModel,

diff --git a/Test/stratifiedinline/Answer b/Test/stratifiedinline/Answer
index 77b00b19..dd5344e8 100644
--- a/Test/stratifiedinline/Answer
+++ b/Test/stratifiedinline/Answer
@@ -1,8 +1,7 @@
 ----- Running regression test bar1.bpl

-bar1.bpl(25,1): Error BP5003: A postcondition might not hold on this return path.

-bar1.bpl(21,1): Related location: This is the postcondition that might not hold.

+(0,0): Error BP5001: This assertion might not hold.

 Execution trace:

-    bar1.bpl(24,3): anon0

+    bar1.bpl(22,3): anon0

     Inlined call to procedure foo begins

         bar1.bpl(13,5): anon0

         Inlined call to procedure bar begins

@@ -16,25 +15,24 @@ Execution trace:
 Boogie program verifier finished with 0 verified, 1 error

 -----

 ----- Running regression test bar2.bpl

-bar2.bpl(21,3): Error BP5001: This assertion might not hold.

+(0,0): Error BP5001: This assertion might not hold.

 Execution trace:

-    bar2.bpl(19,3): anon0

+    bar2.bpl(18,3): anon0

     Inlined call to procedure foo begins

-        bar2.bpl(5,3): anon0

-        bar2.bpl(9,7): anon3_Else

+        bar2.bpl(4,3): anon0

+        bar2.bpl(5,7): anon3_Then

     Inlined call to procedure foo ends

     Inlined call to procedure foo begins

-        bar2.bpl(5,3): anon0

-        bar2.bpl(6,7): anon3_Then

+        bar2.bpl(4,3): anon0

+        bar2.bpl(8,7): anon3_Else

     Inlined call to procedure foo ends

 

 Boogie program verifier finished with 0 verified, 1 error

 -----

 ----- Running regression test bar3.bpl

-bar3.bpl(41,1): Error BP5003: A postcondition might not hold on this return path.

-bar3.bpl(34,1): Related location: This is the postcondition that might not hold.

+(0,0): Error BP5001: This assertion might not hold.

 Execution trace:

-    bar3.bpl(38,3): anon0

+    bar3.bpl(35,3): anon0

     Inlined call to procedure foo begins

         bar3.bpl(18,3): anon0

         bar3.bpl(19,7): anon3_Then

@@ -63,7 +61,7 @@ Boogie program verifier finished with 1 verified, 0 errors
 Boogie program verifier finished with 1 verified, 0 errors

 -----

 ----- Running regression test bar7.bpl

-bar7.bpl(42,3): Error BP5001: This assertion might not hold.

+(0,0): Error BP5001: This assertion might not hold.

 Execution trace:

     bar7.bpl(35,5): anon0

     bar7.bpl(37,5): anon4_Then

@@ -156,7 +154,7 @@ Execution trace:
 Boogie program verifier finished with 0 verified, 1 error

 -----

 ----- Running regression test bar8.bpl

-bar8.bpl(41,3): Error BP5001: This assertion might not hold.

+(0,0): Error BP5001: This assertion might not hold.

 Execution trace:

     bar8.bpl(34,5): anon0

     bar8.bpl(36,5): anon4_Then

@@ -249,7 +247,7 @@ Execution trace:
 Boogie program verifier finished with 0 verified, 1 error

 -----

 ----- Running regression test bar9.bpl

-bar9.bpl(44,3): Error BP5001: This assertion might not hold.

+(0,0): Error BP5001: This assertion might not hold.

 Execution trace:

     bar9.bpl(35,5): anon0

     bar9.bpl(41,5): anon4_Else

@@ -386,7 +384,7 @@ Execution trace:
 Boogie program verifier finished with 0 verified, 1 error

 -----

 ----- Running regression test bar10.bpl

-bar10.bpl(40,3): Error BP5001: This assertion might not hold.

+(0,0): Error BP5001: This assertion might not hold.

 Execution trace:

     bar10.bpl(35,5): anon0

     Inlined call to procedure bar1 begins

@@ -485,10 +483,9 @@ Execution trace:
 Boogie program verifier finished with 0 verified, 1 error

 -----

 ----- Running regression test bar11.bpl

-bar11.bpl(31,1): Error BP5003: A postcondition might not hold on this return path.

-bar11.bpl(26,1): Related location: This is the postcondition that might not hold.

+(0,0): Error BP5001: This assertion might not hold.

 Execution trace:

-    bar11.bpl(30,3): anon0

+    bar11.bpl(26,3): anon0

     Inlined call to procedure foo begins

         bar11.bpl(15,3): anon0

         value = 0

diff --git a/Test/stratifiedinline/bar1.bpl b/Test/stratifiedinline/bar1.bpl
index 845954d5..bd210f70 100644
--- a/Test/stratifiedinline/bar1.bpl
+++ b/Test/stratifiedinline/bar1.bpl
@@ -1,13 +1,13 @@
 var x: int;

 var y: int;

 

-procedure {:inline 1} bar()

+procedure bar()

 modifies y;

 {

   y := y + 1;

 }

 

-procedure {:inline 1} foo() 

+procedure foo() 

 modifies x, y;

 {

   x := x + 1;

@@ -16,11 +16,11 @@ modifies x, y;
   x := x + 1;

 }

 

-procedure main()

-requires x == y;

-ensures x != y;

+procedure {:entrypoint} main()

 modifies x, y;

 {

+  assume x == y;

   call foo();

+  assume x == y;

 }

 

diff --git a/Test/stratifiedinline/bar10.bpl b/Test/stratifiedinline/bar10.bpl
index 8cfcfc13..ab1e4748 100644
--- a/Test/stratifiedinline/bar10.bpl
+++ b/Test/stratifiedinline/bar10.bpl
@@ -1,7 +1,7 @@
 var i: int;

 var m: int;

 

-procedure {:inline 1} foo()

+procedure foo()

 modifies i;

 {

   if (i < 20) {

@@ -10,7 +10,7 @@ modifies i;
   }

 }

 

-procedure {:inline 1} bar1(j: int) 

+procedure bar1(j: int) 

 modifies i;

 {

   if (j < 2*m) 

@@ -20,7 +20,7 @@ modifies i;
   }

 }

 

-procedure {:inline 1} bar2(j: int) 

+procedure bar2(j: int) 

 modifies i;

 {

   if (j < m) {

@@ -29,7 +29,7 @@ modifies i;
   }

 }

 

-procedure main() 

+procedure {:entrypoint} main() 

 modifies i;

 {

   i := 0;

@@ -37,5 +37,5 @@ modifies i;
   call bar2(0);

   i := 0;

   call foo();

-  assert i < 10;

+  assume !(i < 10);

 }
\ No newline at end of file
diff --git a/Test/stratifiedinline/bar11.bpl b/Test/stratifiedinline/bar11.bpl
index baad27a1..67e21ba6 100644
--- a/Test/stratifiedinline/bar11.bpl
+++ b/Test/stratifiedinline/bar11.bpl
@@ -2,14 +2,14 @@ var x: int;
 var y: int;

 procedure boogie_si_record_int(x:int);

 

-procedure {:inline 1} bar()

+procedure bar()

 modifies y;

 {

   y := y + 1;

   call boogie_si_record_int(y);

 }

 

-procedure {:inline 1} foo() 

+procedure foo() 

 modifies x, y;

 {

   call boogie_si_record_int(x);

@@ -20,13 +20,12 @@ modifies x, y;
   call boogie_si_record_int(x);

 }

 

-procedure main()

-requires x == 0;

-requires x == y;

-ensures x != y;

+procedure {:entrypoint} main()

 modifies x, y;

 {

-

+  assume x == 0;

+  assume x == y;

   call foo();

+  assume x == y;

 }

 

diff --git a/Test/stratifiedinline/bar2.bpl b/Test/stratifiedinline/bar2.bpl
index 76991a8f..6c383591 100644
--- a/Test/stratifiedinline/bar2.bpl
+++ b/Test/stratifiedinline/bar2.bpl
@@ -1,5 +1,4 @@
-

-procedure {:inline 1} foo() returns (x: bool)

+procedure foo() returns (x: bool)

 {

   var b: bool;

   if (b) {

@@ -11,14 +10,14 @@ procedure {:inline 1} foo() returns (x: bool)
   }

 }

 

-procedure main()

+procedure {:entrypoint} main()

 {

   var b1: bool;

   var b2: bool;

 

   call b1 := foo();

   call b2 := foo();

-  assert b1 == b2;

+  assume b1 != b2;

 }

 

 

diff --git a/Test/stratifiedinline/bar3.bpl b/Test/stratifiedinline/bar3.bpl
index 7bd91184..a1f0bea3 100644
--- a/Test/stratifiedinline/bar3.bpl
+++ b/Test/stratifiedinline/bar3.bpl
@@ -1,7 +1,7 @@
 var y: int;

 var x: int;

 

-procedure {:inline 1} bar(b: bool)

+procedure bar(b: bool)

 modifies y;

 {

   if (b) {

@@ -11,7 +11,7 @@ modifies y;
   }

 }

 

-procedure {:inline 1} foo() 

+procedure foo() 

 modifies x, y;

 {

   var b: bool;

@@ -29,13 +29,11 @@ modifies x, y;
 }

 

 

-procedure main()

-requires x == y;

-ensures x == y;

+procedure {:entrypoint} main()

 modifies x, y;

-modifies y;

 {

+  assume x == y;

   call foo();

-  assert x == y;

   call bar(false);

+  assume x != y;

 }

diff --git a/Test/stratifiedinline/bar4.bpl b/Test/stratifiedinline/bar4.bpl
index 84640811..4b3a6ee2 100644
--- a/Test/stratifiedinline/bar4.bpl
+++ b/Test/stratifiedinline/bar4.bpl
@@ -1,7 +1,7 @@
 var y: int;

 var x: int;

 

-procedure {:inline 1} bar() returns (b: bool)

+procedure bar() returns (b: bool)

 modifies y;

 {

   if (b) {

@@ -11,7 +11,7 @@ modifies y;
   }

 }

 

-procedure {:inline 1} foo() 

+procedure foo() 

 modifies x, y;

 {

   var b: bool;

@@ -25,14 +25,13 @@ modifies x, y;
 }

 

 

-procedure main() returns (b: bool)

-requires x == y;

-ensures !b ==> x == y+1;

-ensures b ==> x+1 == y;

+procedure {:entrypoint} main() returns (b: bool)

 modifies x, y;

-modifies y;

 {

+  assume x == y;

   call foo();

-  assert x == y;

-  call b := bar();

+  if (x == y) {

+    call b := bar();

+    assume (if b then x+1 != y else x != y+1);

+  }

 }

diff --git a/Test/stratifiedinline/bar6.bpl b/Test/stratifiedinline/bar6.bpl
index e133aef7..dd528f6f 100644
--- a/Test/stratifiedinline/bar6.bpl
+++ b/Test/stratifiedinline/bar6.bpl
@@ -1,6 +1,6 @@
 var M: [int]int;

 

-procedure {:inline 1} bar(y: int) returns (b: bool)

+procedure bar(y: int) returns (b: bool)

 modifies M;

 {

   if (b) {

@@ -10,7 +10,7 @@ modifies M;
   }

 }

 

-procedure {:inline 1} foo(x: int, y: int) 

+procedure foo(x: int, y: int) 

 modifies M;

 {

   var b: bool;

@@ -23,14 +23,14 @@ modifies M;
   }

 }

 

-procedure main(x: int, y: int) returns (b: bool)

-requires x != y;

-requires M[x] == M[y];

-ensures !b ==> M[x] == M[y]+1;

-ensures b ==> M[x]+1 == M[y];

+procedure {:entrypoint} main(x: int, y: int) returns (b: bool)

 modifies M;

 {

+  assume x != y;

+  assume M[x] == M[y];

   call foo(x, y);

-  assert M[x] == M[y];

-  call b := bar(y);

+  if (M[x] == M[y]) {

+    call b := bar(y);

+    assume (if b then M[x]+1 != M[y] else M[x] != M[y]+1);

+  }

 }

diff --git a/Test/stratifiedinline/bar7.bpl b/Test/stratifiedinline/bar7.bpl
index b28777bd..41cf612e 100644
--- a/Test/stratifiedinline/bar7.bpl
+++ b/Test/stratifiedinline/bar7.bpl
@@ -1,7 +1,7 @@
 var i: int;

 var m: int;

 

-procedure {:inline 1} foo()

+procedure foo()

 modifies i;

 {

   if (i < 20) {

@@ -10,7 +10,7 @@ modifies i;
   }

 }

 

-procedure {:inline 1} bar1(j: int) 

+procedure bar1(j: int) 

 modifies i;

 {

   if (j < 2*m) 

@@ -20,7 +20,7 @@ modifies i;
   }

 }

 

-procedure {:inline 1} bar2(j: int) 

+procedure bar2(j: int) 

 modifies i;

 {

   if (j < m) {

@@ -29,7 +29,7 @@ modifies i;
   }

 }

 

-procedure main() 

+procedure {:entrypoint} main() 

 modifies i;

 {

   i := 0;

@@ -39,5 +39,5 @@ modifies i;
     call bar1(0);

     call bar2(0);

   }

-  assert i < 10;

+  assume !(i < 10);

 }
\ No newline at end of file
diff --git a/Test/stratifiedinline/bar8.bpl b/Test/stratifiedinline/bar8.bpl
index e96655f3..356645e6 100644
--- a/Test/stratifiedinline/bar8.bpl
+++ b/Test/stratifiedinline/bar8.bpl
@@ -1,7 +1,7 @@
 var i: int;

 var m: int;

 

-procedure {:inline 1} foo() 

+procedure foo() 

 modifies i;

 {

   if (i < 20) {

@@ -10,7 +10,7 @@ modifies i;
   }

 }

 

-procedure {:inline 1} bar1(j: int) 

+procedure bar1(j: int) 

 modifies i;

 {

   if (j < 2*m) {

@@ -19,7 +19,7 @@ modifies i;
   }

 }

 

-procedure {:inline 1} bar2(j: int) 

+procedure bar2(j: int) 

 modifies i;

 {

   if (j < m) {

@@ -28,7 +28,7 @@ modifies i;
   }

 }

 

-procedure main()

+procedure {:entrypoint} main()

 modifies i;

 {

   i := 0;

@@ -38,5 +38,5 @@ modifies i;
     call bar1(0);

     call bar2(0);

   }

-  assert i < 10;

+  assume !(i < 10);

 }
\ No newline at end of file
diff --git a/Test/stratifiedinline/bar9.bpl b/Test/stratifiedinline/bar9.bpl
index 12de78ad..d1eacb18 100644
--- a/Test/stratifiedinline/bar9.bpl
+++ b/Test/stratifiedinline/bar9.bpl
@@ -1,7 +1,7 @@
 var i: int;

 var m: int;

 

-procedure {:inline 1} foo(x: int)

+procedure foo(x: int)

 modifies i;

 {

   if (i < x) {

@@ -10,7 +10,7 @@ modifies i;
   }

 }

 

-procedure {:inline 1} bar1(j: int) 

+procedure bar1(j: int) 

 modifies i;

 {

   if (j < 2*m) 

@@ -20,7 +20,7 @@ modifies i;
   }

 }

 

-procedure {:inline 1} bar2(j: int) 

+procedure bar2(j: int) 

 modifies i;

 {

   if (j < m) {

@@ -29,7 +29,7 @@ modifies i;
   }

 }

 

-procedure main() 

+procedure {:entrypoint} main() 

 modifies i;

 {

   i := 0;

@@ -41,5 +41,5 @@ modifies i;
     call bar1(0);

     call bar2(0);

   }

-  assert i < 10;

+  assume !(i < 10);

 }
\ No newline at end of file