Merge

20 files changed, 631 insertions, 381 deletions

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index d1b7f43c..b422e836 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -131,6 +131,7 @@ namespace BytecodeTranslator
           this.Traverse(instance);

           Bpl.Expr instanceExpr = TranslatedExpressions.Pop();

           Bpl.IdentifierExpr temp = Bpl.Expr.Ident(this.sink.CreateFreshLocal(field.ResolvedField.Type));

+          AssertOrAssumeNonNull(Bpl.Token.NoToken, instanceExpr);

           this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(temp, this.sink.Heap.ReadHeap(instanceExpr, f, field.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap, temp.Type)));

           TranslatedExpressions.Push(temp);

         } 

@@ -196,15 +197,25 @@ namespace BytecodeTranslator
 

     public override void TraverseChildren(IArrayIndexer arrayIndexer) {

 

-      if (!IsAtomicInstance(arrayIndexer.IndexedObject)) {

-        // Simplify the BE so that all nested dereferences and method calls are broken up into separate assignments to locals.

-        var se = ExpressionSimplifier.Simplify(this.sink, arrayIndexer);

-        this.Traverse(se);

-        return;

-      }

+      //if (!IsAtomicInstance(arrayIndexer.IndexedObject)) {

+      //  // Simplify the BE so that all nested dereferences and method calls are broken up into separate assignments to locals.

+      //  var se = ExpressionSimplifier.Simplify(this.sink, arrayIndexer);

+      //  this.Traverse(se);

+      //  return;

+      //}

 

       this.Traverse(arrayIndexer.IndexedObject);

       Bpl.Expr arrayExpr = TranslatedExpressions.Pop();

+

+      var be = arrayIndexer.IndexedObject as IBoundExpression;

+      if (be != null && be.Instance != null) {

+        var l = this.sink.CreateFreshLocal(be.Type);

+        var lhs = Bpl.Expr.Ident(l);

+        var cmd = Bpl.Cmd.SimpleAssign(arrayIndexer.Token(), lhs, arrayExpr);

+        this.StmtTraverser.StmtBuilder.Add(cmd);

+        arrayExpr = lhs;

+      }

+

       this.Traverse(arrayIndexer.Indices);

       int count = arrayIndexer.Indices.Count();

       Bpl.Expr[] indexExprs = new Bpl.Expr[count];

@@ -220,6 +231,7 @@ namespace BytecodeTranslator
         indexExpr = new Bpl.NAryExpr(arrayIndexer.Token(), new Bpl.FunctionCall(f), new Bpl.ExprSeq(indexExprs));

       }

 

+      AssertOrAssumeNonNull(arrayIndexer.Token(), arrayExpr);

       this.TranslatedExpressions.Push(this.sink.Heap.ReadHeap(arrayExpr, indexExpr, AccessType.Array, this.sink.CciTypeToBoogie(arrayIndexer.Type)));

     }

 

@@ -237,11 +249,24 @@ namespace BytecodeTranslator
     public override void TraverseChildren(IBoundExpression boundExpression)

     {

 

-      if (boundExpression.Instance != null && !IsAtomicInstance(boundExpression.Instance)) {

-        // Simplify the BE so that all nested dereferences and method calls are broken up into separate assignments to locals.

-        var se = ExpressionSimplifier.Simplify(this.sink, boundExpression);

-        this.Traverse(se);

-        return;

+      //if (boundExpression.Instance != null && !IsAtomicInstance(boundExpression.Instance)) {

+      //  // Simplify the BE so that all nested dereferences and method calls are broken up into separate assignments to locals.

+      //  var se = ExpressionSimplifier.Simplify(this.sink, boundExpression);

+      //  this.Traverse(se);

+      //  return;

+      //}

+

+      if (boundExpression.Instance != null) {

+        this.Traverse(boundExpression.Instance);

+        var nestedBE = boundExpression.Instance as IBoundExpression;

+        if (nestedBE != null) {

+          var l = this.sink.CreateFreshLocal(nestedBE.Type);

+          var e = this.TranslatedExpressions.Pop();

+          var lhs = Bpl.Expr.Ident(l);

+          var cmd = Bpl.Cmd.SimpleAssign(boundExpression.Token(), lhs, e);

+          this.StmtTraverser.StmtBuilder.Add(cmd);

+          this.TranslatedExpressions.Push(lhs);

+        }

       }

 

       #region Local

@@ -270,10 +295,13 @@ namespace BytecodeTranslator
         if (instance == null) {

           TranslatedExpressions.Push(f);

         } else {

-          this.Traverse(instance);

+//          this.Traverse(instance);

           Bpl.Expr instanceExpr = TranslatedExpressions.Pop();

           var bplType = this.sink.CciTypeToBoogie(field.Type);

           var e = this.sink.Heap.ReadHeap(instanceExpr, f, field.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap, bplType);

+

+          AssertOrAssumeNonNull(boundExpression.Token(), instanceExpr);

+

           this.TranslatedExpressions.Push(e);

         }

         return;

@@ -320,6 +348,20 @@ namespace BytecodeTranslator
       #endregion

     }

 

+    private void AssertOrAssumeNonNull(Bpl.IToken token, Bpl.Expr instance) {

+      if (this.sink.Options.dereference != Options.Dereference.None) {

+        Bpl.Cmd c;

+        var n = Bpl.Expr.Ident(this.sink.Heap.NullRef);

+        var neq = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, instance, n);

+        if (this.sink.Options.dereference == Options.Dereference.Assume) {

+          c = new Bpl.AssumeCmd(token, neq);

+        } else {

+          c = new Bpl.AssertCmd(token, neq);

+        }

+        this.StmtTraverser.StmtBuilder.Add(c);

+      }

+    }

+

     internal static bool IsAtomicInstance(IExpression expression) {

       var thisInst = expression as IThisReference;

       if (thisInst != null) return true;

@@ -695,6 +737,7 @@ namespace BytecodeTranslator
         this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(local), Bpl.Expr.Ident(eventVar)));

         inexpr.Insert(0, Bpl.Expr.Ident(local));

       } else {

+        AssertOrAssumeNonNull(methodCallToken, thisExpr);

         this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(local), this.sink.Heap.ReadHeap(thisExpr, Bpl.Expr.Ident(eventVar), resolvedMethod.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap, local.TypedIdent.Type)));

         inexpr[0] = Bpl.Expr.Ident(local);

       }

@@ -1175,7 +1218,7 @@ namespace BytecodeTranslator
             this.Traverse(target.Instance);

             x = this.TranslatedExpressions.Pop();

             if (pushTargetRValue) {

-

+              AssertOrAssumeNonNull(tok, x);

               var e2 = this.sink.Heap.ReadHeap(x, f, TranslationHelper.IsStruct(field.ContainingType) ? AccessType.Struct : AccessType.Heap, boogieTypeOfField);

               this.TranslatedExpressions.Push(e2);

 

@@ -1238,6 +1281,7 @@ namespace BytecodeTranslator
           this.Traverse(arrayIndexer.Indices);

           var indexExpr = this.TranslatedExpressions.Peek();

           if (pushTargetRValue) {

+            AssertOrAssumeNonNull(tok, arrayExpr);

             var e2 = this.sink.Heap.ReadHeap(arrayExpr, indexExpr, AccessType.Array, this.sink.CciTypeToBoogie(arrayIndexer.Type));

             this.TranslatedExpressions.Push(e2);

 

@@ -1258,6 +1302,7 @@ namespace BytecodeTranslator
           StmtTraverser.StmtBuilder.Add(sink.Heap.WriteHeap(Bpl.Token.NoToken, x, indices_prime, e, AccessType.Array, sink.CciTypeToBoogie(arrayIndexer.Type)));

 

           if (!treatAsStatement && !resultIsInitialTargetRValue) {

+            AssertOrAssumeNonNull(tok, arrayExpr);

             var e2 = this.sink.Heap.ReadHeap(arrayExpr, indexExpr, AccessType.Array, this.sink.CciTypeToBoogie(arrayIndexer.Type));

             this.TranslatedExpressions.Push(e2);

           } else {

diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index 22b64dca..cf758611 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -69,6 +69,13 @@ namespace BytecodeTranslator {
     [OptionDescription("Instrument branches with unique counter values", ShortForm = "ib")]

     public bool instrumentBranches = false;

 

+    [OptionDescription("Add free ensures that express heap monotonicity", ShortForm = "heapM")]

+    public bool monotonicHeap = false;

+

+    public enum Dereference { Assert, Assume, None, }

+    [OptionDescription("Assert/Assume on all object dereferences", ShortForm = "deref")]

+    public Dereference dereference = Dereference.Assume;

+

   }

 

   public class BCT {

diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index 8622c3a7..425a6b72 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -707,33 +707,35 @@ namespace BytecodeTranslator {
         }

         #endregion

 

-        #region Add free ensures for allocatedness of result (for methods that return references)

-        if (retVariable != null && retVariable.TypedIdent.Type == this.Heap.RefType) {

-          var ens = new Bpl.Ensures(true,

-            Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Or,

-              Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq,

-                Bpl.Expr.Ident(retVariable), Bpl.Expr.Ident(this.Heap.NullRef)),

-              Bpl.Expr.Select(Bpl.Expr.Ident(this.Heap.AllocVariable), Bpl.Expr.Ident(retVariable))

-              ));

-          boogiePostcondition.Add(ens);

-        }

-        #endregion

-        #region Add free ensures for preservation of allocatedness: AllocMapImplies(old($Alloc), $Alloc) == AllocMapConst(true)

-        var preserveAlloc = new Bpl.Ensures(true,

-          Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq,

-            new Bpl.NAryExpr(

-              Bpl.Token.NoToken,

-              new Bpl.FunctionCall(this.Heap.AllocImplies),

-                new Bpl.ExprSeq(

-                  new Bpl.OldExpr(Bpl.Token.NoToken, Bpl.Expr.Ident(this.Heap.AllocVariable)),

-                  Bpl.Expr.Ident(this.Heap.AllocVariable))),

-            new Bpl.NAryExpr(

-              Bpl.Token.NoToken,

-              new Bpl.FunctionCall(this.Heap.AllocConstBool),

-                new Bpl.ExprSeq(Bpl.Expr.True))

+        if (options.monotonicHeap) {

+          #region Add free ensures for allocatedness of result (for methods that return references)

+          if (retVariable != null && retVariable.TypedIdent.Type == this.Heap.RefType) {

+            var ens = new Bpl.Ensures(true,

+              Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Or,

+                Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq,

+                  Bpl.Expr.Ident(retVariable), Bpl.Expr.Ident(this.Heap.NullRef)),

+                Bpl.Expr.Select(Bpl.Expr.Ident(this.Heap.AllocVariable), Bpl.Expr.Ident(retVariable))

                 ));

-        boogiePostcondition.Add(preserveAlloc);

-        #endregion

+            boogiePostcondition.Add(ens);

+          }

+          #endregion

+          #region Add free ensures for preservation of allocatedness: AllocMapImplies(old($Alloc), $Alloc) == AllocMapConst(true)

+          var preserveAlloc = new Bpl.Ensures(true,

+            Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq,

+              new Bpl.NAryExpr(

+                Bpl.Token.NoToken,

+                new Bpl.FunctionCall(this.Heap.AllocImplies),

+                  new Bpl.ExprSeq(

+                    new Bpl.OldExpr(Bpl.Token.NoToken, Bpl.Expr.Ident(this.Heap.AllocVariable)),

+                    Bpl.Expr.Ident(this.Heap.AllocVariable))),

+              new Bpl.NAryExpr(

+                Bpl.Token.NoToken,

+                new Bpl.FunctionCall(this.Heap.AllocConstBool),

+                  new Bpl.ExprSeq(Bpl.Expr.True))

+                  ));

+          boogiePostcondition.Add(preserveAlloc);

+          #endregion

+        }

 

       }

       return procInfo;

diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
index 33f173ce..0fe003ae 100644
--- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
@@ -3,8 +3,6 @@
 

 type HeapType = [Ref][Field]Union;

 

-var $Alloc: [Ref]bool;

-

 procedure {:inline 1} Alloc() returns (x: Ref);

   modifies $Alloc;

 

@@ -18,45 +16,45 @@ implementation {:inline 1} Alloc() returns (x: Ref)
 

 

 

-function {:builtin "MapAdd"} mapadd([Delegate]int, [Delegate]int) : [Delegate]int;

+function {:builtin "MapAdd"} DelegateMapadd([Delegate]int, [Delegate]int) : [Delegate]int;

 

-function {:builtin "MapSub"} mapsub([Delegate]int, [Delegate]int) : [Delegate]int;

+function {:builtin "MapSub"} DelegateMapsub([Delegate]int, [Delegate]int) : [Delegate]int;

 

-function {:builtin "MapMul"} mapmul([Delegate]int, [Delegate]int) : [Delegate]int;

+function {:builtin "MapMul"} DelegateMapmul([Delegate]int, [Delegate]int) : [Delegate]int;

 

-function {:builtin "MapDiv"} mapdiv([Delegate]int, [Delegate]int) : [Delegate]int;

+function {:builtin "MapDiv"} DelegateMapdiv([Delegate]int, [Delegate]int) : [Delegate]int;

 

-function {:builtin "MapMod"} mapmod([Delegate]int, [Delegate]int) : [Delegate]int;

+function {:builtin "MapMod"} DelegateMapmod([Delegate]int, [Delegate]int) : [Delegate]int;

 

-function {:builtin "MapConst"} mapconstint(int) : [Delegate]int;

+function {:builtin "MapConst"} DelegateMapconstint(int) : [Delegate]int;

 

-function {:builtin "MapConst"} mapconstbool(bool) : [Delegate]bool;

+function {:builtin "MapConst"} DelegateMapconstbool(bool) : [Delegate]bool;

 

-function {:builtin "MapAnd"} mapand([Delegate]bool, [Delegate]bool) : [Delegate]bool;

+function {:builtin "MapAnd"} DelegateMapand([Delegate]bool, [Delegate]bool) : [Delegate]bool;

 

-function {:builtin "MapOr"} mapor([Delegate]bool, [Delegate]bool) : [Delegate]bool;

+function {:builtin "MapOr"} DelegateMapor([Delegate]bool, [Delegate]bool) : [Delegate]bool;

 

-function {:builtin "MapNot"} mapnot([Delegate]bool) : [Delegate]bool;

+function {:builtin "MapNot"} DelegateMapnot([Delegate]bool) : [Delegate]bool;

 

-function {:builtin "MapIte"} mapiteint([Delegate]bool, [Delegate]int, [Delegate]int) : [Delegate]int;

+function {:builtin "MapIte"} DelegateMapiteint([Delegate]bool, [Delegate]int, [Delegate]int) : [Delegate]int;

 

-function {:builtin "MapIte"} mapitebool([Delegate]bool, [Delegate]bool, [Delegate]bool) : [Delegate]bool;

+function {:builtin "MapIte"} DelegateMapitebool([Delegate]bool, [Delegate]bool, [Delegate]bool) : [Delegate]bool;

 

-function {:builtin "MapLe"} maple([Delegate]int, [Delegate]int) : [Delegate]bool;

+function {:builtin "MapLe"} DelegateMaple([Delegate]int, [Delegate]int) : [Delegate]bool;

 

-function {:builtin "MapLt"} maplt([Delegate]int, [Delegate]int) : [Delegate]bool;

+function {:builtin "MapLt"} DelegateMaplt([Delegate]int, [Delegate]int) : [Delegate]bool;

 

-function {:builtin "MapGe"} mapge([Delegate]int, [Delegate]int) : [Delegate]bool;

+function {:builtin "MapGe"} DelegateMapge([Delegate]int, [Delegate]int) : [Delegate]bool;

 

-function {:builtin "MapGt"} mapgt([Delegate]int, [Delegate]int) : [Delegate]bool;

+function {:builtin "MapGt"} DelegateMapgt([Delegate]int, [Delegate]int) : [Delegate]bool;

 

-function {:builtin "MapEq"} mapeq([Delegate]int, [Delegate]int) : [Delegate]bool;

+function {:builtin "MapEq"} DelegateMapeq([Delegate]int, [Delegate]int) : [Delegate]bool;

 

-function {:builtin "MapIff"} mapiff([Delegate]bool, [Delegate]bool) : [Delegate]bool;

+function {:builtin "MapIff"} DelegateMapiff([Delegate]bool, [Delegate]bool) : [Delegate]bool;

 

-function {:builtin "MapImp"} mapimp([Delegate]bool, [Delegate]bool) : [Delegate]bool;

+function {:builtin "MapImp"} DelegateMapimp([Delegate]bool, [Delegate]bool) : [Delegate]bool;

 

-axiom MultisetEmpty == mapconstint(0);

+axiom MultisetEmpty == DelegateMapconstint(0);

 

 function IsRef(u: Union) : bool;

 

@@ -289,12 +287,12 @@ function {:inline true} MultisetSingleton(x: Delegate) : DelegateMultiset
 

 function {:inline true} MultisetPlus(x: DelegateMultiset, y: DelegateMultiset) : DelegateMultiset

 {

-  mapadd(x, y)

+  DelegateMapadd(x, y)

 }

 

 function {:inline true} MultisetMinus(x: DelegateMultiset, y: DelegateMultiset) : DelegateMultiset

 {

-  mapiteint(mapgt(x, y), mapsub(x, y), mapconstint(0))

+  DelegateMapiteint(DelegateMapgt(x, y), DelegateMapsub(x, y), DelegateMapconstint(0))

 }

 

 type Field;

@@ -476,6 +474,12 @@ function $Subtype(Type, Type) : bool;
 

 function $DisjointSubtree(Type, Type) : bool;

 

+var $Alloc: [Ref]bool;

+

+function {:builtin "MapImp"} $allocImp([Ref]bool, [Ref]bool) : [Ref]bool;

+

+function {:builtin "MapConst"} $allocConstBool(bool) : [Ref]bool;

+

 function $RefToDelegate(Ref) : Delegate;

 

 function $RefToDelegateMultiset(Ref) : DelegateMultiset;

@@ -553,6 +557,8 @@ implementation {:inline 1} RegressionTestInput.StructContainingStruct.#copy_ctor
 

 

 procedure RegressionTestInput.StructContainingStruct.ReturnCopy$RegressionTestInput.StructContainingStruct($this: Ref, s$in: Ref) returns ($result: Ref);

+  free ensures $result == null || $Alloc[$result];

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -577,10 +583,12 @@ function {:constructor} T$RegressionTestInput.RealNumbers() : Type;
 axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.RealNumbers(), $T) } $Subtype(T$RegressionTestInput.RealNumbers(), $T) <==> T$RegressionTestInput.RealNumbers() == $T || $Subtype(T$System.Object(), $T));

 

 procedure RegressionTestInput.RealNumbers.WriteDouble$System.Double($this: Ref, d$in: Real);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

 procedure {:extern} System.Console.WriteLine$System.Double(value$in: Real);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -604,6 +612,7 @@ implementation RegressionTestInput.RealNumbers.WriteDouble$System.Double($this:
 

 

 procedure RegressionTestInput.RealNumbers.ObjectToDouble$System.Object($this: Ref, o$in: Ref);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -627,6 +636,7 @@ implementation RegressionTestInput.RealNumbers.ObjectToDouble$System.Object($thi
 

 

 procedure RegressionTestInput.RealNumbers.RealOperations($this: Ref);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -680,10 +690,12 @@ implementation RegressionTestInput.RealNumbers.RealOperations($this: Ref)
 

 

 procedure RegressionTestInput.RealNumbers.#ctor($this: Ref);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

 procedure {:extern} System.Object.#ctor($this: Ref);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -721,6 +733,7 @@ const unique F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x: Field;
 const unique F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y: Field;

 

 procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M($this: Ref);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -732,12 +745,14 @@ implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M($this:
     assume {:breadcrumb 5} true;

     assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 130} true;

     assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 130} true;

+    assume $this != null;

     $Heap := Write($Heap, $this, F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y, Int2Union(Union2Int(Read($Heap, $this, F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x))));

 }

 

 

 

 procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor($this: Ref);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -773,6 +788,8 @@ function {:constructor} T$RegressionTestInput.CreateStruct() : Type;
 axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.CreateStruct(), $T) } $Subtype(T$RegressionTestInput.CreateStruct(), $T) <==> T$RegressionTestInput.CreateStruct() == $T || $Subtype(T$System.Object(), $T));

 

 procedure RegressionTestInput.CreateStruct.Create($this: Ref) returns ($result: Ref);

+  free ensures $result == null || $Alloc[$result];

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -793,8 +810,10 @@ implementation RegressionTestInput.CreateStruct.Create($this: Ref) returns ($res
     assume $DynamicType($tmp0) == T$RegressionTestInput.S();

     s_Ref := $tmp0;

     assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 142} true;

+    assume s_Ref != null;

     assert Union2Int(Read($Heap, s_Ref, F$RegressionTestInput.S.x)) == 0;

     assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 143} true;

+    assume s_Ref != null;

     assert !Union2Bool(Read($Heap, s_Ref, F$RegressionTestInput.S.b));

     $result := s_Ref;

     return;

@@ -803,6 +822,8 @@ implementation RegressionTestInput.CreateStruct.Create($this: Ref) returns ($res
 

 

 procedure RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S($this: Ref, s$in: Ref) returns ($result: Ref);

+  free ensures $result == null || $Alloc[$result];

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -818,6 +839,7 @@ implementation RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTes
     assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 147} true;

     $Heap := Write($Heap, s, F$RegressionTestInput.S.x, Int2Union(3));

     assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 148} true;

+    assume s != null;

     assert Union2Int(Read($Heap, s, F$RegressionTestInput.S.x)) == 3;

     $result := s;

     return;

@@ -826,6 +848,7 @@ implementation RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTes
 

 

 procedure RegressionTestInput.CreateStruct.#ctor($this: Ref);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -863,6 +886,7 @@ var F$RegressionTestInput.ClassWithArrayTypes.s: Ref;
 const unique F$RegressionTestInput.ClassWithArrayTypes.a: Field;

 

 procedure RegressionTestInput.ClassWithArrayTypes.Main1();

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -880,19 +904,23 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main1()
     assume $ArrayLength($tmp0) == 1 * 5;

     s_Ref := $tmp0;

     assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 88} true;

+    assume s_Ref != null;

     assert Union2Int($ArrayContents[s_Ref][0]) == 2;

     call $tmp1 := Alloc();

     assume $ArrayLength($tmp1) == 1 * 4;

     t_Ref := $tmp1;

     assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 92} true;

+    assume t_Ref != null;

     assert Union2Int($ArrayContents[t_Ref][0]) == 1;

     assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 94} true;

+    assume s_Ref != null;

     assert Union2Int($ArrayContents[s_Ref][0]) == 2;

 }

 

 

 

 procedure RegressionTestInput.ClassWithArrayTypes.Main2();

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -914,27 +942,31 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main2()
     assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 101} true;

     $ArrayContents := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s][0 := Int2Union(2)]];

     assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 102} true;

+    assume F$RegressionTestInput.ClassWithArrayTypes.s != null;

     assert Union2Int($ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s][0]) == 2;

     call $tmp1 := Alloc();

     assume $ArrayLength($tmp1) == 1 * 4;

     t_Ref := $tmp1;

     assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 106} true;

+    assume t_Ref != null;

     assert Union2Int($ArrayContents[t_Ref][0]) == 1;

     assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 108} true;

+    assume F$RegressionTestInput.ClassWithArrayTypes.s != null;

     assert Union2Int($ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s][0]) == 2;

 }

 

 

 

 procedure RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32($this: Ref, x$in: int);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

 implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32($this: Ref, x$in: int)

 {

   var x: int;

-  var _loc0_Ref: Ref;

-  var _loc1_Ref: Ref;

+  var $tmp0: Ref;

+  var $tmp1: Ref;

   var $localExc: Ref;

   var $label: int;

 

@@ -942,51 +974,31 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32($this:
     assume {:breadcrumb 12} true;

     assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 114} true;

     assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 114} true;

+    assume $this != null;

     $ArrayContents := $ArrayContents[Union2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a)) := $ArrayContents[Union2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a))][x := Int2Union(42)]];

     assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 115} true;

     assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 115} true;

+    assume $this != null;

     $ArrayContents := $ArrayContents[Union2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a)) := $ArrayContents[Union2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a))][x + 1 := Int2Union(43)]];

     assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 116} true;

-    _loc0_Ref := Union2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a));

-    _loc1_Ref := Union2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a));

-    assert Union2Int($ArrayContents[_loc0_Ref][x + 1]) == Union2Int($ArrayContents[_loc1_Ref][x]) + 1;

+    assume $this != null;

+    $tmp0 := Union2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a));

+    assume $tmp0 != null;

+    assume $this != null;

+    $tmp1 := Union2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a));

+    assume $tmp1 != null;

+    assert Union2Int($ArrayContents[$tmp0][x + 1]) == Union2Int($ArrayContents[$tmp1][x]) + 1;

 }

 

 

 

 procedure RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array($this: Ref, xs$in: Ref);

-

-

-

-implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array($this: Ref, xs$in: Ref)

-{

-  var xs: Ref;

-  var $localExc: Ref;

-  var $label: int;

-

-    xs := xs$in;

-    assume {:breadcrumb 13} true;

-    if (!(xs != null))

-    {

-    }

-    else

-    {

-    }

-

-    if ((if !(xs != null) then true else !($ArrayLength(xs) > 0)) == 0)

-    {

-        assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 121} true;

-        assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 121} true;

-        $ArrayContents := $ArrayContents[Union2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a)) := $ArrayContents[Union2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a))][0 := Int2Union(Union2Int($ArrayContents[xs][0]))]];

-    }

-    else

-    {

-    }

-}

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

 procedure RegressionTestInput.ClassWithArrayTypes.#ctor($this: Ref);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1024,6 +1036,7 @@ axiom (forall T: Type, $T: Type :: { $Subtype(T$RegressionTestInput.TestForClass
 const unique F$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.x: Field;

 

 procedure RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.#ctor($this: Ref);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1058,6 +1071,7 @@ function {:constructor} T$RegressionTestInput.BitwiseOperations() : Type;
 axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.BitwiseOperations(), $T) } $Subtype(T$RegressionTestInput.BitwiseOperations(), $T) <==> T$RegressionTestInput.BitwiseOperations() == $T || $Subtype(T$System.Object(), $T));

 

 procedure RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int) returns ($result: int);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1078,6 +1092,7 @@ implementation RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$Sys
 

 

 procedure RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int) returns ($result: int);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1098,6 +1113,7 @@ implementation RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$Syst
 

 

 procedure RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int) returns ($result: int);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1118,6 +1134,7 @@ implementation RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$Sy
 

 

 procedure RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int32($this: Ref, x$in: int) returns ($result: int);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1136,6 +1153,7 @@ implementation RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int3
 

 

 procedure RegressionTestInput.BitwiseOperations.#ctor($this: Ref);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1177,10 +1195,12 @@ axiom (forall $T: Type :: { $Subtype(T$System.Attribute(), $T) } $Subtype(T$Syst
 axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.AsyncAttribute(), $T) } $Subtype(T$RegressionTestInput.AsyncAttribute(), $T) <==> T$RegressionTestInput.AsyncAttribute() == $T || $Subtype(T$System.Attribute(), $T));

 

 procedure RegressionTestInput.AsyncAttribute.#ctor($this: Ref);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

 procedure {:extern} System.Attribute.#ctor($this: Ref);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1214,6 +1234,7 @@ function {:constructor} T$RegressionTestInput.RefParameters() : Type;
 axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.RefParameters(), $T) } $Subtype(T$RegressionTestInput.RefParameters(), $T) <==> T$RegressionTestInput.RefParameters() == $T || $Subtype(T$System.Object(), $T));

 

 procedure RegressionTestInput.RefParameters.M$System.Int32$(x$in: int) returns (x$out: int);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1231,6 +1252,7 @@ implementation RegressionTestInput.RefParameters.M$System.Int32$(x$in: int) retu
 

 

 procedure RegressionTestInput.RefParameters.#ctor($this: Ref);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1264,6 +1286,7 @@ function {:constructor} T$RegressionTestInput.NestedGeneric() : Type;
 axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.NestedGeneric(), $T) } $Subtype(T$RegressionTestInput.NestedGeneric(), $T) <==> T$RegressionTestInput.NestedGeneric() == $T || $Subtype(T$System.Object(), $T));

 

 procedure RegressionTestInput.NestedGeneric.#ctor($this: Ref);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1287,6 +1310,7 @@ function {:constructor} T$RegressionTestInput.NestedGeneric.C() : Type;
 axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.NestedGeneric.C(), $T) } $Subtype(T$RegressionTestInput.NestedGeneric.C(), $T) <==> T$RegressionTestInput.NestedGeneric.C() == $T || $Subtype(T$System.Object(), $T));

 

 procedure RegressionTestInput.NestedGeneric.C.#ctor($this: Ref);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1310,10 +1334,12 @@ function {:constructor} T$RegressionTestInput.NestedGeneric.C.G`1(T: Type) : Typ
 axiom (forall T: Type, $T: Type :: { $Subtype(T$RegressionTestInput.NestedGeneric.C.G`1(T), $T) } $Subtype(T$RegressionTestInput.NestedGeneric.C.G`1(T), $T) <==> T$RegressionTestInput.NestedGeneric.C.G`1(T) == $T || $Subtype(T$System.Object(), $T));

 

 procedure RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this: Ref, x$in: int);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

 procedure {:extern} System.Activator.CreateInstance``1(T: Type) returns ($result: Union);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1417,6 +1443,7 @@ axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.TestForClassesDifferi
 const unique F$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.x: Field;

 

 procedure RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.#ctor($this: Ref);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1453,6 +1480,7 @@ axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.Class0(), $T) } $Subt
 var F$RegressionTestInput.Class0.StaticInt: int;

 

 procedure RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) returns ($result: int);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1471,6 +1499,7 @@ implementation RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) r
 

 

 procedure RegressionTestInput.Class0.M$System.Int32($this: Ref, x$in: int);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1507,6 +1536,7 @@ implementation RegressionTestInput.Class0.M$System.Int32($this: Ref, x$in: int)
 

 

 procedure RegressionTestInput.Class0.M$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1525,6 +1555,7 @@ implementation RegressionTestInput.Class0.M$System.Int32$System.Int32($this: Ref
 

 

 procedure RegressionTestInput.Class0.M$System.Boolean($this: Ref, b$in: bool);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1541,6 +1572,7 @@ implementation RegressionTestInput.Class0.M$System.Boolean($this: Ref, b$in: boo
 

 

 procedure RegressionTestInput.Class0.M$RegressionTestInput.Class0($this: Ref, c$in: Ref);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1557,6 +1589,7 @@ implementation RegressionTestInput.Class0.M$RegressionTestInput.Class0($this: Re
 

 

 procedure RegressionTestInput.Class0.NonVoid($this: Ref) returns ($result: int);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1580,6 +1613,7 @@ implementation RegressionTestInput.Class0.NonVoid($this: Ref) returns ($result:
 

 

 procedure RegressionTestInput.Class0.OutParam$System.Int32$($this: Ref, x$in: int) returns (x$out: int, $result: int);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1601,6 +1635,7 @@ implementation RegressionTestInput.Class0.OutParam$System.Int32$($this: Ref, x$i
 

 

 procedure RegressionTestInput.Class0.RefParam$System.Int32$($this: Ref, x$in: int) returns (x$out: int, $result: int);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1625,6 +1660,7 @@ implementation RegressionTestInput.Class0.RefParam$System.Int32$($this: Ref, x$i
 

 

 procedure RegressionTestInput.Class0.AssignToInParam$System.Int32($this: Ref, x$in: int) returns ($result: int);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1649,6 +1685,7 @@ implementation RegressionTestInput.Class0.AssignToInParam$System.Int32($this: Re
 

 

 procedure {:RegressionTestInput.Async} RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32($this: Ref, x$in: int) returns ($result: int);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1667,6 +1704,7 @@ implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMetho
 

 

 procedure RegressionTestInput.Class0.CallAsyncMethod$System.Int32($this: Ref, y$in: int) returns ($result: int);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1692,6 +1730,7 @@ implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int32($this: Re
 

 

 procedure RegressionTestInput.Class0.#ctor($this: Ref);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1730,6 +1769,7 @@ var F$RegressionTestInput.ClassWithBoolTypes.staticB: bool;
 const unique F$RegressionTestInput.ClassWithBoolTypes.b: Field;

 

 procedure RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(x$in: int, y$in: int) returns ($result: bool);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1750,6 +1790,7 @@ implementation RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3
 

 

 procedure RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean($this: Ref, z$in: bool);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1788,6 +1829,7 @@ implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean($this
 

 

 procedure RegressionTestInput.ClassWithBoolTypes.Main();

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
index 3069f557..5dfc582e 100644
--- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
@@ -1,8 +1,6 @@
 // Copyright (c) 2010, Microsoft Corp.

 // Bytecode Translator prelude

 

-var $Alloc: [Ref]bool;

-

 procedure {:inline 1} Alloc() returns (x: Ref);

   modifies $Alloc;

 

@@ -16,45 +14,45 @@ implementation {:inline 1} Alloc() returns (x: Ref)
 

 

 

-function {:builtin "MapAdd"} mapadd([Delegate]int, [Delegate]int) : [Delegate]int;

+function {:builtin "MapAdd"} DelegateMapadd([Delegate]int, [Delegate]int) : [Delegate]int;

 

-function {:builtin "MapSub"} mapsub([Delegate]int, [Delegate]int) : [Delegate]int;

+function {:builtin "MapSub"} DelegateMapsub([Delegate]int, [Delegate]int) : [Delegate]int;

 

-function {:builtin "MapMul"} mapmul([Delegate]int, [Delegate]int) : [Delegate]int;

+function {:builtin "MapMul"} DelegateMapmul([Delegate]int, [Delegate]int) : [Delegate]int;

 

-function {:builtin "MapDiv"} mapdiv([Delegate]int, [Delegate]int) : [Delegate]int;

+function {:builtin "MapDiv"} DelegateMapdiv([Delegate]int, [Delegate]int) : [Delegate]int;

 

-function {:builtin "MapMod"} mapmod([Delegate]int, [Delegate]int) : [Delegate]int;

+function {:builtin "MapMod"} DelegateMapmod([Delegate]int, [Delegate]int) : [Delegate]int;

 

-function {:builtin "MapConst"} mapconstint(int) : [Delegate]int;

+function {:builtin "MapConst"} DelegateMapconstint(int) : [Delegate]int;

 

-function {:builtin "MapConst"} mapconstbool(bool) : [Delegate]bool;

+function {:builtin "MapConst"} DelegateMapconstbool(bool) : [Delegate]bool;

 

-function {:builtin "MapAnd"} mapand([Delegate]bool, [Delegate]bool) : [Delegate]bool;

+function {:builtin "MapAnd"} DelegateMapand([Delegate]bool, [Delegate]bool) : [Delegate]bool;

 

-function {:builtin "MapOr"} mapor([Delegate]bool, [Delegate]bool) : [Delegate]bool;

+function {:builtin "MapOr"} DelegateMapor([Delegate]bool, [Delegate]bool) : [Delegate]bool;

 

-function {:builtin "MapNot"} mapnot([Delegate]bool) : [Delegate]bool;

+function {:builtin "MapNot"} DelegateMapnot([Delegate]bool) : [Delegate]bool;

 

-function {:builtin "MapIte"} mapiteint([Delegate]bool, [Delegate]int, [Delegate]int) : [Delegate]int;

+function {:builtin "MapIte"} DelegateMapiteint([Delegate]bool, [Delegate]int, [Delegate]int) : [Delegate]int;

 

-function {:builtin "MapIte"} mapitebool([Delegate]bool, [Delegate]bool, [Delegate]bool) : [Delegate]bool;

+function {:builtin "MapIte"} DelegateMapitebool([Delegate]bool, [Delegate]bool, [Delegate]bool) : [Delegate]bool;

 

-function {:builtin "MapLe"} maple([Delegate]int, [Delegate]int) : [Delegate]bool;

+function {:builtin "MapLe"} DelegateMaple([Delegate]int, [Delegate]int) : [Delegate]bool;

 

-function {:builtin "MapLt"} maplt([Delegate]int, [Delegate]int) : [Delegate]bool;

+function {:builtin "MapLt"} DelegateMaplt([Delegate]int, [Delegate]int) : [Delegate]bool;

 

-function {:builtin "MapGe"} mapge([Delegate]int, [Delegate]int) : [Delegate]bool;

+function {:builtin "MapGe"} DelegateMapge([Delegate]int, [Delegate]int) : [Delegate]bool;

 

-function {:builtin "MapGt"} mapgt([Delegate]int, [Delegate]int) : [Delegate]bool;

+function {:builtin "MapGt"} DelegateMapgt([Delegate]int, [Delegate]int) : [Delegate]bool;

 

-function {:builtin "MapEq"} mapeq([Delegate]int, [Delegate]int) : [Delegate]bool;

+function {:builtin "MapEq"} DelegateMapeq([Delegate]int, [Delegate]int) : [Delegate]bool;

 

-function {:builtin "MapIff"} mapiff([Delegate]bool, [Delegate]bool) : [Delegate]bool;

+function {:builtin "MapIff"} DelegateMapiff([Delegate]bool, [Delegate]bool) : [Delegate]bool;

 

-function {:builtin "MapImp"} mapimp([Delegate]bool, [Delegate]bool) : [Delegate]bool;

+function {:builtin "MapImp"} DelegateMapimp([Delegate]bool, [Delegate]bool) : [Delegate]bool;

 

-axiom MultisetEmpty == mapconstint(0);

+axiom MultisetEmpty == DelegateMapconstint(0);

 

 function IsRef(u: Union) : bool;

 

@@ -275,12 +273,12 @@ function {:inline true} MultisetSingleton(x: Delegate) : DelegateMultiset
 

 function {:inline true} MultisetPlus(x: DelegateMultiset, y: DelegateMultiset) : DelegateMultiset

 {

-  mapadd(x, y)

+  DelegateMapadd(x, y)

 }

 

 function {:inline true} MultisetMinus(x: DelegateMultiset, y: DelegateMultiset) : DelegateMultiset

 {

-  mapiteint(mapgt(x, y), mapsub(x, y), mapconstint(0))

+  DelegateMapiteint(DelegateMapgt(x, y), DelegateMapsub(x, y), DelegateMapconstint(0))

 }

 

 type Field;

@@ -462,6 +460,12 @@ function $Subtype(Type, Type) : bool;
 

 function $DisjointSubtree(Type, Type) : bool;

 

+var $Alloc: [Ref]bool;

+

+function {:builtin "MapImp"} $allocImp([Ref]bool, [Ref]bool) : [Ref]bool;

+

+function {:builtin "MapConst"} $allocConstBool(bool) : [Ref]bool;

+

 function $RefToDelegate(Ref) : Delegate;

 

 function $RefToDelegateMultiset(Ref) : DelegateMultiset;

@@ -539,6 +543,8 @@ implementation {:inline 1} RegressionTestInput.StructContainingStruct.#copy_ctor
 

 

 procedure RegressionTestInput.StructContainingStruct.ReturnCopy$RegressionTestInput.StructContainingStruct($this: Ref, s$in: Ref) returns ($result: Ref);

+  free ensures $result == null || $Alloc[$result];

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -550,7 +556,7 @@ implementation RegressionTestInput.StructContainingStruct.ReturnCopy$RegressionT
   var $label: int;

 

     s := s$in;

-    assume {:breadcrumb 43} true;

+    assume {:breadcrumb 0} true;

     call t_Ref := RegressionTestInput.StructContainingStruct.#copy_ctor(s);

     $result := t_Ref;

     return;

@@ -563,10 +569,12 @@ function {:constructor} T$RegressionTestInput.RealNumbers() : Type;
 axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.RealNumbers(), $T) } $Subtype(T$RegressionTestInput.RealNumbers(), $T) <==> T$RegressionTestInput.RealNumbers() == $T || $Subtype(T$System.Object(), $T));

 

 procedure RegressionTestInput.RealNumbers.WriteDouble$System.Double($this: Ref, d$in: Real);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

 procedure {:extern} System.Console.WriteLine$System.Double(value$in: Real);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -577,7 +585,7 @@ implementation RegressionTestInput.RealNumbers.WriteDouble$System.Double($this:
   var $label: int;

 

     d := d$in;

-    assume {:breadcrumb 44} true;

+    assume {:breadcrumb 1} true;

     assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 162} true;

     assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 162} true;

     call System.Console.WriteLine$System.Double(d);

@@ -590,6 +598,7 @@ implementation RegressionTestInput.RealNumbers.WriteDouble$System.Double($this:
 

 

 procedure RegressionTestInput.RealNumbers.ObjectToDouble$System.Object($this: Ref, o$in: Ref);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -600,7 +609,7 @@ implementation RegressionTestInput.RealNumbers.ObjectToDouble$System.Object($thi
   var $label: int;

 

     o := o$in;

-    assume {:breadcrumb 45} true;

+    assume {:breadcrumb 2} true;

     assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 165} true;

     assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 165} true;

     call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, $Unbox2Real(o));

@@ -613,6 +622,7 @@ implementation RegressionTestInput.RealNumbers.ObjectToDouble$System.Object($thi
 

 

 procedure RegressionTestInput.RealNumbers.RealOperations($this: Ref);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -627,7 +637,7 @@ implementation RegressionTestInput.RealNumbers.RealOperations($this: Ref)
   var $localExc: Ref;

   var $label: int;

 

-    assume {:breadcrumb 46} true;

+    assume {:breadcrumb 3} true;

     d_Real := $real_literal_3_0;

     d2_Real := $real_literal_4_0;

     assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 170} true;

@@ -666,10 +676,12 @@ implementation RegressionTestInput.RealNumbers.RealOperations($this: Ref)
 

 

 procedure RegressionTestInput.RealNumbers.#ctor($this: Ref);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

 procedure {:extern} System.Object.#ctor($this: Ref);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -678,7 +690,7 @@ implementation RegressionTestInput.RealNumbers.#ctor($this: Ref)
   var $localExc: Ref;

   var $label: int;

 

-    assume {:breadcrumb 47} true;

+    assume {:breadcrumb 4} true;

     call System.Object.#ctor($this);

     if ($Exception != null)

     {

@@ -707,6 +719,7 @@ var F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x: [Ref]int;
 var F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y: [Ref]int;

 

 procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M($this: Ref);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -715,15 +728,17 @@ implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M($this:
   var $localExc: Ref;

   var $label: int;

 

-    assume {:breadcrumb 48} true;

+    assume {:breadcrumb 5} true;

     assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 130} true;

     assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 130} true;

+    assume $this != null;

     F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y[$this] := F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x[$this];

 }

 

 

 

 procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor($this: Ref);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -734,7 +749,7 @@ implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor($th
 

     F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x[$this] := 0;

     F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y[$this] := 0;

-    assume {:breadcrumb 49} true;

+    assume {:breadcrumb 6} true;

     call System.Object.#ctor($this);

     if ($Exception != null)

     {

@@ -759,6 +774,8 @@ function {:constructor} T$RegressionTestInput.CreateStruct() : Type;
 axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.CreateStruct(), $T) } $Subtype(T$RegressionTestInput.CreateStruct(), $T) <==> T$RegressionTestInput.CreateStruct() == $T || $Subtype(T$System.Object(), $T));

 

 procedure RegressionTestInput.CreateStruct.Create($this: Ref) returns ($result: Ref);

+  free ensures $result == null || $Alloc[$result];

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -773,14 +790,16 @@ implementation RegressionTestInput.CreateStruct.Create($this: Ref) returns ($res
   var $localExc: Ref;

   var $label: int;

 

-    assume {:breadcrumb 50} true;

+    assume {:breadcrumb 7} true;

     call $tmp0 := Alloc();

     call RegressionTestInput.S.#default_ctor($tmp0);

     assume $DynamicType($tmp0) == T$RegressionTestInput.S();

     s_Ref := $tmp0;

     assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 142} true;

+    assume s_Ref != null;

     assert F$RegressionTestInput.S.x[s_Ref] == 0;

     assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 143} true;

+    assume s_Ref != null;

     assert !F$RegressionTestInput.S.b[s_Ref];

     $result := s_Ref;

     return;

@@ -789,6 +808,8 @@ implementation RegressionTestInput.CreateStruct.Create($this: Ref) returns ($res
 

 

 procedure RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S($this: Ref, s$in: Ref) returns ($result: Ref);

+  free ensures $result == null || $Alloc[$result];

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -799,11 +820,12 @@ implementation RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTes
   var $label: int;

 

     s := s$in;

-    assume {:breadcrumb 51} true;

+    assume {:breadcrumb 8} true;

     assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 147} true;

     assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 147} true;

     F$RegressionTestInput.S.x[s] := 3;

     assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 148} true;

+    assume s != null;

     assert F$RegressionTestInput.S.x[s] == 3;

     $result := s;

     return;

@@ -812,6 +834,7 @@ implementation RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTes
 

 

 procedure RegressionTestInput.CreateStruct.#ctor($this: Ref);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -820,7 +843,7 @@ implementation RegressionTestInput.CreateStruct.#ctor($this: Ref)
   var $localExc: Ref;

   var $label: int;

 

-    assume {:breadcrumb 52} true;

+    assume {:breadcrumb 9} true;

     call System.Object.#ctor($this);

     if ($Exception != null)

     {

@@ -849,6 +872,7 @@ var F$RegressionTestInput.ClassWithArrayTypes.s: Ref;
 var F$RegressionTestInput.ClassWithArrayTypes.a: [Ref]Ref;

 

 procedure RegressionTestInput.ClassWithArrayTypes.Main1();

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -861,24 +885,28 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main1()
   var $localExc: Ref;

   var $label: int;

 

-    assume {:breadcrumb 53} true;

+    assume {:breadcrumb 10} true;

     call $tmp0 := Alloc();

     assume $ArrayLength($tmp0) == 1 * 5;

     s_Ref := $tmp0;

     assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 88} true;

+    assume s_Ref != null;

     assert Union2Int($ArrayContents[s_Ref][0]) == 2;

     call $tmp1 := Alloc();

     assume $ArrayLength($tmp1) == 1 * 4;

     t_Ref := $tmp1;

     assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 92} true;

+    assume t_Ref != null;

     assert Union2Int($ArrayContents[t_Ref][0]) == 1;

     assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 94} true;

+    assume s_Ref != null;

     assert Union2Int($ArrayContents[s_Ref][0]) == 2;

 }

 

 

 

 procedure RegressionTestInput.ClassWithArrayTypes.Main2();

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -890,7 +918,7 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main2()
   var $localExc: Ref;

   var $label: int;

 

-    assume {:breadcrumb 54} true;

+    assume {:breadcrumb 11} true;

     assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 100} true;

     assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 100} true;

     call $tmp0 := Alloc();

@@ -900,79 +928,63 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main2()
     assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 101} true;

     $ArrayContents := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s][0 := Int2Union(2)]];

     assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 102} true;

+    assume F$RegressionTestInput.ClassWithArrayTypes.s != null;

     assert Union2Int($ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s][0]) == 2;

     call $tmp1 := Alloc();

     assume $ArrayLength($tmp1) == 1 * 4;

     t_Ref := $tmp1;

     assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 106} true;

+    assume t_Ref != null;

     assert Union2Int($ArrayContents[t_Ref][0]) == 1;

     assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 108} true;

+    assume F$RegressionTestInput.ClassWithArrayTypes.s != null;

     assert Union2Int($ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s][0]) == 2;

 }

 

 

 

 procedure RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32($this: Ref, x$in: int);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

 implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32($this: Ref, x$in: int)

 {

   var x: int;

-  var _loc0_Ref: Ref;

-  var _loc1_Ref: Ref;

+  var $tmp0: Ref;

+  var $tmp1: Ref;

   var $localExc: Ref;

   var $label: int;

 

     x := x$in;

-    assume {:breadcrumb 55} true;

+    assume {:breadcrumb 12} true;

     assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 114} true;

     assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 114} true;

+    assume $this != null;

     $ArrayContents := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.a[$this] := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.a[$this]][x := Int2Union(42)]];

     assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 115} true;

     assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 115} true;

+    assume $this != null;

     $ArrayContents := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.a[$this] := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.a[$this]][x + 1 := Int2Union(43)]];

     assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 116} true;

-    _loc0_Ref := F$RegressionTestInput.ClassWithArrayTypes.a[$this];

-    _loc1_Ref := F$RegressionTestInput.ClassWithArrayTypes.a[$this];

-    assert Union2Int($ArrayContents[_loc0_Ref][x + 1]) == Union2Int($ArrayContents[_loc1_Ref][x]) + 1;

+    assume $this != null;

+    $tmp0 := F$RegressionTestInput.ClassWithArrayTypes.a[$this];

+    assume $tmp0 != null;

+    assume $this != null;

+    $tmp1 := F$RegressionTestInput.ClassWithArrayTypes.a[$this];

+    assume $tmp1 != null;

+    assert Union2Int($ArrayContents[$tmp0][x + 1]) == Union2Int($ArrayContents[$tmp1][x]) + 1;

 }

 

 

 

 procedure RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array($this: Ref, xs$in: Ref);

-

-

-

-implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array($this: Ref, xs$in: Ref)

-{

-  var xs: Ref;

-  var $localExc: Ref;

-  var $label: int;

-

-    xs := xs$in;

-    assume {:breadcrumb 56} true;

-    if (!(xs != null))

-    {

-    }

-    else

-    {

-    }

-

-    if ((if !(xs != null) then true else !($ArrayLength(xs) > 0)) == 0)

-    {

-        assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 121} true;

-        assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 121} true;

-        $ArrayContents := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.a[$this] := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.a[$this]][0 := Int2Union(Union2Int($ArrayContents[xs][0]))]];

-    }

-    else

-    {

-    }

-}

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

 procedure RegressionTestInput.ClassWithArrayTypes.#ctor($this: Ref);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -982,7 +994,7 @@ implementation RegressionTestInput.ClassWithArrayTypes.#ctor($this: Ref)
   var $label: int;

 

     F$RegressionTestInput.ClassWithArrayTypes.a[$this] := null;

-    assume {:breadcrumb 57} true;

+    assume {:breadcrumb 14} true;

     call System.Object.#ctor($this);

     if ($Exception != null)

     {

@@ -1010,6 +1022,7 @@ axiom (forall T: Type, $T: Type :: { $Subtype(T$RegressionTestInput.TestForClass
 var F$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.x: [Ref]int;

 

 procedure RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.#ctor($this: Ref);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1019,7 +1032,7 @@ implementation RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.#
   var $label: int;

 

     F$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.x[$this] := 0;

-    assume {:breadcrumb 58} true;

+    assume {:breadcrumb 15} true;

     call System.Object.#ctor($this);

     if ($Exception != null)

     {

@@ -1044,6 +1057,7 @@ function {:constructor} T$RegressionTestInput.BitwiseOperations() : Type;
 axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.BitwiseOperations(), $T) } $Subtype(T$RegressionTestInput.BitwiseOperations(), $T) <==> T$RegressionTestInput.BitwiseOperations() == $T || $Subtype(T$System.Object(), $T));

 

 procedure RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int) returns ($result: int);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1056,7 +1070,7 @@ implementation RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$Sys
 

     x := x$in;

     y := y$in;

-    assume {:breadcrumb 59} true;

+    assume {:breadcrumb 16} true;

     $result := BitwiseAnd(x, y);

     return;

 }

@@ -1064,6 +1078,7 @@ implementation RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$Sys
 

 

 procedure RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int) returns ($result: int);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1076,7 +1091,7 @@ implementation RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$Syst
 

     x := x$in;

     y := y$in;

-    assume {:breadcrumb 60} true;

+    assume {:breadcrumb 17} true;

     $result := BitwiseOr(x, y);

     return;

 }

@@ -1084,6 +1099,7 @@ implementation RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$Syst
 

 

 procedure RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int) returns ($result: int);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1096,7 +1112,7 @@ implementation RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$Sy
 

     x := x$in;

     y := y$in;

-    assume {:breadcrumb 61} true;

+    assume {:breadcrumb 18} true;

     $result := BitwiseExclusiveOr(x, y);

     return;

 }

@@ -1104,6 +1120,7 @@ implementation RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$Sy
 

 

 procedure RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int32($this: Ref, x$in: int) returns ($result: int);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1114,7 +1131,7 @@ implementation RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int3
   var $label: int;

 

     x := x$in;

-    assume {:breadcrumb 62} true;

+    assume {:breadcrumb 19} true;

     $result := BitwiseNegation(x);

     return;

 }

@@ -1122,6 +1139,7 @@ implementation RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int3
 

 

 procedure RegressionTestInput.BitwiseOperations.#ctor($this: Ref);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1130,7 +1148,7 @@ implementation RegressionTestInput.BitwiseOperations.#ctor($this: Ref)
   var $localExc: Ref;

   var $label: int;

 

-    assume {:breadcrumb 63} true;

+    assume {:breadcrumb 20} true;

     call System.Object.#ctor($this);

     if ($Exception != null)

     {

@@ -1163,10 +1181,12 @@ axiom (forall $T: Type :: { $Subtype(T$System.Attribute(), $T) } $Subtype(T$Syst
 axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.AsyncAttribute(), $T) } $Subtype(T$RegressionTestInput.AsyncAttribute(), $T) <==> T$RegressionTestInput.AsyncAttribute() == $T || $Subtype(T$System.Attribute(), $T));

 

 procedure RegressionTestInput.AsyncAttribute.#ctor($this: Ref);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

 procedure {:extern} System.Attribute.#ctor($this: Ref);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1175,7 +1195,7 @@ implementation RegressionTestInput.AsyncAttribute.#ctor($this: Ref)
   var $localExc: Ref;

   var $label: int;

 

-    assume {:breadcrumb 64} true;

+    assume {:breadcrumb 21} true;

     call System.Attribute.#ctor($this);

     if ($Exception != null)

     {

@@ -1200,6 +1220,7 @@ function {:constructor} T$RegressionTestInput.RefParameters() : Type;
 axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.RefParameters(), $T) } $Subtype(T$RegressionTestInput.RefParameters(), $T) <==> T$RegressionTestInput.RefParameters() == $T || $Subtype(T$System.Object(), $T));

 

 procedure RegressionTestInput.RefParameters.M$System.Int32$(x$in: int) returns (x$out: int);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1209,7 +1230,7 @@ implementation RegressionTestInput.RefParameters.M$System.Int32$(x$in: int) retu
   var $label: int;

 

     x$out := x$in;

-    assume {:breadcrumb 65} true;

+    assume {:breadcrumb 22} true;

     assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 156} true;

     x$out := x$out + 1;

 }

@@ -1217,6 +1238,7 @@ implementation RegressionTestInput.RefParameters.M$System.Int32$(x$in: int) retu
 

 

 procedure RegressionTestInput.RefParameters.#ctor($this: Ref);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1225,7 +1247,7 @@ implementation RegressionTestInput.RefParameters.#ctor($this: Ref)
   var $localExc: Ref;

   var $label: int;

 

-    assume {:breadcrumb 66} true;

+    assume {:breadcrumb 23} true;

     call System.Object.#ctor($this);

     if ($Exception != null)

     {

@@ -1250,6 +1272,7 @@ function {:constructor} T$RegressionTestInput.NestedGeneric() : Type;
 axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.NestedGeneric(), $T) } $Subtype(T$RegressionTestInput.NestedGeneric(), $T) <==> T$RegressionTestInput.NestedGeneric() == $T || $Subtype(T$System.Object(), $T));

 

 procedure RegressionTestInput.NestedGeneric.#ctor($this: Ref);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1258,7 +1281,7 @@ implementation RegressionTestInput.NestedGeneric.#ctor($this: Ref)
   var $localExc: Ref;

   var $label: int;

 

-    assume {:breadcrumb 67} true;

+    assume {:breadcrumb 24} true;

     call System.Object.#ctor($this);

     if ($Exception != null)

     {

@@ -1273,6 +1296,7 @@ function {:constructor} T$RegressionTestInput.NestedGeneric.C() : Type;
 axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.NestedGeneric.C(), $T) } $Subtype(T$RegressionTestInput.NestedGeneric.C(), $T) <==> T$RegressionTestInput.NestedGeneric.C() == $T || $Subtype(T$System.Object(), $T));

 

 procedure RegressionTestInput.NestedGeneric.C.#ctor($this: Ref);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1281,7 +1305,7 @@ implementation RegressionTestInput.NestedGeneric.C.#ctor($this: Ref)
   var $localExc: Ref;

   var $label: int;

 

-    assume {:breadcrumb 68} true;

+    assume {:breadcrumb 25} true;

     call System.Object.#ctor($this);

     if ($Exception != null)

     {

@@ -1296,10 +1320,12 @@ function {:constructor} T$RegressionTestInput.NestedGeneric.C.G`1(T: Type) : Typ
 axiom (forall T: Type, $T: Type :: { $Subtype(T$RegressionTestInput.NestedGeneric.C.G`1(T), $T) } $Subtype(T$RegressionTestInput.NestedGeneric.C.G`1(T), $T) <==> T$RegressionTestInput.NestedGeneric.C.G`1(T) == $T || $Subtype(T$System.Object(), $T));

 

 procedure RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this: Ref, x$in: int);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

 procedure {:extern} System.Activator.CreateInstance``1(T: Type) returns ($result: Union);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1315,7 +1341,7 @@ implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this:
   var $label: int;

 

     x := x$in;

-    assume {:breadcrumb 69} true;

+    assume {:breadcrumb 26} true;

     assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 187} true;

     assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 187} true;

     call System.Object.#ctor($this);

@@ -1403,6 +1429,7 @@ axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.TestForClassesDifferi
 var F$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.x: [Ref]int;

 

 procedure RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.#ctor($this: Ref);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1412,7 +1439,7 @@ implementation RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.#ct
   var $label: int;

 

     F$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.x[$this] := 0;

-    assume {:breadcrumb 70} true;

+    assume {:breadcrumb 27} true;

     call System.Object.#ctor($this);

     if ($Exception != null)

     {

@@ -1439,6 +1466,7 @@ axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.Class0(), $T) } $Subt
 var F$RegressionTestInput.Class0.StaticInt: int;

 

 procedure RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) returns ($result: int);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1449,7 +1477,7 @@ implementation RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) r
   var $label: int;

 

     x := x$in;

-    assume {:breadcrumb 71} true;

+    assume {:breadcrumb 28} true;

     $result := x + 1;

     return;

 }

@@ -1457,6 +1485,7 @@ implementation RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) r
 

 

 procedure RegressionTestInput.Class0.M$System.Int32($this: Ref, x$in: int);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1468,7 +1497,7 @@ implementation RegressionTestInput.Class0.M$System.Int32($this: Ref, x$in: int)
   var $label: int;

 

     x := x$in;

-    assume {:breadcrumb 72} true;

+    assume {:breadcrumb 29} true;

     assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 21} true;

     assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 21} true;

     x := 3;

@@ -1493,6 +1522,7 @@ implementation RegressionTestInput.Class0.M$System.Int32($this: Ref, x$in: int)
 

 

 procedure RegressionTestInput.Class0.M$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1505,12 +1535,13 @@ implementation RegressionTestInput.Class0.M$System.Int32$System.Int32($this: Ref
 

     x := x$in;

     y := y$in;

-    assume {:breadcrumb 73} true;

+    assume {:breadcrumb 30} true;

 }

 

 

 

 procedure RegressionTestInput.Class0.M$System.Boolean($this: Ref, b$in: bool);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1521,12 +1552,13 @@ implementation RegressionTestInput.Class0.M$System.Boolean($this: Ref, b$in: boo
   var $label: int;

 

     b := b$in;

-    assume {:breadcrumb 74} true;

+    assume {:breadcrumb 31} true;

 }

 

 

 

 procedure RegressionTestInput.Class0.M$RegressionTestInput.Class0($this: Ref, c$in: Ref);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1537,12 +1569,13 @@ implementation RegressionTestInput.Class0.M$RegressionTestInput.Class0($this: Re
   var $label: int;

 

     c := c$in;

-    assume {:breadcrumb 75} true;

+    assume {:breadcrumb 32} true;

 }

 

 

 

 procedure RegressionTestInput.Class0.NonVoid($this: Ref) returns ($result: int);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1552,7 +1585,7 @@ implementation RegressionTestInput.Class0.NonVoid($this: Ref) returns ($result:
   var $localExc: Ref;

   var $label: int;

 

-    assume {:breadcrumb 76} true;

+    assume {:breadcrumb 33} true;

     call $tmp0 := RegressionTestInput.Class0.StaticMethod$System.Int32(3);

     if ($Exception != null)

     {

@@ -1566,6 +1599,7 @@ implementation RegressionTestInput.Class0.NonVoid($this: Ref) returns ($result:
 

 

 procedure RegressionTestInput.Class0.OutParam$System.Int32$($this: Ref, x$in: int) returns (x$out: int, $result: int);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1575,7 +1609,7 @@ implementation RegressionTestInput.Class0.OutParam$System.Int32$($this: Ref, x$i
   var $label: int;

 

     x$out := x$in;

-    assume {:breadcrumb 77} true;

+    assume {:breadcrumb 34} true;

     assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 37} true;

     assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 37} true;

     assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 37} true;

@@ -1587,6 +1621,7 @@ implementation RegressionTestInput.Class0.OutParam$System.Int32$($this: Ref, x$i
 

 

 procedure RegressionTestInput.Class0.RefParam$System.Int32$($this: Ref, x$in: int) returns (x$out: int, $result: int);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1596,7 +1631,7 @@ implementation RegressionTestInput.Class0.RefParam$System.Int32$($this: Ref, x$i
   var $label: int;

 

     x$out := x$in;

-    assume {:breadcrumb 78} true;

+    assume {:breadcrumb 35} true;

     assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 42} true;

     assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 42} true;

     assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 42} true;

@@ -1611,6 +1646,7 @@ implementation RegressionTestInput.Class0.RefParam$System.Int32$($this: Ref, x$i
 

 

 procedure RegressionTestInput.Class0.AssignToInParam$System.Int32($this: Ref, x$in: int) returns ($result: int);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1621,7 +1657,7 @@ implementation RegressionTestInput.Class0.AssignToInParam$System.Int32($this: Re
   var $label: int;

 

     x := x$in;

-    assume {:breadcrumb 79} true;

+    assume {:breadcrumb 36} true;

     assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 48} true;

     assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 48} true;

     x := x + 1;

@@ -1635,6 +1671,7 @@ implementation RegressionTestInput.Class0.AssignToInParam$System.Int32($this: Re
 

 

 procedure {:RegressionTestInput.Async} RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32($this: Ref, x$in: int) returns ($result: int);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1645,7 +1682,7 @@ implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMetho
   var $label: int;

 

     x := x$in;

-    assume {:breadcrumb 80} true;

+    assume {:breadcrumb 37} true;

     $result := x;

     return;

 }

@@ -1653,6 +1690,7 @@ implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMetho
 

 

 procedure RegressionTestInput.Class0.CallAsyncMethod$System.Int32($this: Ref, y$in: int) returns ($result: int);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1664,7 +1702,7 @@ implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int32($this: Re
   var $label: int;

 

     y := y$in;

-    assume {:breadcrumb 81} true;

+    assume {:breadcrumb 38} true;

     call {:async} $tmp0 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32($this, y);

     if ($Exception != null)

     {

@@ -1678,6 +1716,7 @@ implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int32($this: Re
 

 

 procedure RegressionTestInput.Class0.#ctor($this: Ref);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1686,7 +1725,7 @@ implementation RegressionTestInput.Class0.#ctor($this: Ref)
   var $localExc: Ref;

   var $label: int;

 

-    assume {:breadcrumb 82} true;

+    assume {:breadcrumb 39} true;

     call System.Object.#ctor($this);

     if ($Exception != null)

     {

@@ -1716,6 +1755,7 @@ var F$RegressionTestInput.ClassWithBoolTypes.staticB: bool;
 var F$RegressionTestInput.ClassWithBoolTypes.b: [Ref]bool;

 

 procedure RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(x$in: int, y$in: int) returns ($result: bool);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1728,7 +1768,7 @@ implementation RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3
 

     x := x$in;

     y := y$in;

-    assume {:breadcrumb 83} true;

+    assume {:breadcrumb 40} true;

     $result := x < y;

     return;

 }

@@ -1736,6 +1776,7 @@ implementation RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3
 

 

 procedure RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean($this: Ref, z$in: bool);

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1747,7 +1788,7 @@ implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean($this
 

     z := z$in;

     F$RegressionTestInput.ClassWithBoolTypes.b[$this] := false;

-    assume {:breadcrumb 84} true;

+    assume {:breadcrumb 41} true;

     assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 72} true;

     assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 72} true;

     call System.Object.#ctor($this);

@@ -1774,6 +1815,7 @@ implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean($this
 

 

 procedure RegressionTestInput.ClassWithBoolTypes.Main();

+  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

 

 

@@ -1783,7 +1825,7 @@ implementation RegressionTestInput.ClassWithBoolTypes.Main()
   var $localExc: Ref;

   var $label: int;

 

-    assume {:breadcrumb 85} true;

+    assume {:breadcrumb 42} true;

     assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 78} true;

     assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 78} true;

     call $tmp0 := RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(3, 4);

diff --git a/BCT/RegressionTests/TranslationTest/UnitTest0.cs b/BCT/RegressionTests/TranslationTest/UnitTest0.cs
index bd400303..62ce9155 100644
--- a/BCT/RegressionTests/TranslationTest/UnitTest0.cs
+++ b/BCT/RegressionTests/TranslationTest/UnitTest0.cs
@@ -61,7 +61,10 @@ namespace TranslationTest {
     #endregion

 

     private string ExecuteTest(string assemblyName, HeapFactory heapFactory) {

-      BCT.TranslateAssemblyAndWriteOutput(new List<string> { assemblyName }, heapFactory, new Options(), null, false);

+      var options = new Options();

+      options.monotonicHeap = true;

+      options.dereference = Options.Dereference.Assume;

+      BCT.TranslateAssemblyAndWriteOutput(new List<string> { assemblyName }, heapFactory, options, null, false);

       var fileName = Path.ChangeExtension(assemblyName, "bpl");

       var s = File.ReadAllText(fileName);

       return s;

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index ed80f6ac..1827b12e 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -564,6 +564,7 @@ namespace Microsoft.Boogie {
     public int StratifiedInliningOption = 0;

     public bool StratifiedInliningWithoutModels = false; // disable model generation for SI

     public int StratifiedInliningVerbose = 0; // verbosity level

+    public bool BctModeForStratifiedInlining = false;

     public int RecursionBound = 500;

     public bool NonUniformUnfolding = false;

     public string inferLeastForUnsat = null;

@@ -1009,6 +1010,12 @@ namespace Microsoft.Boogie {
             StratifiedInliningVerbose = Int32.Parse(cce.NonNull(args[ps.i]));

           }

           return true;

+        case "siBct":

+          if (ps.ConfirmArgumentCount(1))

+          {

+              BctModeForStratifiedInlining = (Int32.Parse(cce.NonNull(args[ps.i])) == 1);

+          }

+          return true;

         case "recursionBound":

           if (ps.ConfirmArgumentCount(1)) {

             RecursionBound = Int32.Parse(cce.NonNull(args[ps.i]));

diff --git a/Source/GPUVerify.sln b/Source/GPUVerify.sln
index a31d8600..4d515300 100644
--- a/Source/GPUVerify.sln
+++ b/Source/GPUVerify.sln
@@ -15,8 +15,6 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Graph", "Graph\Graph.csproj
 EndProject

 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ParserHelper", "ParserHelper\ParserHelper.csproj", "{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}"

 EndProject

-Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "BoogieDriver", "BoogieDriver\BoogieDriver.csproj", "{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}"

-EndProject

 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "AbsInt", "AbsInt\AbsInt.csproj", "{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}"

 EndProject

 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Houdini", "Houdini\Houdini.csproj", "{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}"

@@ -189,26 +187,6 @@ Global
 		{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|Mixed Platforms.ActiveCfg = Checked|Any CPU

 		{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|Mixed Platforms.Build.0 = Checked|Any CPU

 		{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|x86.ActiveCfg = Checked|Any CPU

-		{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Checked|Any CPU.ActiveCfg = Checked|Any CPU

-		{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Checked|Any CPU.Build.0 = Checked|Any CPU

-		{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU

-		{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Checked|Mixed Platforms.Build.0 = Checked|Any CPU

-		{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Checked|x86.ActiveCfg = Checked|Any CPU

-		{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Debug|Any CPU.ActiveCfg = Debug|Any CPU

-		{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Debug|Any CPU.Build.0 = Debug|Any CPU

-		{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU

-		{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU

-		{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Debug|x86.ActiveCfg = Debug|Any CPU

-		{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Release|Any CPU.ActiveCfg = Release|Any CPU

-		{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Release|Any CPU.Build.0 = Release|Any CPU

-		{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU

-		{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Release|Mixed Platforms.Build.0 = Release|Any CPU

-		{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Release|x86.ActiveCfg = Release|Any CPU

-		{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.z3apidebug|Any CPU.ActiveCfg = z3apidebug|Any CPU

-		{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.z3apidebug|Any CPU.Build.0 = z3apidebug|Any CPU

-		{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.z3apidebug|Mixed Platforms.ActiveCfg = z3apidebug|Any CPU

-		{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.z3apidebug|Mixed Platforms.Build.0 = z3apidebug|Any CPU

-		{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU

 		{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}.Checked|Any CPU.ActiveCfg = Checked|Any CPU

 		{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}.Checked|Any CPU.Build.0 = Checked|Any CPU

 		{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU

diff --git a/Source/GPUVerify/CommandLineOptions.cs b/Source/GPUVerify/CommandLineOptions.cs
index 8c090b6a..b2e54dbd 100644
--- a/Source/GPUVerify/CommandLineOptions.cs
+++ b/Source/GPUVerify/CommandLineOptions.cs
@@ -44,6 +44,8 @@ namespace GPUVerify
         public static bool ShowMayBeTidPlusConstantAnalysis = false;

         public static bool ShowArrayControlFlowAnalysis = false;

 

+        public static bool NoLoopPredicateInvariants = false;

+

         public static int Parse(string[] args)

         {

             for (int i = 0; i < args.Length; i++)

@@ -196,6 +198,11 @@ namespace GPUVerify
                     ShowArrayControlFlowAnalysis = true;

                     break;

 

+                    case "-noLoopPredicateInvariants":

+                    case "/noLoopPredicateInvariants":

+                    NoLoopPredicateInvariants = true;

+                    break;

+

                     default:

                         inputFiles.Add(args[i]);

                         break;

diff --git a/Source/GPUVerify/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj
index b767816c..9881b0f0 100644
--- a/Source/GPUVerify/GPUVerify.csproj
+++ b/Source/GPUVerify/GPUVerify.csproj
@@ -152,10 +152,6 @@
       <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>

       <Name>Basetypes</Name>

     </ProjectReference>

-    <ProjectReference Include="..\BoogieDriver\BoogieDriver.csproj">

-      <Project>{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}</Project>

-      <Name>BoogieDriver</Name>

-    </ProjectReference>

     <ProjectReference Include="..\Core\Core.csproj">

       <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>

       <Name>Core</Name>

diff --git a/Source/GPUVerify/Main.cs b/Source/GPUVerify/Main.cs
index b70260ce..48cd8a2f 100644
--- a/Source/GPUVerify/Main.cs
+++ b/Source/GPUVerify/Main.cs
@@ -28,7 +28,7 @@ namespace GPUVerify
 

             if (CommandLineOptions.inputFiles.Count < 1)

             {

-                OnlyBoogie.ErrorWriteLine("*** Error: No input files were specified.");

+                Console.WriteLine("*** Error: No input files were specified.");

                 Environment.Exit(1);

             }

 

@@ -41,7 +41,7 @@ namespace GPUVerify
                 }

                 if (extension != ".gbpl")

                 {

-                    OnlyBoogie.AdvisoryWriteLine("Warning '{0}': Should only pass filename with extension .gbpl. Input must be GBoogie programs.", file);

+                    Console.WriteLine("Warning '{0}': Should only pass filename with extension .gbpl. Input must be GBoogie programs.", file);

                 }

             }

 

@@ -220,14 +220,14 @@ namespace GPUVerify
                     errorCount = Parser.Parse(bplFileName, defines, out programSnippet);

                     if (programSnippet == null || errorCount != 0)

                     {

-                        OnlyBoogie.ErrorWriteLine("{0} parse errors detected in {1}", errorCount, bplFileName);

+                        Console.WriteLine("{0} parse errors detected in {1}", errorCount, bplFileName);

                         okay = false;

                         continue;

                     }

                 }

                 catch (IOException e)

                 {

-                    OnlyBoogie.ErrorWriteLine("Error opening file \"{0}\": {1}", bplFileName, e.Message);

+                    Console.WriteLine("Error opening file \"{0}\": {1}", bplFileName, e.Message);

                     okay = false;

                     continue;

                 }

diff --git a/Source/GPUVerify/Predicator.cs b/Source/GPUVerify/Predicator.cs
index 0950cd9a..316a3df6 100644
--- a/Source/GPUVerify/Predicator.cs
+++ b/Source/GPUVerify/Predicator.cs
@@ -251,7 +251,7 @@ namespace GPUVerify
                     VisitWhileInvariants(whileCmd.Invariants, NewGuard),

                     VisitStmtList(whileCmd.Body));

 

-                if (NewInvariant != null)

+                if (NewInvariant != null && !CommandLineOptions.NoLoopPredicateInvariants)

                 {

                     NewWhile.Invariants.Add(NewInvariant);

                 }

diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs
index f99c4651..b837e61a 100644
--- a/Source/Houdini/Checker.cs
+++ b/Source/Houdini/Checker.cs
@@ -22,8 +22,15 @@ namespace Microsoft.Boogie.Houdini {
     private VCExpr conjecture;

     private ProverInterface.ErrorHandler handler;

     ConditionGeneration.CounterexampleCollector collector;

+    HashSet<Variable> unsatCoreSet;

 

-    public HoudiniSession(VCGen vcgen, Checker checker, Program program, Implementation impl) {

+    public bool InUnsatCore(Variable constant) {

+      if (unsatCoreSet == null)

+        return true;

+      return unsatCoreSet.Contains(constant);

+    }

+

+    public HoudiniSession(VCGen vcgen, ProverInterface proverInterface, Program program, Implementation impl) {

       descriptiveName = impl.Name;

       collector = new ConditionGeneration.CounterexampleCollector();

       collector.OnProgress("HdnVCGen", 0, 0, 0.0);

@@ -33,36 +40,82 @@ namespace Microsoft.Boogie.Houdini {
       Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = vcgen.PassifyImpl(impl, program, out mvInfo);

       Hashtable/*<int, Absy!>*/ label2absy;

 

-      var exprGen = checker.TheoremProver.Context.ExprGen;

+      var exprGen = proverInterface.Context.ExprGen;

       VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : exprGen.Integer(BigNum.ZERO);

       

-      conjecture = vcgen.GenerateVC(impl, controlFlowVariableExpr, out label2absy, checker);

-

+      conjecture = vcgen.GenerateVC(impl, controlFlowVariableExpr, out label2absy, proverInterface.Context);

       if (!CommandLineOptions.Clo.UseLabels) {

         VCExpr controlFlowFunctionAppl = exprGen.ControlFlowFunctionApplication(exprGen.Integer(BigNum.ZERO), exprGen.Integer(BigNum.ZERO));

         VCExpr eqExpr = exprGen.Eq(controlFlowFunctionAppl, exprGen.Integer(BigNum.FromInt(impl.Blocks[0].UniqueId)));

         conjecture = exprGen.Implies(eqExpr, conjecture);

       }

 

+      Macro macro = new Macro(Token.NoToken, descriptiveName, new VariableSeq(), new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Type.Bool), false));

+      proverInterface.DefineMacro(macro, conjecture);

+      conjecture = exprGen.Function(macro);

+

       if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Local) {

-        handler = new VCGen.ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, vcgen.incarnationOriginMap, collector, mvInfo, vcgen.implName2LazyInliningInfo, checker.TheoremProver.Context, program);

+        handler = new VCGen.ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, vcgen.incarnationOriginMap, collector, mvInfo, vcgen.implName2LazyInliningInfo, proverInterface.Context, program);

       }

       else {

-        handler = new VCGen.ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, vcgen.incarnationOriginMap, collector, mvInfo, vcgen.implName2LazyInliningInfo, checker.TheoremProver.Context, program);

+        handler = new VCGen.ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, vcgen.incarnationOriginMap, collector, mvInfo, vcgen.implName2LazyInliningInfo, proverInterface.Context, program);

       }

     }

 

-    public ProverInterface.Outcome Verify(Checker checker, VCExpr axiom, out List<Counterexample> errors) {

+    private VCExpr BuildAxiom(ProverInterface proverInterface, Dictionary<Variable, bool> currentAssignment) {

+      ProverContext proverContext = proverInterface.Context;

+      Boogie2VCExprTranslator exprTranslator = proverContext.BoogieExprTranslator;

+      VCExpressionGenerator exprGen = proverInterface.VCExprGen;

+

+      VCExpr expr = VCExpressionGenerator.True;

+      foreach (KeyValuePair<Variable, bool> kv in currentAssignment) {

+        Variable constant = kv.Key;

+        VCExprVar exprVar = exprTranslator.LookupVariable(constant);

+        if (kv.Value) {

+          expr = exprGen.And(expr, exprVar);

+        }

+        else {

+          expr = exprGen.And(expr, exprGen.Not(exprVar));

+        }

+      }

+      return expr;

+    }

+

+    public ProverInterface.Outcome Verify(ProverInterface proverInterface, Dictionary<Variable, bool> assignment, out List<Counterexample> errors) {

       collector.examples.Clear();

-      VCExpr vc = checker.VCExprGen.Implies(axiom, conjecture);

+      VCExpr vc = proverInterface.VCExprGen.Implies(BuildAxiom(proverInterface, assignment), conjecture);

 

       if (CommandLineOptions.Clo.Trace) {

         Console.WriteLine("Verifying " + descriptiveName);

       }

       DateTime now = DateTime.UtcNow;

-      checker.BeginCheck(descriptiveName, vc, handler);

-      WaitHandle.WaitAny(new WaitHandle[] { checker.ProverDone });

-      ProverInterface.Outcome proverOutcome = checker.ReadOutcome();

+

+      proverInterface.BeginCheck(descriptiveName, vc, handler);

+      ProverInterface.Outcome proverOutcome = proverInterface.CheckOutcome(handler);

+

+#if UNSAT_CORE

+      Boogie2VCExprTranslator exprTranslator = proverInterface.Context.BoogieExprTranslator;

+      proverInterface.Push();

+      proverInterface.Assert(conjecture, false);

+      foreach (var v in assignment.Keys) {

+        if (assignment[v]) continue;

+        proverInterface.Assert(exprTranslator.LookupVariable(v), false);

+      }

+      List<Variable> assumptionVars = new List<Variable>();

+      List<VCExpr> assumptionExprs = new List<VCExpr>();

+      foreach (var v in assignment.Keys) {

+        if (!assignment[v]) continue;

+        assumptionVars.Add(v);

+        assumptionExprs.Add(exprTranslator.LookupVariable(v));

+      }

+      List<int> unsatCore;

+      ProverInterface.Outcome proverOutcome = proverInterface.CheckAssumptions(assumptionExprs, out unsatCore, handler);

+      unsatCoreSet = new HashSet<Variable>();

+      foreach (int i in unsatCore)

+        unsatCoreSet.Add(assumptionVars[i]);

+      proverInterface.Pop();

+#endif

+

       double queryTime = (DateTime.UtcNow - now).TotalSeconds;

       proverTime += queryTime;

       numProverQueries++;

diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index f6c334e7..5f60feff 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -39,7 +39,7 @@ namespace Microsoft.Boogie.Houdini {
     public virtual void UpdateStart(Program program, int numConstants) { }

     public virtual void UpdateIteration() { }

     public virtual void UpdateImplementation(Implementation implementation) { }

-    public virtual void UpdateAssignment(Dictionary<string, bool> assignment) { }

+    public virtual void UpdateAssignment(Dictionary<Variable, bool> assignment) { }

     public virtual void UpdateOutcome(ProverInterface.Outcome outcome) { }

     public virtual void UpdateEnqueue(Implementation implementation) { }

     public virtual void UpdateDequeue() { }

@@ -141,10 +141,10 @@ namespace Microsoft.Boogie.Houdini {
       wr.WriteLine("implementation under analysis :" + implementation.Name);

       wr.Flush();

     }

-    public override void UpdateAssignment(Dictionary<string, bool> assignment) {

+    public override void UpdateAssignment(Dictionary<Variable, bool> assignment) {

       bool firstTime = true;

       wr.Write("assignment under analysis : axiom (");

-      foreach (KeyValuePair<string, bool> kv in assignment) {

+      foreach (KeyValuePair<Variable, bool> kv in assignment) {

         if (!firstTime) wr.Write(" && "); else firstTime = false;

         string valString; // ugliness to get it lower cased

         if (kv.Value) valString = "true"; else valString = "false";

@@ -215,7 +215,7 @@ namespace Microsoft.Boogie.Houdini {
     protected void NotifyImplementation(Implementation implementation) {

       Notify((NotifyDelegate)delegate(HoudiniObserver r) { r.UpdateImplementation(implementation); });

     }

-    protected void NotifyAssignment(Dictionary<string, bool> assignment) {

+    protected void NotifyAssignment(Dictionary<Variable, bool> assignment) {

       Notify((NotifyDelegate)delegate(HoudiniObserver r) { r.UpdateAssignment(assignment); });

     }

     protected void NotifyOutcome(ProverInterface.Outcome outcome) {

@@ -279,6 +279,11 @@ namespace Microsoft.Boogie.Houdini {
     }

   }

 

+  public class Macro : Function {

+    public Macro(IToken tok, string name, VariableSeq args, Variable result)

+      : base(tok, name, args, result) { }

+  }

+

   public class FreeRequiresVisitor : StandardVisitor {

     public override Requires VisitRequires(Requires requires) {

       if (requires.Free)

@@ -298,13 +303,72 @@ namespace Microsoft.Boogie.Houdini {
 

   public class Houdini : ObservableHoudini {

     private Program program;

-    private ReadOnlyDictionary<string, IdentifierExpr> houdiniConstants;

+    private HashSet<Variable> houdiniConstants;

     private ReadOnlyDictionary<Implementation, HoudiniSession> houdiniSessions;

     private VCGen vcgen;

-    private Checker checker;

+    private ProverInterface proverInterface;

     private Graph<Implementation> callGraph;

     private HashSet<Implementation> vcgenFailures;

 

+

+    private ProverInterface CreateProver(Program prog, string/*?*/ logFilePath, bool appendLogFile, int timeout) {

+      Contract.Requires(prog != null);

+

+      ProverOptions options = cce.NonNull(CommandLineOptions.Clo.TheProverFactory).BlankProverOptions();

+

+      if (logFilePath != null) {

+        options.LogFilename = logFilePath;

+        if (appendLogFile)

+          options.AppendLogFile = appendLogFile;

+      }

+

+      if (timeout > 0) {

+        options.TimeLimit = timeout * 1000;

+      }

+

+      options.Parse(CommandLineOptions.Clo.ProverOptions);

+

+      ProverContext ctx = (ProverContext)CommandLineOptions.Clo.TheProverFactory.NewProverContext(options);

+

+      // set up the context

+      foreach (Declaration decl in prog.TopLevelDeclarations) {

+        Contract.Assert(decl != null);

+        TypeCtorDecl t = decl as TypeCtorDecl;

+        if (t != null) {

+          ctx.DeclareType(t, null);

+        }

+      }

+      foreach (Declaration decl in prog.TopLevelDeclarations) {

+        Contract.Assert(decl != null);

+        Constant c = decl as Constant;

+        if (c != null) {

+          ctx.DeclareConstant(c, c.Unique, null);

+        }

+        else {

+          Function f = decl as Function;

+          if (f != null) {

+            ctx.DeclareFunction(f, null);

+          }

+        }

+      }

+      foreach (Declaration decl in prog.TopLevelDeclarations) {

+        Contract.Assert(decl != null);

+        Axiom ax = decl as Axiom;

+        if (ax != null) {

+          ctx.AddAxiom(ax, null);

+        }

+      }

+      foreach (Declaration decl in prog.TopLevelDeclarations) {

+        Contract.Assert(decl != null);

+        GlobalVariable v = decl as GlobalVariable;

+        if (v != null) {

+          ctx.DeclareGlobalVariable(v, null);

+        }

+      }

+

+      return (ProverInterface) CommandLineOptions.Clo.TheProverFactory.SpawnProver(options, ctx);

+    }

+

     public Houdini(Program program) {

       this.program = program;

 

@@ -321,7 +385,7 @@ namespace Microsoft.Boogie.Houdini {
       Inline();

       

       this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);

-      this.checker = new Checker(vcgen, program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, CommandLineOptions.Clo.ProverKillTime);

+      this.proverInterface = CreateProver(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, CommandLineOptions.Clo.ProverKillTime);

 

       vcgenFailures = new HashSet<Implementation>();

       Dictionary<Implementation, HoudiniSession> houdiniSessions = new Dictionary<Implementation, HoudiniSession>();

@@ -331,7 +395,7 @@ namespace Microsoft.Boogie.Houdini {
         try {

           if (CommandLineOptions.Clo.Trace)

             Console.WriteLine("Generating VC for {0}", impl.Name);

-          HoudiniSession session = new HoudiniSession(vcgen, checker, program, impl);

+          HoudiniSession session = new HoudiniSession(vcgen, proverInterface, program, impl);

           houdiniSessions.Add(impl, session);

         }

         catch (VCGenException) {

@@ -395,19 +459,19 @@ namespace Microsoft.Boogie.Houdini {
       }

     }

 

-    private ReadOnlyDictionary<string, IdentifierExpr> CollectExistentialConstants() {

-      Dictionary<string, IdentifierExpr> existentialConstants = new Dictionary<string, IdentifierExpr>();

+    private HashSet<Variable> CollectExistentialConstants() {

+      HashSet<Variable> existentialConstants = new HashSet<Variable>();

       foreach (Declaration decl in program.TopLevelDeclarations) {

         Constant constant = decl as Constant;

         if (constant != null) {

           bool result = false;

           if (constant.CheckBooleanAttribute("existential", ref result)) {

             if (result == true)

-              existentialConstants.Add(constant.Name, new IdentifierExpr(Token.NoToken, constant));

+              existentialConstants.Add(constant);

           }

         }

       }

-      return new ReadOnlyDictionary<string, IdentifierExpr>(existentialConstants);

+      return existentialConstants;

     }

 

     private Graph<Implementation> BuildCallGraph() {

@@ -467,44 +531,23 @@ namespace Microsoft.Boogie.Houdini {
        */

     }

 

-    private bool MatchCandidate(Expr boogieExpr, out string candidateConstant) {

+    private bool MatchCandidate(Expr boogieExpr, out Variable candidateConstant) {

       candidateConstant = null;

       IExpr antecedent;

       IExpr expr = boogieExpr as IExpr;

       if (expr != null && ExprUtil.Match(expr, Prop.Implies, out antecedent)) {

         IdentifierExpr.ConstantFunApp constantFunApp = antecedent as IdentifierExpr.ConstantFunApp;

-        if (constantFunApp != null && houdiniConstants.ContainsKey(constantFunApp.IdentifierExpr.Name)) {

-          candidateConstant = constantFunApp.IdentifierExpr.Name;

+        if (constantFunApp != null && houdiniConstants.Contains(constantFunApp.IdentifierExpr.Decl)) {

+          candidateConstant = constantFunApp.IdentifierExpr.Decl;

           return true;

         }

       }

       return false;

     }

 

-    private VCExpr BuildAxiom(Dictionary<string, bool> currentAssignment) {

-      DeclFreeProverContext proverContext = (DeclFreeProverContext)checker.TheoremProver.Context;

-      Boogie2VCExprTranslator exprTranslator = proverContext.BoogieExprTranslator;

-      VCExpressionGenerator exprGen = checker.VCExprGen;

-

-      VCExpr expr = VCExpressionGenerator.True;

-      foreach (KeyValuePair<string, bool> kv in currentAssignment) {

-        IdentifierExpr constantExpr;

-        houdiniConstants.TryGetValue(kv.Key, out constantExpr);

-        Contract.Assume(constantExpr != null);

-        VCExprVar exprVar = exprTranslator.LookupVariable(constantExpr.Decl);

-        if (kv.Value) {

-          expr = exprGen.And(expr, exprVar);

-        }

-        else {

-          expr = exprGen.And(expr, exprGen.Not(exprVar));

-        }

-      }

-      return expr;

-    }

-

-    private Dictionary<string, bool> BuildAssignment(Dictionary<string, IdentifierExpr>.KeyCollection constants) {

-      Dictionary<string, bool> initial = new Dictionary<string, bool>();

-      foreach (string constant in constants)

+    private Dictionary<Variable, bool> BuildAssignment(HashSet<Variable> constants) {

+      Dictionary<Variable, bool> initial = new Dictionary<Variable, bool>();

+      foreach (var constant in constants)

         initial.Add(constant, true);

       return initial;

     }

@@ -547,7 +590,6 @@ namespace Microsoft.Boogie.Houdini {
 

     private void FlushWorkList(HoudiniState current) {

       this.NotifyFlushStart();

-      VCExpr axiom = BuildAxiom(current.Assignment);

       while (current.WorkQueue.Count > 0) {

         this.NotifyIteration();

 

@@ -557,7 +599,7 @@ namespace Microsoft.Boogie.Houdini {
         HoudiniSession session;

         houdiniSessions.TryGetValue(current.Implementation, out session);

         List<Counterexample> errors;

-        ProverInterface.Outcome outcome = TryCatchVerify(session, axiom, out errors);

+        ProverInterface.Outcome outcome = TryCatchVerify(session, current.Assignment, out errors);

         UpdateHoudiniOutcome(current.Outcome, current.Implementation, outcome, errors);

         this.NotifyOutcome(outcome);

 

@@ -573,24 +615,19 @@ namespace Microsoft.Boogie.Houdini {
       }

       current.Assignment.Remove(refAnnot.Constant);

       current.Assignment.Add(refAnnot.Constant, false);

-      this.NotifyConstant(refAnnot.Constant);

-    }

-

-    private void AddToWorkList(HoudiniState current, Implementation imp) {

-      if (!current.WorkQueue.Contains(imp) && !current.isBlackListed(imp.Name)) {

-        current.WorkQueue.Enqueue(imp);

-        this.NotifyEnqueue(imp);

-      }

+      this.NotifyConstant(refAnnot.Constant.Name);

     }

 

     private void AddRelatedToWorkList(HoudiniState current, RefutedAnnotation refutedAnnotation) {

       Contract.Assume(current.Implementation != null);

       foreach (Implementation implementation in FindImplementationsToEnqueue(refutedAnnotation, current.Implementation)) {

-        AddToWorkList(current, implementation);

+        if (!current.isBlackListed(implementation.Name)) {

+          current.WorkQueue.Enqueue(implementation);

+          this.NotifyEnqueue(implementation);

+        }

       }

     }

 

-

     // Updates the worklist and current assignment

     // @return true if the current function is dequeued

     private bool UpdateAssignmentWorkList(HoudiniState current,

@@ -654,11 +691,11 @@ namespace Microsoft.Boogie.Houdini {
     private class HoudiniState {

       private WorkQueue _workQueue;

       private HashSet<string> blackList;

-      private Dictionary<string, bool> _assignment;

+      private Dictionary<Variable, bool> _assignment;

       private Implementation _implementation;

       private HoudiniOutcome _outcome;

 

-      public HoudiniState(WorkQueue workQueue, Dictionary<string, bool> currentAssignment) {

+      public HoudiniState(WorkQueue workQueue, Dictionary<Variable, bool> currentAssignment) {

         this._workQueue = workQueue;

         this._assignment = currentAssignment;

         this._implementation = null;

@@ -669,7 +706,7 @@ namespace Microsoft.Boogie.Houdini {
       public WorkQueue WorkQueue {

         get { return this._workQueue; }

       }

-      public Dictionary<string, bool> Assignment {

+      public Dictionary<Variable, bool> Assignment {

         get { return this._assignment; }

       }

       public Implementation Implementation {

@@ -688,8 +725,8 @@ namespace Microsoft.Boogie.Houdini {
     }

 

     public HoudiniOutcome PerformHoudiniInference() {

-      HoudiniState current = new HoudiniState(BuildWorkList(program), BuildAssignment(houdiniConstants.Keys));

-      this.NotifyStart(program, houdiniConstants.Keys.Count);

+      HoudiniState current = new HoudiniState(BuildWorkList(program), BuildAssignment(houdiniConstants));

+      this.NotifyStart(program, houdiniConstants.Count);

       foreach (Implementation impl in vcgenFailures) {

         current.addToBlackList(impl.Name);

       }

@@ -705,23 +742,31 @@ namespace Microsoft.Boogie.Houdini {
         HoudiniVerifyCurrent(session, current);

       }

       this.NotifyEnd(true);

-      current.Outcome.assignment = current.Assignment;

+      Dictionary<string, bool> assignment = new Dictionary<string, bool>();

+      foreach (var x in current.Assignment)

+        assignment[x.Key.Name] = x.Value;

+      current.Outcome.assignment = assignment;

       return current.Outcome;

     }

 

     private List<Implementation> FindImplementationsToEnqueue(RefutedAnnotation refutedAnnotation, Implementation currentImplementation) {

+      HoudiniSession session;

       List<Implementation> implementations = new List<Implementation>();

       switch (refutedAnnotation.Kind) {

         case RefutedAnnotationKind.REQUIRES:

           foreach (Implementation callee in callGraph.Successors(currentImplementation)) {

+            houdiniSessions.TryGetValue(callee, out session);

             Contract.Assume(callee.Proc != null);

-            if (callee.Proc.Equals(refutedAnnotation.CalleeProc))

+            if (callee.Proc.Equals(refutedAnnotation.CalleeProc) && session.InUnsatCore(refutedAnnotation.Constant)) 

               implementations.Add(callee);

           }

           break;

         case RefutedAnnotationKind.ENSURES:

-          foreach (Implementation caller in callGraph.Predecessors(currentImplementation))

-            implementations.Add(caller);

+          foreach (Implementation caller in callGraph.Predecessors(currentImplementation)) {

+            houdiniSessions.TryGetValue(caller, out session);

+            if (session.InUnsatCore(refutedAnnotation.Constant))

+              implementations.Add(caller);

+          }

           break;

         case RefutedAnnotationKind.ASSERT: //the implementation is already in queue

           break;

@@ -734,11 +779,11 @@ namespace Microsoft.Boogie.Houdini {
     private enum RefutedAnnotationKind { REQUIRES, ENSURES, ASSERT };

 

     private class RefutedAnnotation {

-      private string _constant;

+      private Variable _constant;

       private RefutedAnnotationKind _kind;

       private Procedure _callee;

 

-      private RefutedAnnotation(string constant, RefutedAnnotationKind kind, Procedure callee) {

+      private RefutedAnnotation(Variable constant, RefutedAnnotationKind kind, Procedure callee) {

         this._constant = constant;

         this._kind = kind;

         this._callee = callee;

@@ -746,19 +791,19 @@ namespace Microsoft.Boogie.Houdini {
       public RefutedAnnotationKind Kind {

         get { return this._kind; }

       }

-      public string Constant {

+      public Variable Constant {

         get { return this._constant; }

       }

       public Procedure CalleeProc {

         get { return this._callee; }

       }

-      public static RefutedAnnotation BuildRefutedRequires(string constant, Procedure callee) {

+      public static RefutedAnnotation BuildRefutedRequires(Variable constant, Procedure callee) {

         return new RefutedAnnotation(constant, RefutedAnnotationKind.REQUIRES, callee);

       }

-      public static RefutedAnnotation BuildRefutedEnsures(string constant) {

+      public static RefutedAnnotation BuildRefutedEnsures(Variable constant) {

         return new RefutedAnnotation(constant, RefutedAnnotationKind.ENSURES, null);

       }

-      public static RefutedAnnotation BuildRefutedAssert(string constant) {

+      public static RefutedAnnotation BuildRefutedAssert(Variable constant) {

         return new RefutedAnnotation(constant, RefutedAnnotationKind.ASSERT, null);

       }

 

@@ -766,7 +811,7 @@ namespace Microsoft.Boogie.Houdini {
 

     private void PrintRefutedCall(CallCounterexample err, XmlSink xmlOut) {

       Expr cond = err.FailingRequires.Condition;

-      string houdiniConst;

+      Variable houdiniConst;

       if (MatchCandidate(cond, out houdiniConst)) {

         xmlOut.WriteError("precondition violation", err.FailingCall.tok, err.FailingRequires.tok, err.Trace);

       }

@@ -774,7 +819,7 @@ namespace Microsoft.Boogie.Houdini {
 

     private void PrintRefutedReturn(ReturnCounterexample err, XmlSink xmlOut) {

       Expr cond = err.FailingEnsures.Condition;

-      string houdiniConst;

+      Variable houdiniConst;

       if (MatchCandidate(cond, out houdiniConst)) {

         xmlOut.WriteError("postcondition violation", err.FailingReturn.tok, err.FailingEnsures.tok, err.Trace);

       }

@@ -782,7 +827,7 @@ namespace Microsoft.Boogie.Houdini {
 

     private void PrintRefutedAssert(AssertCounterexample err, XmlSink xmlOut) {

       Expr cond = err.FailingAssert.OrigExpr;

-      string houdiniConst;

+      Variable houdiniConst;

       if (MatchCandidate(cond, out houdiniConst)) {

         xmlOut.WriteError("postcondition violation", err.FailingAssert.tok, err.FailingAssert.tok, err.Trace);

       }

@@ -809,7 +854,7 @@ namespace Microsoft.Boogie.Houdini {
     }

 

     private RefutedAnnotation ExtractRefutedAnnotation(Counterexample error) {

-      string houdiniConstant;

+      Variable houdiniConstant;

       CallCounterexample callCounterexample = error as CallCounterexample;

       if (callCounterexample != null) {

         Procedure failingProcedure = callCounterexample.FailingCall.Proc;

@@ -839,10 +884,10 @@ namespace Microsoft.Boogie.Houdini {
       return null;

     }

 

-    private ProverInterface.Outcome TryCatchVerify(HoudiniSession session, VCExpr axiom, out List<Counterexample> errors) {

+    private ProverInterface.Outcome TryCatchVerify(HoudiniSession session, Dictionary<Variable, bool> assignment, out List<Counterexample> errors) {

       ProverInterface.Outcome outcome;

       try {

-        outcome = session.Verify(checker, axiom, out errors);

+        outcome = session.Verify(proverInterface, assignment, out errors);

       }

       catch (UnexpectedProverOutputException upo) {

         Contract.Assume(upo != null);

@@ -854,12 +899,11 @@ namespace Microsoft.Boogie.Houdini {
 

     private void HoudiniVerifyCurrent(HoudiniSession session, HoudiniState current) {

       while (true) {

-        VCExpr currentAx = BuildAxiom(current.Assignment);

         this.NotifyAssignment(current.Assignment);

 

         //check the VC with the current assignment

         List<Counterexample> errors;

-        ProverInterface.Outcome outcome = TryCatchVerify(session, currentAx, out errors);

+        ProverInterface.Outcome outcome = TryCatchVerify(session, current.Assignment, out errors);

         this.NotifyOutcome(outcome);

 

         DebugRefutedCandidates(current.Implementation, errors);

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 08322ebb..014af458 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -78,14 +78,14 @@ namespace Microsoft.Boogie.SMTLib
 

       SetupProcess();

 

-      if (CommandLineOptions.Clo.StratifiedInlining > 0)

+      if (CommandLineOptions.Clo.StratifiedInlining > 0 || CommandLineOptions.Clo.ContractInfer)

       {

           // Prepare for ApiChecker usage

           if (options.LogFilename != null && currentLogFile == null)

           {

               currentLogFile = OpenOutputFile("");

           }

-          if (CommandLineOptions.Clo.ProcedureCopyBound > 0)

+          if (CommandLineOptions.Clo.ProcedureCopyBound > 0 || CommandLineOptions.Clo.ContractInfer)

           {

               SendThisVC("(set-option :produce-unsat-cores true)");

               this.usingUnsatCore = true;

@@ -770,6 +770,14 @@ namespace Microsoft.Boogie.SMTLib
         SendThisVC(a);

     }

 

+    public override void DefineMacro(Function fun, VCExpr vc) {

+      DeclCollector.AddFunction(fun);

+      string name = Namer.GetName(fun, fun.Name);

+      string a = "(define-fun " + name + "() Bool " + VCExpr2String(vc, 1) + ")";

+      AssertAxioms();

+      SendThisVC(a);

+    }

+

     public override void AssertAxioms()

     {

         FlushAxioms();

@@ -805,7 +813,9 @@ namespace Microsoft.Boogie.SMTLib
             nameCounter++;

             nameToAssumption.Add(name, i);

 

-            SendThisVC(string.Format("(assert (! {0} :named {1}))", VCExpr2String(vc, 1), name));

+            string vcString = VCExpr2String(vc, 1);

+            AssertAxioms();

+            SendThisVC(string.Format("(assert (! {0} :named {1}))", vcString, name));

             i++;

         }

         Check();

diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs
index 05a6caf3..a4bdee51 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -164,6 +164,11 @@ void ObjectInvariant()
       return TypeToString(t);

     }

 

+    public void AddFunction(Function func) {

+      if (KnownFunctions.Contains(func))

+        return;

+      KnownFunctions.Add(func);

+    }

 

     public override bool Visit(VCExprNAry node, bool arg) {

       Contract.Requires(node != null);

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index f9999a74..9ebf4d63 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -851,9 +851,14 @@ namespace Microsoft.Boogie {
     public abstract ProverContext Context {

       get;

     }

+

     public abstract VCExpressionGenerator VCExprGen {

       get;

     }

+

+    public virtual void DefineMacro(Function fun, VCExpr vc) {

+      throw new NotImplementedException();

+    }

   }

 

   public class ProverInterfaceContracts : ProverInterface {

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index 98f20d21..ea17983f 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -210,7 +210,7 @@ namespace VC
             var bet = ctx.BoogieExprTranslator;

             VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : bet.LookupVariable(info.controlFlowVariable);

 

-            VCExpr vcexpr = gen.Not(GenerateVC(impl, controlFlowVariableExpr, out label2absy, checker));

+            VCExpr vcexpr = gen.Not(GenerateVC(impl, controlFlowVariableExpr, out label2absy, checker.TheoremProver.Context));

             Contract.Assert(vcexpr != null);

             if (!CommandLineOptions.Clo.UseLabels) {

               VCExpr controlFlowFunctionAppl = exprGen.ControlFlowFunctionApplication(controlFlowVariableExpr, exprGen.Integer(BigNum.ZERO));

@@ -438,8 +438,11 @@ namespace VC
                 checker2.Pop();

 

                 var end = DateTime.UtcNow;

-                Console.WriteLine("Summary computation took {0} sec and inferred {1} of {2} contracts", 

-                    (end - start).TotalSeconds, found, calls.allSummaryConst.Count);

+                if (CommandLineOptions.Clo.StratifiedInliningVerbose > 0)

+                {

+                    Console.WriteLine(">> Summary computation took {0} sec and inferred {1} of {2} contracts",

+                        (end - start).TotalSeconds, found, calls.allSummaryConst.Count);

+                }

 

             }

 

@@ -1263,7 +1266,7 @@ namespace VC
             Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = PassifyImpl(impl, program, out mvInfo);

             var exprGen = checker.TheoremProver.Context.ExprGen;

             VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : exprGen.Integer(BigNum.ZERO); 

-            vcMain = GenerateVC(impl, controlFlowVariableExpr, out mainLabel2absy, checker);

+            vcMain = GenerateVC(impl, controlFlowVariableExpr, out mainLabel2absy, checker.TheoremProver.Context);

             if (!CommandLineOptions.Clo.UseLabels) {

               VCExpr controlFlowFunctionAppl = exprGen.ControlFlowFunctionApplication(exprGen.Integer(BigNum.ZERO), exprGen.Integer(BigNum.ZERO));

               VCExpr eqExpr = exprGen.Eq(controlFlowFunctionAppl, exprGen.Integer(BigNum.FromInt(impl.Blocks[0].UniqueId)));

@@ -1570,7 +1573,7 @@ namespace VC
 

                 foreach (int id in calls.currCandidates)

                 {

-                    if (calls.isNonTrivialCandidate(id) && calls.getRecursionBound(id) <= CommandLineOptions.Clo.RecursionBound)

+                    if (calls.getRecursionBound(id) <= CommandLineOptions.Clo.RecursionBound)

                     {

                         toExpand.Add(id);

                     }

@@ -1754,7 +1757,14 @@ namespace VC
                         if (CommandLineOptions.Clo.StratifiedInliningVerbose > 0)

                         {

                             Console.Write(">> SI Inlining: ");

-                            reporter.candidatesToExpand.ForEach(c => Console.Write("{0} ", calls.getProc(c)));

+                            reporter.candidatesToExpand.ForEach(c =>

+                                { if (!calls.isSkipped(c)) Console.Write("{0} ", calls.getProc(c)); });

+

+                            Console.WriteLine();

+                            Console.Write(">> SI Skipping: ");

+                            reporter.candidatesToExpand.ForEach(c =>

+                            { if (calls.isSkipped(c)) Console.Write("{0} ", calls.getProc(c)); });

+

                             Console.WriteLine();

                         }

                         // Expand and try again

@@ -1790,7 +1800,7 @@ namespace VC
                 Console.WriteLine(">> SI: Calls to Z3: {0}", vState.numQueries);

                 Console.WriteLine(">> SI: Expansions performed: {0}", vState.expansionCount);

                 Console.WriteLine(">> SI: Candidates left: {0}", calls.currCandidates.Count);

-                Console.WriteLine(">> SI: Nontrivial Candidates left: {0}", calls.numNonTrivialCandidates());

+                Console.WriteLine(">> SI: Candidates skipped: {0}", calls.currCandidates.Where(i => calls.isSkipped(i)).Count());

                 Console.WriteLine(">> SI: VC Size: {0}", vState.vcSize);

             }

             #endregion

@@ -2171,11 +2181,11 @@ namespace VC
             reporter.underapproximationMode = true;

             checker.LogComment(";;;;;;;;;;;; Underapprox mode begin ;;;;;;;;;;");

             List<VCExpr> assumptions = new List<VCExpr>();

-            List<int> ids = new List<int>();

+            

             foreach (int id in calls.currCandidates)

             {

-                assumptions.Add(calls.getFalseExpr(id));

-                ids.Add(id);

+                if (!calls.isSkipped(id))

+                    assumptions.Add(calls.getFalseExpr(id));

             }

             Outcome ret = checker.CheckAssumptions(assumptions);

             checker.LogComment(";;;;;;;;;;;; Underapprox mode end ;;;;;;;;;;");

@@ -2211,11 +2221,14 @@ namespace VC
 

             foreach (int id in calls.currCandidates)

             {

+                if (calls.isSkipped(id)) continue;

+

                 int idBound = calls.getRecursionBound(id);

                 if (idBound <= bound)

                 {

                     if (idBound > 1)

                       softAssumptions.Add(calls.getFalseExpr(id));

+

                     if (block.Contains(id))

                     {

                         Contract.Assert(useSummary);

@@ -2287,6 +2300,9 @@ namespace VC
 

         // Does on-demand inlining -- pushes procedure bodies on the theorem prover stack.

         private void DoExpansion(bool incremental, List<int>/*!*/ candidates, VerificationState vState) {

+          // Skipped calls don't get inlined

+          candidates = candidates.FindAll(id => !vState.calls.isSkipped(id));

+

           vState.expansionCount += candidates.Count;

 

           if (incremental)

@@ -2503,7 +2519,7 @@ namespace VC
             var exprGen = checker.TheoremProver.Context.ExprGen;

             VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : exprGen.Integer(BigNum.ZERO);

 

-            vc = GenerateVC(impl, controlFlowVariableExpr, out label2absy, checker);

+            vc = GenerateVC(impl, controlFlowVariableExpr, out label2absy, checker.TheoremProver.Context);

 

             if (!CommandLineOptions.Clo.UseLabels) {

               VCExpr controlFlowFunctionAppl = exprGen.ControlFlowFunctionApplication(exprGen.Integer(BigNum.ZERO), exprGen.Integer(BigNum.ZERO));

@@ -2859,37 +2875,23 @@ namespace VC
                 return cce.NonNull(implName2StratifiedInliningInfo[currProc].label2absy);

             }

 

-            // How many of the current candidates represent calls to procedures

-            // with non-trivial mod sets.

-            // This is only used for statistic purposes

-            public bool isNonTrivialCandidate(int id)

+            // Is this candidate a "skipped" call

+            // Currently this is experimental

+            public bool isSkipped(int id)

             {

-                string proc = getProc(id);

-                if (proc == "") return false;

-                if (!implName2StratifiedInliningInfo.ContainsKey(proc)) return false;

-                var info = implName2StratifiedInliningInfo[proc];

-                if (info.impl.Proc.Modifies.Length != 0) return true;

-                return false;

-                /*

-                foreach (IdentifierExpr ie in info.impl.Proc.Modifies)

-                {

-                    if (ie.Decl.Name.StartsWith("Mem_") || ie.Decl.Name.StartsWith("Res_"))

-                    {

-                        return true;

-                    }

-                }

-                return false;

-                 */

-            }

+                if (!CommandLineOptions.Clo.BctModeForStratifiedInlining) return false;

 

-            public int numNonTrivialCandidates()

-            {

-                int ret = 0;

-                foreach (int id in currCandidates)

-                {

-                    if (isNonTrivialCandidate(id)) ret++;

-                }

-                return ret;

+                var proc = getProc(id);

+                if (!implName2StratifiedInliningInfo.ContainsKey(proc)) return false;

+                var modSet = new HashSet<string>();

+                implName2StratifiedInliningInfo[proc].impl.Proc.Modifies

+                    .Cast<IdentifierExpr>()

+                    .Select(ie => ie.Decl.Name)

+                    .Iter(s => modSet.Add(s));

+                modSet.Remove("$Alloc");

+                modSet.Remove("assertsPassed");

+                modSet.Remove("$Exception");

+                return modSet.Count == 0;

             }

 

             // Finds labels and changes them:

@@ -3453,7 +3455,7 @@ namespace VC
                 if (underapproximationMode)

                 {

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

-                    Debug.Assert(candidatesToExpand.Count == 0);

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

                     if (cex != null) {

                       GetModelWithStates(model);

                       callback.OnCounterexample(cex, null);

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 008810cb..5761ca70 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -611,7 +611,7 @@ namespace VC {
         var exprGen = ch.TheoremProver.Context.ExprGen;

         VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : exprGen.Integer(BigNum.ZERO);

 

-        VCExpr vc = parent.GenerateVC(impl, controlFlowVariableExpr, out label2Absy, ch);

+        VCExpr vc = parent.GenerateVC(impl, controlFlowVariableExpr, out label2Absy, ch.TheoremProver.Context);

         Contract.Assert(vc != null);

 

         if (!CommandLineOptions.Clo.UseLabels) {

@@ -1550,7 +1550,7 @@ namespace VC {
         var exprGen = ctx.ExprGen;

         VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : exprGen.Integer(BigNum.ZERO);

 

-        VCExpr vc = parent.GenerateVCAux(impl, controlFlowVariableExpr, label2absy, checker);

+        VCExpr vc = parent.GenerateVCAux(impl, controlFlowVariableExpr, label2absy, checker.TheoremProver.Context);

         Contract.Assert(vc != null);

 

         if (!CommandLineOptions.Clo.UseLabels) {

@@ -1630,20 +1630,20 @@ namespace VC {
     }

     #endregion

 

-    public VCExpr GenerateVC(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, out Hashtable/*<int, Absy!>*//*!*/ label2absy, Checker/*!*/ ch)

+    public VCExpr GenerateVC(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, out Hashtable/*<int, Absy!>*//*!*/ label2absy, ProverContext proverContext)

     {

       Contract.Requires(impl != null);

-      Contract.Requires(ch != null);

+      Contract.Requires(proverContext != null);

       Contract.Ensures(Contract.ValueAtReturn(out label2absy) != null);

       Contract.Ensures(Contract.Result<VCExpr>() != null);

 

       label2absy = new Hashtable/*<int, Absy!>*/();

-      return GenerateVCAux(impl, controlFlowVariableExpr, label2absy, ch);

+      return GenerateVCAux(impl, controlFlowVariableExpr, label2absy, proverContext);

     }

 

-    protected VCExpr GenerateVCAux(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, Hashtable/*<int, Absy!>*//*!*/ label2absy, Checker/*!*/ ch) {

+    protected VCExpr GenerateVCAux(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, Hashtable/*<int, Absy!>*//*!*/ label2absy, ProverContext proverContext) {

       Contract.Requires(impl != null);

-      Contract.Requires(ch != null);

+      Contract.Requires(proverContext != null);

       Contract.Ensures(Contract.Result<VCExpr>() != null);

 

       TypecheckingContext tc = new TypecheckingContext(null);

@@ -1653,35 +1653,35 @@ namespace VC {
       int assertionCount;

       switch (CommandLineOptions.Clo.vcVariety) {

         case CommandLineOptions.VCVariety.Structured:

-          vc = VCViaStructuredProgram(impl, label2absy, ch.TheoremProver.Context, out assertionCount);

+          vc = VCViaStructuredProgram(impl, label2absy, proverContext, out assertionCount);

           break;

         case CommandLineOptions.VCVariety.Block:

-          vc = FlatBlockVC(impl, label2absy, false, false, false, ch.TheoremProver.Context, out assertionCount);

+          vc = FlatBlockVC(impl, label2absy, false, false, false, proverContext, out assertionCount);

           break;

         case CommandLineOptions.VCVariety.BlockReach:

-          vc = FlatBlockVC(impl, label2absy, false, true, false, ch.TheoremProver.Context, out assertionCount);

+          vc = FlatBlockVC(impl, label2absy, false, true, false, proverContext, out assertionCount);

           break;

         case CommandLineOptions.VCVariety.Local:

-          vc = FlatBlockVC(impl, label2absy, true, false, false, ch.TheoremProver.Context, out assertionCount);

+          vc = FlatBlockVC(impl, label2absy, true, false, false, proverContext, out assertionCount);

           break;

         case CommandLineOptions.VCVariety.BlockNested:

-          vc = NestedBlockVC(impl, label2absy, false, ch.TheoremProver.Context, out assertionCount);

+          vc = NestedBlockVC(impl, label2absy, false, proverContext, out assertionCount);

           break;

         case CommandLineOptions.VCVariety.BlockNestedReach:

-          vc = NestedBlockVC(impl, label2absy, true, ch.TheoremProver.Context, out assertionCount);

+          vc = NestedBlockVC(impl, label2absy, true, proverContext, out assertionCount);

           break;

         case CommandLineOptions.VCVariety.Dag:

           if (cce.NonNull(CommandLineOptions.Clo.TheProverFactory).SupportsDags) {

-            vc = DagVC(cce.NonNull(impl.Blocks[0]), controlFlowVariableExpr, label2absy, new Hashtable/*<Block, VCExpr!>*/(), ch.TheoremProver.Context, out assertionCount);

+            vc = DagVC(cce.NonNull(impl.Blocks[0]), controlFlowVariableExpr, label2absy, new Hashtable/*<Block, VCExpr!>*/(), proverContext, out assertionCount);

           } else {

-            vc = LetVC(cce.NonNull(impl.Blocks[0]), controlFlowVariableExpr, label2absy, ch.TheoremProver.Context, out assertionCount);

+            vc = LetVC(cce.NonNull(impl.Blocks[0]), controlFlowVariableExpr, label2absy, proverContext, out assertionCount);

           }

           break;

         case CommandLineOptions.VCVariety.DagIterative:

-          vc = LetVCIterative(impl.Blocks, controlFlowVariableExpr, label2absy, ch.TheoremProver.Context, out assertionCount);

+          vc = LetVCIterative(impl.Blocks, controlFlowVariableExpr, label2absy, proverContext, out assertionCount);

           break;

         case CommandLineOptions.VCVariety.Doomed:

-          vc = FlatBlockVC(impl, label2absy, false, false, true, ch.TheoremProver.Context, out assertionCount);

+          vc = FlatBlockVC(impl, label2absy, false, false, true, proverContext, out assertionCount);

           break;

         default:

           Contract.Assert(false);

diff --git a/_admin/Boogie/aste/summary.log b/_admin/Boogie/aste/summary.log
index 84f7c157..6a7862c5 100644
--- a/_admin/Boogie/aste/summary.log
+++ b/_admin/Boogie/aste/summary.log
@@ -1,15 +1,15 @@
-# Aste started: 2012-03-12 07:00:05

+# Aste started: 2012-04-18 07:00:01

 # Host id: Boogiebox

 # Configuration: boogie.cfg

 # Task: aste.tasks.boogie.FullBuild

-# [2012-03-12 07:05:12] SpecSharp revision: e3878dffb70b

-# [2012-03-12 07:05:12] SscBoogie revision: e3878dffb70b

-# [2012-03-12 07:08:40] Boogie revision: b0709df982cd

-[2012-03-12 07:10:18] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com SpecSharp.sln /Project "Checkin Tests" /Build

+# [2012-04-18 07:00:59] SpecSharp revision: caeb8178d12f

+# [2012-04-18 07:00:59] SscBoogie revision: caeb8178d12f

+# [2012-04-18 07:03:19] Boogie revision: 0bec765e8854

+[2012-04-18 07:04:57] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com SpecSharp.sln /Project "Checkin Tests" /Build

 

     1>corflags : warning CF011: The specified file is strong name signed.  Using /Force will invalidate the signature of this image and will require the assembly to be resigned.


     warning CF011: The specified file is strong name signed.  Using /Force will invalidate the signature of this image and will require the assembly to be resigned.


-[2012-03-12 07:11:45] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com Boogie.sln /Rebuild Checked

+[2012-04-18 07:06:25] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com Boogie.sln /Rebuild Checked

 

     D:\Temp\aste\Boogie\Source\Core\AbsyType.cs(823,16): warning CS0659: 'Microsoft.Boogie.BasicType' overrides Object.Equals(object o) but does not override Object.GetHashCode()


     D:\Temp\aste\Boogie\Source\Core\AbsyType.cs(2802,16): warning CS0659: 'Microsoft.Boogie.CtorType' overrides Object.Equals(object o) but does not override Object.GetHashCode()


@@ -24,6 +24,7 @@
     D:\Temp\aste\Boogie\Source\AbsInt\IntervalDomain.cs(49,9): warning CC1036: Detected call to method 'Microsoft.Boogie.AbstractInterpretation.NativeIntervallDomain+Node.StrictlyBefore(Microsoft.Boogie.Variable,Microsoft.Boogie.Variable)' without [Pure] in contracts of method 'Microsoft.Boogie.AbstractInterpretation.NativeIntervallDomain+Node.#ctor(Microsoft.Boogie.Variable,System.Nullable`1<System.Numerics.BigInteger>,System.Nullable`1<System.Numerics.BigInteger>,Microsoft.Boogie.AbstractInterpretation.NativeIntervallDomain+Node)'.


     D:\Temp\aste\Boogie\Source\VCGeneration\VC.cs(1717,11): warning CS0162: Unreachable code detected


     D:\Temp\aste\Boogie\Source\VCGeneration\VC.cs(1878,11): warning CS0162: Unreachable code detected


+    D:\Temp\aste\Boogie\Source\Houdini\Checker.cs(25,23): warning CS0649: Field 'Microsoft.Boogie.Houdini.HoudiniSession.unsatCoreSet' is never assigned to, and will always have its default value null


     EXEC : warning CC1032: Method 'Microsoft.Boogie.Houdini.InlineRequiresVisitor.VisitCmdSeq(Microsoft.Boogie.CmdSeq)' overrides 'Microsoft.Boogie.StandardVisitor.VisitCmdSeq(Microsoft.Boogie.CmdSeq)', thus cannot add Requires.


     EXEC : warning CC1032: Method 'Microsoft.Boogie.Houdini.FreeRequiresVisitor.VisitAssertRequiresCmd(Microsoft.Boogie.AssertRequiresCmd)' overrides 'Microsoft.Boogie.StandardVisitor.VisitAssertRequiresCmd(Microsoft.Boogie.AssertRequiresCmd)', thus cannot add Requires.


     warning CS0659: 'Microsoft.Boogie.BasicType' overrides Object.Equals(object o) but does not override Object.GetHashCode()


@@ -39,7 +40,8 @@
     warning CC1036: Detected call to method 'Microsoft.Boogie.AbstractInterpretation.NativeIntervallDomain+Node.StrictlyBefore(Microsoft.Boogie.Variable,Microsoft.Boogie.Variable)' without [Pure] in contracts of method 'Microsoft.Boogie.AbstractInterpretation.NativeIntervallDomain+Node.#ctor(Microsoft.Boogie.Variable,System.Nullable`1<System.Numerics.BigInteger>,System.Nullable`1<System.Numerics.BigInteger>,Microsoft.Boogie.AbstractInterpretation.NativeIntervallDomain+Node)'.


     warning CS0162: Unreachable code detected


     warning CS0162: Unreachable code detected


+    warning CS0649: Field 'Microsoft.Boogie.Houdini.HoudiniSession.unsatCoreSet' is never assigned to, and will always have its default value null


     warning CC1032: Method 'Microsoft.Boogie.Houdini.InlineRequiresVisitor.VisitCmdSeq(Microsoft.Boogie.CmdSeq)' overrides 'Microsoft.Boogie.StandardVisitor.VisitCmdSeq(Microsoft.Boogie.CmdSeq)', thus cannot add Requires.


     warning CC1032: Method 'Microsoft.Boogie.Houdini.FreeRequiresVisitor.VisitAssertRequiresCmd(Microsoft.Boogie.AssertRequiresCmd)' overrides 'Microsoft.Boogie.StandardVisitor.VisitAssertRequiresCmd(Microsoft.Boogie.AssertRequiresCmd)', thus cannot add Requires.


-[2012-03-12 08:11:41] 0 out of 33 test(s) in D:\Temp\aste\Boogie\Test\alltests.txt failed

-# [2012-03-12 08:12:49] Released nightly of Boogie

+[2012-04-18 08:05:01] 0 out of 33 test(s) in D:\Temp\aste\Boogie\Test\alltests.txt failed

+# [2012-04-18 08:05:43] Released nightly of Boogie