Uniformity analysis. Patch by Peter Collingbourne.

4 files changed, 1318 insertions, 696 deletions

diff --git a/Source/VCGeneration/GraphAlgorithms.cs b/Source/VCGeneration/GraphAlgorithms.cs
index 1a8ab9b1..006a923f 100644
--- a/Source/VCGeneration/GraphAlgorithms.cs
+++ b/Source/VCGeneration/GraphAlgorithms.cs
@@ -93,6 +93,34 @@ public static class GraphAlgorithms {
 
     return sortedNodes;
   }
+  
+  // Algorithm from Jeanne Ferrante, Karl J. Ottenstein, Joe D. Warren,
+  // "The Program Dependence Graph and Its Use in Optimization"
+  public static Dictionary<Node, HashSet<Node>> ControlDependence<Node>(this Graph<Node> g) where Node : class, new() {
+    Graph<Node> dual = g.Dual(new Node());
+    DomRelation<Node> pdom = dual.DominatorMap;
+    var result = new Dictionary<Node, HashSet<Node>>();
+
+    var S = g.Edges.Where(e => !pdom.DominatedBy(e.Item1, e.Item2));
+    foreach (var edge in S) {
+      var L = pdom.LeastCommonAncestor(edge.Item1, edge.Item2);
+      var deps = new List<Node>();
+      if (L == edge.Item1) {
+        pdom.DominatedBy(edge.Item2, edge.Item1, deps);
+        deps.Add(edge.Item2);
+        deps.Add(edge.Item1);
+      } else {
+        pdom.DominatedBy(edge.Item2, L, deps);
+        deps.Add(edge.Item2);
+      }
+      if (result.ContainsKey(edge.Item1)) {
+        result[edge.Item1].UnionWith(deps);
+      } else {
+        result[edge.Item1] = new HashSet<Node>(deps);
+      }
+    }
+    return result;
+  }
 
 }
 
diff --git a/Source/VCGeneration/SmartBlockPredicator.cs b/Source/VCGeneration/SmartBlockPredicator.cs
index f769822c..9dada1a5 100644
--- a/Source/VCGeneration/SmartBlockPredicator.cs
+++ b/Source/VCGeneration/SmartBlockPredicator.cs
@@ -1,469 +1,523 @@
-using Graphing;

-using System;

-using System.Collections.Generic;

-using System.Diagnostics;

-using System.Diagnostics.Contracts;

-using System.Linq;

-

-namespace Microsoft.Boogie {

-

-public class SmartBlockPredicator {

-

-  Program prog;

-  Implementation impl;

-  Graph<Block> blockGraph;

-  List<Tuple<Block, bool>> sortedBlocks;

-

-  bool useProcedurePredicates = true;

-

-  Dictionary<Block, Variable> predMap, defMap;

-  Dictionary<Block, HashSet<Variable>> ownedMap;

-  Dictionary<Block, Block> parentMap;

-  Dictionary<Block, PartInfo> partInfo;

-

-  IdentifierExpr fp;

-  Dictionary<Microsoft.Boogie.Type, IdentifierExpr> havocVars =

-    new Dictionary<Microsoft.Boogie.Type, IdentifierExpr>();

-  Dictionary<Block, Expr> blockIds = new Dictionary<Block, Expr>();

-  HashSet<Block> doneBlocks = new HashSet<Block>();

-

-  SmartBlockPredicator(Program p, Implementation i, bool upp) {

-    prog = p;

-    impl = i;

-    useProcedurePredicates = upp;

-  }

-

-  void PredicateCmd(Expr p, List<Block> blocks, Block block, Cmd cmd, out Block nextBlock) {

-    if (!useProcedurePredicates && cmd is CallCmd) {

-      var trueBlock = new Block();

-      blocks.Add(trueBlock);

-      trueBlock.Label = block.Label + ".call.true";

-      trueBlock.Cmds.Add(new AssumeCmd(Token.NoToken, p));

-      trueBlock.Cmds.Add(cmd);

-

-      var falseBlock = new Block();

-      blocks.Add(falseBlock);

-      falseBlock.Label = block.Label + ".call.false";

-      falseBlock.Cmds.Add(new AssumeCmd(Token.NoToken, Expr.Not(p)));

-

-      var contBlock = new Block();

-      blocks.Add(contBlock);

-      contBlock.Label = block.Label + ".call.cont";

-

-      block.TransferCmd =

-        new GotoCmd(Token.NoToken, new BlockSeq(trueBlock, falseBlock));

-      trueBlock.TransferCmd = falseBlock.TransferCmd =

-        new GotoCmd(Token.NoToken, new BlockSeq(contBlock));

-      nextBlock = contBlock;

-    } else {

-      PredicateCmd(p, block.Cmds, cmd);

-      nextBlock = block;

-    }

-  }

-

-  void PredicateCmd(Expr p, CmdSeq cmdSeq, Cmd cmd) {

-    if (p == null) {

-      cmdSeq.Add(cmd);

-      return;

-    }

-

-    if (cmd is AssignCmd) {

-      var aCmd = (AssignCmd)cmd;

-      cmdSeq.Add(new AssignCmd(Token.NoToken, aCmd.Lhss,

-                   new List<Expr>(aCmd.Lhss.Zip(aCmd.Rhss, (lhs, rhs) =>

-                     new NAryExpr(Token.NoToken,

-                       new IfThenElse(Token.NoToken),

-                       new ExprSeq(p, rhs, lhs.AsExpr))))));

-    } else if (cmd is AssertCmd) {

-      var aCmd = (AssertCmd)cmd;

-      Expr newExpr = new EnabledReplacementVisitor(p).VisitExpr(aCmd.Expr);

-      aCmd.Expr = QKeyValue.FindBoolAttribute(aCmd.Attributes, "do_not_predicate") ? newExpr : Expr.Imp(p, newExpr);

-      cmdSeq.Add(aCmd);

-    } else if (cmd is AssumeCmd) {

-      var aCmd = (AssumeCmd)cmd;

-      cmdSeq.Add(new AssumeCmd(Token.NoToken, Expr.Imp(p, aCmd.Expr)));

-    } else if (cmd is HavocCmd) {

-      var hCmd = (HavocCmd)cmd;

-      foreach (IdentifierExpr v in hCmd.Vars) {

-        Microsoft.Boogie.Type type = v.Decl.TypedIdent.Type;

-        Contract.Assert(type != null);

-

-        IdentifierExpr havocTempExpr;

-        if (havocVars.ContainsKey(type)) {

-          havocTempExpr = havocVars[type];

-        } else {

-          var havocVar = new LocalVariable(Token.NoToken,

-                             new TypedIdent(Token.NoToken,

-                                            "_HAVOC_" + type.ToString(), type));

-          impl.LocVars.Add(havocVar);

-          havocVars[type] = havocTempExpr =

-            new IdentifierExpr(Token.NoToken, havocVar);

-        }

-        cmdSeq.Add(new HavocCmd(Token.NoToken,

-                                new IdentifierExprSeq(havocTempExpr)));

-        cmdSeq.Add(Cmd.SimpleAssign(Token.NoToken, v,

-                                    new NAryExpr(Token.NoToken,

-                                      new IfThenElse(Token.NoToken),

-                                      new ExprSeq(p, havocTempExpr, v))));

-      }

-    } else if (cmd is CallCmd) {

-      Debug.Assert(useProcedurePredicates);

-      var cCmd = (CallCmd)cmd;

-      cCmd.Ins.Insert(0, p);

-      cmdSeq.Add(cCmd);

-    }

-    else if (cmd is CommentCmd) {

-      // skip

-    }

-    else if (cmd is StateCmd) {

-      var sCmd = (StateCmd)cmd;

-      var newCmdSeq = new CmdSeq();

-      foreach (Cmd c in sCmd.Cmds)

-        PredicateCmd(p, newCmdSeq, c);

-      sCmd.Cmds = newCmdSeq;

-      cmdSeq.Add(sCmd);

-    }

-    else {

-      Console.WriteLine("Unsupported cmd: " + cmd.GetType().ToString());

-    }

-  }

-

-  void PredicateTransferCmd(Expr p, Block src, CmdSeq cmdSeq, TransferCmd cmd) {

-    if (cmd is GotoCmd) {

-      var gCmd = (GotoCmd)cmd;

-      if (gCmd.labelTargets.Length == 1) {

-        if (defMap.ContainsKey(gCmd.labelTargets[0]))

-          PredicateCmd(p, cmdSeq,

-                       Cmd.SimpleAssign(Token.NoToken,

-                                        Expr.Ident(predMap[gCmd.labelTargets[0]]), Expr.True));

-      } else {

-        Debug.Assert(gCmd.labelTargets.Length > 1);

-        Debug.Assert(gCmd.labelTargets.Cast<Block>().All(t => partInfo.ContainsKey(t)));

-        foreach (Block target in gCmd.labelTargets) {

-          var part = partInfo[target];

-          if (defMap.ContainsKey(part.realDest))

-            PredicateCmd(p, cmdSeq,

-                         Cmd.SimpleAssign(Token.NoToken,

-                                          Expr.Ident(predMap[part.realDest]), part.pred));

-          var predsExitingLoop = new Dictionary<Block, List<Expr>>();

-          foreach (Block exit in LoopsExited(src, target)) {

-            List<Expr> predList;

-            if (!predsExitingLoop.ContainsKey(exit))

-              predList = predsExitingLoop[exit] = new List<Expr>();

-            else

-              predList = predsExitingLoop[exit];

-            predList.Add(part.pred);

-          }

-          foreach (var pred in predsExitingLoop) {

-            PredicateCmd(p, cmdSeq,

-                         Cmd.SimpleAssign(Token.NoToken,

-                                          Expr.Ident(predMap[pred.Key]),

-                                          Expr.Not(pred.Value.Aggregate(Expr.Or))));

-          }

-        }

-      }

-    } else if (cmd is ReturnCmd) {

-      // Blocks which end in a return will never share a predicate with a block

-      // which appears after it.  Furthermore, such a block cannot be part of a

-      // loop.  So it is safe to do nothing here.

-    } else {

-      Console.WriteLine("Unsupported cmd: " + cmd.GetType().ToString());

-    }

-  }

-

-  Variable FreshPredicate(ref int predCount) {

-    var pVar = new LocalVariable(Token.NoToken,

-                                 new TypedIdent(Token.NoToken,

-                                                "p" + predCount++,

-                                                Microsoft.Boogie.Type.Bool));

-    impl.LocVars.Add(pVar);

-    return pVar;

-  }

-

-  void AssignPredicates(Graph<Block> blockGraph,

-                        DomRelation<Block> dom,

-                        DomRelation<Block> pdom,

-                        IEnumerator<Tuple<Block, bool>> i,

-                        Variable headPredicate,

-                        ref int predCount) {

-    var header = i.Current.Item1;

-    var regionPreds = new List<Tuple<Block, Variable>>();

-    var ownedPreds = new HashSet<Variable>();

-    ownedMap[header] = ownedPreds;

-

-    predMap[header] = headPredicate;

-    defMap[header] = headPredicate;

-    regionPreds.Add(new Tuple<Block, Variable>(header, headPredicate));

-

-    while (i.MoveNext()) {

-      var block = i.Current;

-      if (block.Item2) {

-        if (block.Item1 == header)

-          return;

-      } else {

-        if (blockGraph.Headers.Contains(block.Item1)) {

-          parentMap[block.Item1] = header;

-          var loopPred = FreshPredicate(ref predCount);

-          ownedPreds.Add(loopPred);

-          AssignPredicates(blockGraph, dom, pdom, i, loopPred, ref predCount);

-        } else {

-          bool foundExisting = false;

-          foreach (var regionPred in regionPreds) {

-            if (dom.DominatedBy(block.Item1, regionPred.Item1) &&

-                pdom.DominatedBy(regionPred.Item1, block.Item1)) {

-              predMap[block.Item1] = regionPred.Item2;

-              foundExisting = true;

-              break;

-            }

-          }

-          if (!foundExisting) {

-            var condPred = FreshPredicate(ref predCount);

-            predMap[block.Item1] = condPred;

-            defMap[block.Item1] = condPred;

-            ownedPreds.Add(condPred);

-            regionPreds.Add(new Tuple<Block, Variable>(block.Item1, condPred));

-          }

-        }

-      }

-    }

-  }

-

-  void AssignPredicates() {

-    DomRelation<Block> dom = blockGraph.DominatorMap;

-

-    Graph<Block> dualGraph = blockGraph.Dual(new Block());

-    DomRelation<Block> pdom = dualGraph.DominatorMap;

-

-    var iter = sortedBlocks.GetEnumerator();

-    if (!iter.MoveNext()) {

-      predMap = defMap = null;

-      ownedMap = null;

-      return;

-    }

-

-    int predCount = 0;

-    predMap = new Dictionary<Block, Variable>();

-    defMap = new Dictionary<Block, Variable>();

-    ownedMap = new Dictionary<Block, HashSet<Variable>>();

-    parentMap = new Dictionary<Block, Block>();

-    AssignPredicates(blockGraph, dom, pdom, iter,

-                     useProcedurePredicates ? impl.InParams[0] : null,

-                     ref predCount);

-  }

-

-  IEnumerable<Block> LoopsExited(Block src, Block dest) {

-    var i = sortedBlocks.GetEnumerator();

-    while (i.MoveNext()) {

-      var b = i.Current;

-      if (b.Item1 == src) {

-        return LoopsExitedForwardEdge(dest, i);

-      } else if (b.Item1 == dest) {

-        return LoopsExitedBackEdge(src, i);

-      }

-    }

-    Debug.Assert(false);

-    return null;

-  }

-

-  private IEnumerable<Block> LoopsExitedBackEdge(Block src, IEnumerator<Tuple<Block, bool>> i) {

-    var headsSeen = new HashSet<Block>();

-    while (i.MoveNext()) {

-      var b = i.Current;

-      if (!b.Item2 && blockGraph.Headers.Contains(b.Item1))

-        headsSeen.Add(b.Item1);

-      else if (b.Item2)

-        headsSeen.Remove(b.Item1);

-      if (b.Item1 == src)

-        return headsSeen;

-    }

-    Debug.Assert(false);

-    return null;

-  }

-

-  private IEnumerable<Block> LoopsExitedForwardEdge(Block dest, IEnumerator<Tuple<Block, bool>> i) {

-    var headsSeen = new HashSet<Block>();

-    while (i.MoveNext()) {

-      var b = i.Current;

-      if (b.Item1 == dest)

-        yield break;

-      else if (!b.Item2 && blockGraph.Headers.Contains(b.Item1))

-        headsSeen.Add(b.Item1);

-      else if (b.Item2 && !headsSeen.Contains(b.Item1))

-        yield return b.Item1;

-    }

-    Debug.Assert(false);

-  }

-

-  class PartInfo {

-    public PartInfo(Expr p, Block r) { pred = p; realDest = r; }

-    public Expr pred;

-    public Block realDest;

-  }

-

-  Dictionary<Block, PartInfo> BuildPartitionInfo() {

-    var partInfo = new Dictionary<Block, PartInfo>();

-    foreach (var block in blockGraph.Nodes) {

-      var parts = block.Cmds.Cast<Cmd>().TakeWhile(

-          c => c is AssumeCmd &&

-          QKeyValue.FindBoolAttribute(((AssumeCmd)c).Attributes, "partition"));

-

-      Expr pred = null;

-      if (parts.Count() > 0) {

-        pred = parts.Select(a => ((AssumeCmd)a).Expr).Aggregate(Expr.And);

-        block.Cmds =

-          new CmdSeq(block.Cmds.Cast<Cmd>().Skip(parts.Count()).ToArray());

-      } else {

-        continue;

-      }

-

-      Block realDest = block;

-      if (block.Cmds.Length == 0) {

-        var gc = block.TransferCmd as GotoCmd;

-        if (gc != null && gc.labelTargets.Length == 1)

-          realDest = gc.labelTargets[0];

-      }

-      partInfo[block] = new PartInfo(pred, realDest);

-    }

-

-    return partInfo;

-  }

-

-  void PredicateImplementation() {

-    blockGraph = prog.ProcessLoops(impl);

-    sortedBlocks = blockGraph.LoopyTopSort();

-

-    AssignPredicates();

-    partInfo = BuildPartitionInfo();

-

-    if (useProcedurePredicates)

-      fp = Expr.Ident(impl.InParams[0]);

-

-    var newBlocks = new List<Block>();

-    Block prevBlock = null;

-    foreach (var n in sortedBlocks) {

-      var p = predMap[n.Item1];

-      var pExpr = Expr.Ident(p);

-

-      if (n.Item2) {

-        var backedgeBlock = new Block();

-        newBlocks.Add(backedgeBlock);

-

-        backedgeBlock.Label = n.Item1.Label + ".backedge";

-        backedgeBlock.Cmds = new CmdSeq(new AssumeCmd(Token.NoToken, pExpr,

-          new QKeyValue(Token.NoToken, "backedge", new List<object>(), null)));

-        backedgeBlock.TransferCmd = new GotoCmd(Token.NoToken,

-                                                new BlockSeq(n.Item1));

-

-        var tailBlock = new Block();

-        newBlocks.Add(tailBlock);

-

-        tailBlock.Label = n.Item1.Label + ".tail";

-        tailBlock.Cmds = new CmdSeq(new AssumeCmd(Token.NoToken,

-                                             Expr.Not(pExpr)));

-

-        if (prevBlock != null)

-          prevBlock.TransferCmd = new GotoCmd(Token.NoToken,

-                                        new BlockSeq(backedgeBlock, tailBlock));

-        prevBlock = tailBlock;

-      } else {

-        var runBlock = n.Item1;

-        var oldCmdSeq = runBlock.Cmds;

-        runBlock.Cmds = new CmdSeq();

-        newBlocks.Add(runBlock);

-        if (prevBlock != null)

-          prevBlock.TransferCmd = new GotoCmd(Token.NoToken,

-                                              new BlockSeq(runBlock));

-

-        if (parentMap.ContainsKey(runBlock)) {

-          var parent = parentMap[runBlock];

-          if (predMap.ContainsKey(parent)) {

-            var parentPred = predMap[parent];

-            if (parentPred != null) {

-              runBlock.Cmds.Add(new AssertCmd(Token.NoToken,

-                                              Expr.Imp(pExpr, Expr.Ident(parentPred))));

-            }

-          }

-        }

-

-        var transferCmd = runBlock.TransferCmd;

-        foreach (Cmd cmd in oldCmdSeq)

-          PredicateCmd(pExpr, newBlocks, runBlock, cmd, out runBlock);

-

-        if (ownedMap.ContainsKey(n.Item1)) {

-          var owned = ownedMap[n.Item1];

-          foreach (var v in owned)

-            runBlock.Cmds.Add(Cmd.SimpleAssign(Token.NoToken, Expr.Ident(v), Expr.False));

-        }

-

-        PredicateTransferCmd(pExpr, runBlock, runBlock.Cmds, transferCmd);

-

-        prevBlock = runBlock;

-        doneBlocks.Add(runBlock);

-      }

-    }

-

-    prevBlock.TransferCmd = new ReturnCmd(Token.NoToken);

-    impl.Blocks = newBlocks;

-  }

-

-  private Expr CreateIfFPThenElse(Expr then, Expr eElse) {

-    if (useProcedurePredicates) {

-      return new NAryExpr(Token.NoToken,

-                 new IfThenElse(Token.NoToken),

-                 new ExprSeq(fp, then, eElse));

-    } else {

-      return then;

-    }

-  }

-

-  public static void Predicate(Program p,

-                               bool useProcedurePredicates = true) {

-    foreach (var decl in p.TopLevelDeclarations.ToList()) {

-      if (useProcedurePredicates && decl is DeclWithFormals && !(decl is Function)) {

-        var dwf = (DeclWithFormals)decl;

-        var fpVar = new Formal(Token.NoToken,

-                               new TypedIdent(Token.NoToken, "_P",

-                                              Microsoft.Boogie.Type.Bool),

-                               /*incoming=*/true);

-        dwf.InParams = new VariableSeq(

-          (new Variable[] {fpVar}.Concat(dwf.InParams.Cast<Variable>()))

-            .ToArray());

-

-        if (dwf is Procedure)

-        {

-            var proc = (Procedure)dwf;

-            var newRequires = new RequiresSeq();

-            foreach (Requires r in proc.Requires)

-            {

-                newRequires.Add(new Requires(r.Free,

-                    new EnabledReplacementVisitor(new IdentifierExpr(Token.NoToken, fpVar)).VisitExpr(r.Condition)));

-            }

-            var newEnsures = new EnsuresSeq();

-            foreach (Ensures e in proc.Ensures)

-            {

-                newEnsures.Add(new Ensures(e.Free,

-                    new EnabledReplacementVisitor(new IdentifierExpr(Token.NoToken, fpVar)).VisitExpr(e.Condition)));

-            }

-        }

-

-      }

-

-      try {

-        var impl = decl as Implementation;

-        if (impl != null)

-          new SmartBlockPredicator(p, impl, useProcedurePredicates).PredicateImplementation();

-      }

-      catch (Program.IrreducibleLoopException) { }

-    }

-  }

-

-  public static void Predicate(Program p, Implementation impl) {

-    try {

-      new SmartBlockPredicator(p, impl, false).PredicateImplementation();

-    }

-    catch (Program.IrreducibleLoopException) { }

-  }

-

-}

-

-}

+using Graphing;
+using System;
+using System.Collections.Generic;
+using System.Diagnostics;
+using System.Diagnostics.Contracts;
+using System.Linq;
+
+namespace Microsoft.Boogie {
+
+public class SmartBlockPredicator {
+
+  Program prog;
+  Implementation impl;
+  Graph<Block> blockGraph;
+  List<Tuple<Block, bool>> sortedBlocks;
+
+  Func<Procedure, bool> useProcedurePredicates;
+
+  Dictionary<Block, Variable> predMap, defMap;
+  Dictionary<Block, HashSet<Variable>> ownedMap;
+  Dictionary<Block, Block> parentMap;
+  Dictionary<Block, PartInfo> partInfo;
+
+  IdentifierExpr fp;
+  Dictionary<Microsoft.Boogie.Type, IdentifierExpr> havocVars =
+    new Dictionary<Microsoft.Boogie.Type, IdentifierExpr>();
+  Dictionary<Block, Expr> blockIds = new Dictionary<Block, Expr>();
+  HashSet<Block> doneBlocks = new HashSet<Block>();
+  bool myUseProcedurePredicates;
+  UniformityAnalyser uni;
+
+  SmartBlockPredicator(Program p, Implementation i, Func<Procedure, bool> upp, UniformityAnalyser u) {
+    prog = p;
+    impl = i;
+    useProcedurePredicates = upp;
+    myUseProcedurePredicates = useProcedurePredicates(i.Proc);
+    uni = u;
+  }
+
+  void PredicateCmd(Expr p, List<Block> blocks, Block block, Cmd cmd, out Block nextBlock) {
+    var cCmd = cmd as CallCmd;
+    if (cCmd != null && !useProcedurePredicates(cCmd.Proc)) {
+      if (p == null) {
+        block.Cmds.Add(cmd);
+        nextBlock = block;
+        return;
+      }
+
+      var trueBlock = new Block();
+      blocks.Add(trueBlock);
+      trueBlock.Label = block.Label + ".call.true";
+      trueBlock.Cmds.Add(new AssumeCmd(Token.NoToken, p));
+      trueBlock.Cmds.Add(cmd);
+
+      var falseBlock = new Block();
+      blocks.Add(falseBlock);
+      falseBlock.Label = block.Label + ".call.false";
+      falseBlock.Cmds.Add(new AssumeCmd(Token.NoToken, Expr.Not(p)));
+
+      var contBlock = new Block();
+      blocks.Add(contBlock);
+      contBlock.Label = block.Label + ".call.cont";
+
+      block.TransferCmd =
+        new GotoCmd(Token.NoToken, new BlockSeq(trueBlock, falseBlock));
+      trueBlock.TransferCmd = falseBlock.TransferCmd =
+        new GotoCmd(Token.NoToken, new BlockSeq(contBlock));
+      nextBlock = contBlock;
+    } else {
+      PredicateCmd(p, block.Cmds, cmd);
+      nextBlock = block;
+    }
+  }
+
+  void PredicateCmd(Expr p, CmdSeq cmdSeq, Cmd cmd) {
+    if (cmd is CallCmd) {
+      var cCmd = (CallCmd)cmd;
+      Debug.Assert(useProcedurePredicates(cCmd.Proc));
+      cCmd.Ins.Insert(0, p != null ? p : Expr.True);
+      cmdSeq.Add(cCmd);
+    } else if (p == null) {
+      cmdSeq.Add(cmd);
+    } else if (cmd is AssignCmd) {
+      var aCmd = (AssignCmd)cmd;
+      cmdSeq.Add(new AssignCmd(Token.NoToken, aCmd.Lhss,
+                   new List<Expr>(aCmd.Lhss.Zip(aCmd.Rhss, (lhs, rhs) =>
+                     new NAryExpr(Token.NoToken,
+                       new IfThenElse(Token.NoToken),
+                       new ExprSeq(p, rhs, lhs.AsExpr))))));
+    } else if (cmd is AssertCmd) {
+      var aCmd = (AssertCmd)cmd;
+      Expr newExpr = new EnabledReplacementVisitor(p).VisitExpr(aCmd.Expr);
+      aCmd.Expr = QKeyValue.FindBoolAttribute(aCmd.Attributes, "do_not_predicate") ? newExpr : Expr.Imp(p, newExpr);
+      cmdSeq.Add(aCmd);
+    } else if (cmd is AssumeCmd) {
+      var aCmd = (AssumeCmd)cmd;
+      cmdSeq.Add(new AssumeCmd(Token.NoToken, Expr.Imp(p, aCmd.Expr)));
+    } else if (cmd is HavocCmd) {
+      var hCmd = (HavocCmd)cmd;
+      foreach (IdentifierExpr v in hCmd.Vars) {
+        Microsoft.Boogie.Type type = v.Decl.TypedIdent.Type;
+        Contract.Assert(type != null);
+
+        IdentifierExpr havocTempExpr;
+        if (havocVars.ContainsKey(type)) {
+          havocTempExpr = havocVars[type];
+        } else {
+          var havocVar = new LocalVariable(Token.NoToken,
+                             new TypedIdent(Token.NoToken,
+                                            "_HAVOC_" + type.ToString(), type));
+          impl.LocVars.Add(havocVar);
+          havocVars[type] = havocTempExpr =
+            new IdentifierExpr(Token.NoToken, havocVar);
+        }
+        cmdSeq.Add(new HavocCmd(Token.NoToken,
+                                new IdentifierExprSeq(havocTempExpr)));
+        cmdSeq.Add(Cmd.SimpleAssign(Token.NoToken, v,
+                                    new NAryExpr(Token.NoToken,
+                                      new IfThenElse(Token.NoToken),
+                                      new ExprSeq(p, havocTempExpr, v))));
+      }
+    } else if (cmd is CommentCmd) {
+      // skip
+    } else if (cmd is StateCmd) {
+      var sCmd = (StateCmd)cmd;
+      var newCmdSeq = new CmdSeq();
+      foreach (Cmd c in sCmd.Cmds)
+        PredicateCmd(p, newCmdSeq, c);
+      sCmd.Cmds = newCmdSeq;
+      cmdSeq.Add(sCmd);
+    } else {
+      Console.WriteLine("Unsupported cmd: " + cmd.GetType().ToString());
+    }
+  }
+
+  // hasPredicatedRegion is true iff the block or its targets are predicated
+  // (i.e. we enter, stay within or exit a predicated region).
+  void PredicateTransferCmd(Expr p, Block src, CmdSeq cmdSeq, TransferCmd cmd, out bool hasPredicatedRegion) {
+    hasPredicatedRegion = predMap.ContainsKey(src);
+
+    if (cmd is GotoCmd) {
+      var gCmd = (GotoCmd)cmd;
+
+      hasPredicatedRegion = hasPredicatedRegion ||
+        gCmd.labelTargets.Cast<Block>().Any(b => predMap.ContainsKey(b));
+
+      if (gCmd.labelTargets.Length == 1) {
+        if (defMap.ContainsKey(gCmd.labelTargets[0]))
+          PredicateCmd(p, cmdSeq,
+                       Cmd.SimpleAssign(Token.NoToken,
+                                        Expr.Ident(predMap[gCmd.labelTargets[0]]), Expr.True));
+      } else {
+        Debug.Assert(gCmd.labelTargets.Length > 1);
+        Debug.Assert(gCmd.labelTargets.Cast<Block>().All(t => uni.IsUniform(impl.Name, t) ||
+                                                              partInfo.ContainsKey(t)));
+        foreach (Block target in gCmd.labelTargets) {
+          if (!partInfo.ContainsKey(target))
+            continue;
+
+          var part = partInfo[target];
+          if (defMap.ContainsKey(part.realDest))
+            PredicateCmd(p, cmdSeq,
+                         Cmd.SimpleAssign(Token.NoToken,
+                                          Expr.Ident(predMap[part.realDest]), part.pred));
+          var predsExitingLoop = new Dictionary<Block, List<Expr>>();
+          foreach (Block exit in LoopsExited(src, target)) {
+            List<Expr> predList;
+            if (!predsExitingLoop.ContainsKey(exit))
+              predList = predsExitingLoop[exit] = new List<Expr>();
+            else
+              predList = predsExitingLoop[exit];
+            predList.Add(part.pred);
+          }
+          foreach (var pred in predsExitingLoop) {
+            PredicateCmd(p, cmdSeq,
+                         Cmd.SimpleAssign(Token.NoToken,
+                                          Expr.Ident(predMap[pred.Key]),
+                                          Expr.Not(pred.Value.Aggregate(Expr.Or))));
+          }
+        }
+      }
+    } else if (cmd is ReturnCmd) {
+      // Blocks which end in a return will never share a predicate with a block
+      // which appears after it.  Furthermore, such a block cannot be part of a
+      // loop.  So it is safe to do nothing here.
+    } else {
+      Console.WriteLine("Unsupported cmd: " + cmd.GetType().ToString());
+    }
+  }
+
+  Variable FreshPredicate(ref int predCount) {
+    var pVar = new LocalVariable(Token.NoToken,
+                                 new TypedIdent(Token.NoToken,
+                                                "p" + predCount++,
+                                                Microsoft.Boogie.Type.Bool));
+    impl.LocVars.Add(pVar);
+    return pVar;
+  }
+
+  void AssignPredicates(Graph<Block> blockGraph,
+                        DomRelation<Block> dom,
+                        DomRelation<Block> pdom,
+                        IEnumerator<Tuple<Block, bool>> i,
+                        Variable headPredicate,
+                        ref int predCount) {
+    var header = i.Current.Item1;
+    var regionPreds = new List<Tuple<Block, Variable>>();
+    var ownedPreds = new HashSet<Variable>();
+    ownedMap[header] = ownedPreds;
+
+    if (headPredicate != null) {
+      predMap[header] = headPredicate;
+      defMap[header] = headPredicate;
+      regionPreds.Add(new Tuple<Block, Variable>(header, headPredicate));
+    }
+
+    while (i.MoveNext()) {
+      var block = i.Current;
+      if (uni != null && uni.IsUniform(impl.Name, block.Item1))
+        continue;
+      if (block.Item2) {
+        if (block.Item1 == header)
+          return;
+      } else {
+        if (blockGraph.Headers.Contains(block.Item1)) {
+          parentMap[block.Item1] = header;
+          var loopPred = FreshPredicate(ref predCount);
+          ownedPreds.Add(loopPred);
+          AssignPredicates(blockGraph, dom, pdom, i, loopPred, ref predCount);
+        } else {
+          bool foundExisting = false;
+          foreach (var regionPred in regionPreds) {
+            if (dom.DominatedBy(block.Item1, regionPred.Item1) &&
+                pdom.DominatedBy(regionPred.Item1, block.Item1)) {
+              predMap[block.Item1] = regionPred.Item2;
+              foundExisting = true;
+              break;
+            }
+          }
+          if (!foundExisting) {
+            var condPred = FreshPredicate(ref predCount);
+            predMap[block.Item1] = condPred;
+            defMap[block.Item1] = condPred;
+            ownedPreds.Add(condPred);
+            regionPreds.Add(new Tuple<Block, Variable>(block.Item1, condPred));
+          }
+        }
+      }
+    }
+  }
+
+  void AssignPredicates() {
+    DomRelation<Block> dom = blockGraph.DominatorMap;
+
+    Graph<Block> dualGraph = blockGraph.Dual(new Block());
+    DomRelation<Block> pdom = dualGraph.DominatorMap;
+
+    var iter = sortedBlocks.GetEnumerator();
+    if (!iter.MoveNext()) {
+      predMap = defMap = null;
+      ownedMap = null;
+      return;
+    }
+
+    int predCount = 0;
+    predMap = new Dictionary<Block, Variable>();
+    defMap = new Dictionary<Block, Variable>();
+    ownedMap = new Dictionary<Block, HashSet<Variable>>();
+    parentMap = new Dictionary<Block, Block>();
+    AssignPredicates(blockGraph, dom, pdom, iter,
+                     myUseProcedurePredicates ? impl.InParams[0] : null,
+                     ref predCount);
+  }
+
+  IEnumerable<Block> LoopsExited(Block src, Block dest) {
+    var i = sortedBlocks.GetEnumerator();
+    while (i.MoveNext()) {
+      var b = i.Current;
+      if (b.Item1 == src) {
+        return LoopsExitedForwardEdge(dest, i);
+      } else if (b.Item1 == dest) {
+        return LoopsExitedBackEdge(src, i);
+      }
+    }
+    Debug.Assert(false);
+    return null;
+  }
+
+  private IEnumerable<Block> LoopsExitedBackEdge(Block src, IEnumerator<Tuple<Block, bool>> i) {
+    var headsSeen = new HashSet<Block>();
+    while (i.MoveNext()) {
+      var b = i.Current;
+      if (!b.Item2 && blockGraph.Headers.Contains(b.Item1))
+        headsSeen.Add(b.Item1);
+      else if (b.Item2)
+        headsSeen.Remove(b.Item1);
+      if (b.Item1 == src)
+        return headsSeen;
+    }
+    Debug.Assert(false);
+    return null;
+  }
+
+  private IEnumerable<Block> LoopsExitedForwardEdge(Block dest, IEnumerator<Tuple<Block, bool>> i) {
+    var headsSeen = new HashSet<Block>();
+    while (i.MoveNext()) {
+      var b = i.Current;
+      if (b.Item1 == dest)
+        yield break;
+      else if (!b.Item2 && blockGraph.Headers.Contains(b.Item1))
+        headsSeen.Add(b.Item1);
+      else if (b.Item2 && !headsSeen.Contains(b.Item1))
+        yield return b.Item1;
+    }
+    Debug.Assert(false);
+  }
+
+  class PartInfo {
+    public PartInfo(Expr p, Block r) { pred = p; realDest = r; }
+    public Expr pred;
+    public Block realDest;
+  }
+
+  Dictionary<Block, PartInfo> BuildPartitionInfo() {
+    var partInfo = new Dictionary<Block, PartInfo>();
+    foreach (var block in blockGraph.Nodes) {
+      if (uni.IsUniform(impl.Name, block))
+        continue;
+
+      var parts = block.Cmds.Cast<Cmd>().TakeWhile(
+          c => c is AssumeCmd &&
+          QKeyValue.FindBoolAttribute(((AssumeCmd)c).Attributes, "partition"));
+
+      Expr pred = null;
+      if (parts.Count() > 0) {
+        pred = parts.Select(a => ((AssumeCmd)a).Expr).Aggregate(Expr.And);
+        block.Cmds =
+          new CmdSeq(block.Cmds.Cast<Cmd>().Skip(parts.Count()).ToArray());
+      } else {
+        continue;
+      }
+
+      Block realDest = block;
+      if (block.Cmds.Length == 0) {
+        var gc = block.TransferCmd as GotoCmd;
+        if (gc != null && gc.labelTargets.Length == 1)
+          realDest = gc.labelTargets[0];
+      }
+      partInfo[block] = new PartInfo(pred, realDest);
+    }
+
+    return partInfo;
+  }
+
+  void PredicateImplementation() {
+    blockGraph = prog.ProcessLoops(impl);
+    sortedBlocks = blockGraph.LoopyTopSort();
+
+    AssignPredicates();
+    partInfo = BuildPartitionInfo();
+
+    if (myUseProcedurePredicates)
+      fp = Expr.Ident(impl.InParams[0]);
+
+    var newBlocks = new List<Block>();
+    Block prevBlock = null;
+    foreach (var n in sortedBlocks) {
+      if (predMap.ContainsKey(n.Item1)) {
+        var p = predMap[n.Item1];
+        var pExpr = Expr.Ident(p);
+
+        if (n.Item2) {
+          var backedgeBlock = new Block();
+          newBlocks.Add(backedgeBlock);
+
+          backedgeBlock.Label = n.Item1.Label + ".backedge";
+          backedgeBlock.Cmds = new CmdSeq(new AssumeCmd(Token.NoToken, pExpr,
+            new QKeyValue(Token.NoToken, "backedge", new List<object>(), null)));
+          backedgeBlock.TransferCmd = new GotoCmd(Token.NoToken,
+                                                  new BlockSeq(n.Item1));
+
+          var tailBlock = new Block();
+          newBlocks.Add(tailBlock);
+
+          tailBlock.Label = n.Item1.Label + ".tail";
+          tailBlock.Cmds = new CmdSeq(new AssumeCmd(Token.NoToken,
+                                               Expr.Not(pExpr)));
+
+          if (prevBlock != null)
+            prevBlock.TransferCmd = new GotoCmd(Token.NoToken,
+                                          new BlockSeq(backedgeBlock, tailBlock));
+          prevBlock = tailBlock;
+        } else {
+          PredicateBlock(pExpr, n.Item1, newBlocks, ref prevBlock);
+        }
+      } else {
+        if (!n.Item2) {
+          PredicateBlock(null, n.Item1, newBlocks, ref prevBlock);
+        }
+      }
+    }
+
+    if (prevBlock != null)
+      prevBlock.TransferCmd = new ReturnCmd(Token.NoToken);
+
+    impl.Blocks = newBlocks;
+  }
+
+  private void PredicateBlock(Expr pExpr, Block block, List<Block> newBlocks, ref Block prevBlock) {
+    var firstBlock = block;
+
+    var oldCmdSeq = block.Cmds;
+    block.Cmds = new CmdSeq();
+    newBlocks.Add(block);
+    if (prevBlock != null) {
+      prevBlock.TransferCmd = new GotoCmd(Token.NoToken, new BlockSeq(block));
+    }
+
+    if (parentMap.ContainsKey(block)) {
+      var parent = parentMap[block];
+      if (predMap.ContainsKey(parent)) {
+        var parentPred = predMap[parent];
+        if (parentPred != null) {
+          block.Cmds.Add(new AssertCmd(Token.NoToken,
+                                          pExpr != null ? (Expr)Expr.Imp(pExpr, Expr.Ident(parentPred))
+                                                        : Expr.Ident(parentPred)));
+        }
+      }
+    }
+
+    var transferCmd = block.TransferCmd;
+    foreach (Cmd cmd in oldCmdSeq)
+      PredicateCmd(pExpr, newBlocks, block, cmd, out block);
+
+    if (ownedMap.ContainsKey(firstBlock)) {
+      var owned = ownedMap[firstBlock];
+      foreach (var v in owned)
+        block.Cmds.Add(Cmd.SimpleAssign(Token.NoToken, Expr.Ident(v), Expr.False));
+    }
+
+    bool hasPredicatedRegion;
+    PredicateTransferCmd(pExpr, block, block.Cmds, transferCmd, out hasPredicatedRegion);
+
+    if (hasPredicatedRegion)
+      prevBlock = block;
+    else
+      prevBlock = null;
+
+    doneBlocks.Add(block);
+  }
+
+  private Expr CreateIfFPThenElse(Expr then, Expr eElse) {
+    if (myUseProcedurePredicates) {
+      return new NAryExpr(Token.NoToken,
+                 new IfThenElse(Token.NoToken),
+                 new ExprSeq(fp, then, eElse));
+    } else {
+      return then;
+    }
+  }
+
+  public static void Predicate(Program p,
+                               Func<Procedure, bool> useProcedurePredicates = null,
+                               UniformityAnalyser uni = null) {
+    useProcedurePredicates = useProcedurePredicates ?? (proc => false);
+    if (uni != null) {
+      var oldUPP = useProcedurePredicates;
+      useProcedurePredicates = proc => oldUPP(proc) && !uni.IsUniform(proc.Name);
+    }
+
+    foreach (var decl in p.TopLevelDeclarations.ToList()) {
+      if (decl is Procedure || decl is Implementation) {
+        var proc = decl as Procedure;
+        Implementation impl = null;
+        if (proc == null) {
+          impl = (Implementation)decl;
+          proc = impl.Proc;
+        }
+
+        bool upp = useProcedurePredicates(proc);
+        if (upp) {
+          var dwf = (DeclWithFormals)decl;
+          var fpVar = new Formal(Token.NoToken,
+                                 new TypedIdent(Token.NoToken, "_P",
+                                                Microsoft.Boogie.Type.Bool),
+                                 /*incoming=*/true);
+          dwf.InParams = new VariableSeq(
+            (new Variable[] {fpVar}.Concat(dwf.InParams.Cast<Variable>()))
+              .ToArray());
+
+          if (impl == null) {
+            var newRequires = new RequiresSeq();
+            foreach (Requires r in proc.Requires) {
+              newRequires.Add(new Requires(r.Free,
+                new EnabledReplacementVisitor(new IdentifierExpr(Token.NoToken, fpVar)).VisitExpr(r.Condition)));
+            }
+            var newEnsures = new EnsuresSeq();
+            foreach (Ensures e in proc.Ensures) {
+              newEnsures.Add(new Ensures(e.Free,
+                new EnabledReplacementVisitor(new IdentifierExpr(Token.NoToken, fpVar)).VisitExpr(e.Condition)));
+            }
+          }
+        }
+
+        if (impl != null) {
+          try {
+            new SmartBlockPredicator(p, impl, useProcedurePredicates, uni).PredicateImplementation();
+          } catch (Program.IrreducibleLoopException) { }
+        }
+      }
+    }
+  }
+
+  public static void Predicate(Program p, Implementation impl) {
+    try {
+      new SmartBlockPredicator(p, impl, proc => false, null).PredicateImplementation();
+    }
+    catch (Program.IrreducibleLoopException) { }
+  }
+
+}
+
+}
diff --git a/Source/VCGeneration/UniformityAnalyser.cs b/Source/VCGeneration/UniformityAnalyser.cs
new file mode 100644
index 00000000..e5647a21
--- /dev/null
+++ b/Source/VCGeneration/UniformityAnalyser.cs
@@ -0,0 +1,539 @@
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.Boogie;
+using System.Diagnostics;
+using Graphing;
+
+namespace Microsoft.Boogie
+{
+
+    public class UniformityAnalyser
+    {
+        private Program prog;
+
+        private bool doAnalysis, unstructured;
+
+        private ISet<Implementation> entryPoints;
+
+        private IEnumerable<Variable> nonUniformVars;
+
+        private bool ProcedureChanged;
+
+        private Dictionary<string, KeyValuePair<bool, Dictionary<string, bool>>> uniformityInfo;
+
+        private Dictionary<string, HashSet<int>> nonUniformLoops;
+
+        private Dictionary<string, HashSet<Block>> nonUniformBlocks;
+
+        private Dictionary<string, HashSet<int>> loopsWithNonuniformReturn;
+
+        private Dictionary<string, List<string>> inParameters;
+
+        private Dictionary<string, List<string>> outParameters;
+
+        private List<WhileCmd> loopStack;
+
+        private bool hitNonuniformReturn;
+
+        public UniformityAnalyser(Program prog, bool doAnalysis, bool unstructured, ISet<Implementation> entryPoints, IEnumerable<Variable> nonUniformVars)
+        {
+            this.prog = prog;
+            this.doAnalysis = doAnalysis;
+            this.unstructured = unstructured;
+            this.entryPoints = entryPoints;
+            this.nonUniformVars = nonUniformVars;
+            uniformityInfo = new Dictionary<string, KeyValuePair<bool, Dictionary<string, bool>>>();
+            nonUniformLoops = new Dictionary<string, HashSet<int>>();
+            nonUniformBlocks = new Dictionary<string, HashSet<Block>>();
+            loopsWithNonuniformReturn = new Dictionary<string, HashSet<int>>();
+            inParameters = new Dictionary<string, List<string>>();
+            outParameters = new Dictionary<string, List<string>>();
+            loopStack = new List<WhileCmd>();
+        }
+
+        public void Analyse()
+        {
+            var impls = prog.TopLevelDeclarations.OfType<Implementation>();
+
+            foreach (var Impl in impls)
+            {
+                bool uniformProcedure = doAnalysis || entryPoints.Contains(Impl);
+
+                uniformityInfo.Add(Impl.Name, new KeyValuePair<bool, Dictionary<string, bool>>
+                    (uniformProcedure, new Dictionary<string, bool> ()));
+
+                nonUniformLoops.Add(Impl.Name, new HashSet<int>());
+                loopsWithNonuniformReturn.Add(Impl.Name, new HashSet<int>());
+
+                foreach (var v in nonUniformVars)
+                    SetNonUniform(Impl.Name, v.Name);
+
+                foreach (Variable v in Impl.LocVars)
+                {
+                    if (doAnalysis)
+                    {
+                        SetUniform(Impl.Name, v.Name);
+                    }
+                    else
+                    {
+                        SetNonUniform(Impl.Name, v.Name);
+                    }
+                }
+
+                inParameters[Impl.Name] = new List<string>();
+
+                foreach (Variable v in Impl.InParams)
+                {
+                    inParameters[Impl.Name].Add(v.Name);
+                    if (doAnalysis)
+                    {
+                        SetUniform(Impl.Name, v.Name);
+                    }
+                    else
+                    {
+                        SetNonUniform(Impl.Name, v.Name);
+                    }
+                }
+
+                outParameters[Impl.Name] = new List<string>();
+                foreach (Variable v in Impl.OutParams)
+                {
+                    outParameters[Impl.Name].Add(v.Name);
+                    if (doAnalysis)
+                    {
+                        SetUniform(Impl.Name, v.Name);
+                    }
+                    else
+                    {
+                        SetNonUniform(Impl.Name, v.Name);
+                    }
+                }
+
+                ProcedureChanged = true;
+            }
+
+            if (doAnalysis)
+            {
+                while (ProcedureChanged)
+                {

+                    ProcedureChanged = false;
+
+                    foreach (var Impl in impls)
+                    {
+                        hitNonuniformReturn = false;
+                        Analyse(Impl, uniformityInfo[Impl.Name].Key);
+                    }
+                }
+            }
+
+            foreach (var Impl in impls)
+            {
+                if (!IsUniform (Impl.Name))
+                {
+                    List<string> newIns = new List<String>();
+                    newIns.Add("_P");
+                    foreach (string s in inParameters[Impl.Name])
+                    {
+                        newIns.Add(s);
+                    }
+                    inParameters[Impl.Name] = newIns;
+                }
+            }
+        }
+
+        private void Analyse(Implementation Impl, bool ControlFlowIsUniform)
+        {
+            if (unstructured)
+            {

+                if (!ControlFlowIsUniform)
+                {
+                    nonUniformBlocks[Impl.Name] = new HashSet<Block>(Impl.Blocks);
+
+                    foreach (Variable v in Impl.LocVars) {
+                        if (IsUniform(Impl.Name, v.Name)) {
+                            SetNonUniform(Impl.Name, v.Name);
+                        }
+                    }

+

+                    foreach (Variable v in Impl.InParams) {

+                        if (IsUniform(Impl.Name, v.Name)) {

+                            SetNonUniform(Impl.Name, v.Name);

+                        }

+                    }

+

+                    foreach (Variable v in Impl.OutParams) {

+                      if (IsUniform(Impl.Name, v.Name)) {

+                         SetNonUniform(Impl.Name, v.Name);

+                      }

+                    }

+                        
+                    return;
+                }
+
+                Graph<Block> blockGraph = prog.ProcessLoops(Impl);
+                var ctrlDep = blockGraph.ControlDependence();
+
+                // Compute transitive closure of control dependence info.
+                bool changed;
+                do
+                {
+                    changed = false;
+                    foreach (var depEntry in ctrlDep)
+                    {
+                        var newDepSet = new HashSet<Block>(depEntry.Value);
+                        foreach (var dep in depEntry.Value)
+                        {
+                            if (ctrlDep.ContainsKey(dep))
+                                newDepSet.UnionWith(ctrlDep[dep]);
+                        }
+                        if (newDepSet.Count != depEntry.Value.Count)
+                        {
+                            depEntry.Value.UnionWith(newDepSet);
+                            changed = true;
+                        }
+                    }
+                } while (changed);
+
+                var nonUniformBlockSet = new HashSet<Block>();
+                nonUniformBlocks[Impl.Name] = nonUniformBlockSet;

+

+                do {

+                  changed = false;

+                  foreach (var block in Impl.Blocks) {

+                    bool uniform = !nonUniformBlockSet.Contains(block);

+                    bool newUniform = Analyse(Impl, block.Cmds, uniform);

+                    if (uniform && !newUniform) {

+                      changed = true;

+                      nonUniformBlockSet.Add(block);

+                      Block pred = blockGraph.Predecessors(block).Single();

+                      if (ctrlDep.ContainsKey(pred))

+                        nonUniformBlockSet.UnionWith(ctrlDep[pred]);

+                    }

+                  }

+                } while (changed);

+            }
+            else
+            {
+                Analyse(Impl, Impl.StructuredStmts, ControlFlowIsUniform);
+            }
+        }
+
+
+        private void Analyse(Implementation impl, StmtList stmtList, bool ControlFlowIsUniform)
+        {
+            ControlFlowIsUniform &= !hitNonuniformReturn;
+            foreach (BigBlock bb in stmtList.BigBlocks)
+            {
+                Analyse(impl, bb, ControlFlowIsUniform);
+            }
+        }
+
+        private Implementation GetImplementation(string procedureName)
+        {
+            foreach (Declaration D in prog.TopLevelDeclarations)
+            {
+                if (D is Implementation && ((D as Implementation).Name == procedureName))
+                {
+                    return D as Implementation;
+                }
+            }
+            return null;
+        }
+
+        private void Analyse(Implementation impl, BigBlock bb, bool ControlFlowIsUniform)
+        {
+            ControlFlowIsUniform &= !hitNonuniformReturn;
+            Analyse(impl, bb.simpleCmds, ControlFlowIsUniform);
+
+            if (bb.ec is WhileCmd)
+            {
+                WhileCmd wc = bb.ec as WhileCmd;
+                loopStack.Add(wc);
+                Analyse(impl, wc.Body, ControlFlowIsUniform && IsUniform(impl.Name, wc.Guard) && 
+                    !nonUniformLoops[impl.Name].Contains(GetLoopId(wc)));
+                loopStack.RemoveAt(loopStack.Count - 1);
+            }
+            else if (bb.ec is IfCmd)
+            {
+                IfCmd ifCmd = bb.ec as IfCmd;
+                Analyse(impl, ifCmd.thn, ControlFlowIsUniform && IsUniform(impl.Name, ifCmd.Guard));
+                if (ifCmd.elseBlock != null)
+                {
+                    Analyse(impl, ifCmd.elseBlock, ControlFlowIsUniform && IsUniform(impl.Name, ifCmd.Guard));
+                }
+                Debug.Assert(ifCmd.elseIf == null);
+            }
+            else if (bb.ec is BreakCmd)
+            {
+                if (!ControlFlowIsUniform && !nonUniformLoops[impl.Name].Contains(GetLoopId(loopStack[loopStack.Count - 1])))
+                {
+                    SetNonUniform(impl.Name, loopStack[loopStack.Count - 1]);
+                }
+            }
+
+            if (bb.tc is ReturnCmd && !ControlFlowIsUniform)
+            {
+                hitNonuniformReturn = true;
+                if (loopStack.Count > 0 && !nonUniformLoops[impl.Name].Contains(GetLoopId(loopStack[0])))
+                {
+                    SetNonUniform(impl.Name, loopStack[0]);
+                    loopsWithNonuniformReturn[impl.Name].Add(GetLoopId(loopStack[0]));
+                }
+            }
+
+
+        }
+
+        private bool Analyse(Implementation impl, CmdSeq cmdSeq, bool ControlFlowIsUniform)
+        {
+            foreach (Cmd c in cmdSeq)
+            {
+                if (c is AssignCmd)
+                {
+                    AssignCmd assignCmd = c as AssignCmd;
+                    foreach (var a in assignCmd.Lhss.Zip(assignCmd.Rhss))
+                    {

+
+                        if (a.Item1 is SimpleAssignLhs)
+                        {
+                            SimpleAssignLhs lhs = a.Item1 as SimpleAssignLhs;

+                            Expr rhs = a.Item2;

+                            if (IsUniform(impl.Name, lhs.AssignedVariable.Name) &&
+                                (!ControlFlowIsUniform || !IsUniform(impl.Name, rhs)))
+                            {

+                                SetNonUniform(impl.Name, lhs.AssignedVariable.Name);
+                            }

+

+                        }
+                    }
+                }
+                else if (c is CallCmd)
+                {
+                    CallCmd callCmd = c as CallCmd;
+                    Implementation CalleeImplementation = GetImplementation(callCmd.callee);
+
+                    if (CalleeImplementation != null)
+                    {
+
+                        if (!ControlFlowIsUniform)
+                        {
+                            if (IsUniform(callCmd.callee))
+                            {
+                                SetNonUniform(callCmd.callee);
+                            }
+                        }
+                        for (int i = 0; i < CalleeImplementation.InParams.Length; i++)
+                        {
+                            if (IsUniform(callCmd.callee, CalleeImplementation.InParams[i].Name)
+                                && !IsUniform(impl.Name, callCmd.Ins[i]))
+                            {
+                                SetNonUniform(callCmd.callee, CalleeImplementation.InParams[i].Name);
+                            }
+                        }
+
+                        for (int i = 0; i < CalleeImplementation.OutParams.Length; i++)
+                        {
+                            if (IsUniform(impl.Name, callCmd.Outs[i].Name)
+                                && !IsUniform(callCmd.callee, CalleeImplementation.OutParams[i].Name))
+                            {
+                                SetNonUniform(impl.Name, callCmd.Outs[i].Name);
+                            }
+                        }
+
+                    }
+                }
+                else if (c is AssumeCmd)
+                {
+                    var ac = (AssumeCmd)c;
+                    if (ControlFlowIsUniform && QKeyValue.FindBoolAttribute(ac.Attributes, "partition") &&
+                        !IsUniform(impl.Name, ac.Expr))
+                    {

+                      ControlFlowIsUniform = false;

+                    }
+                }
+            }
+
+            return ControlFlowIsUniform;
+        }
+
+        private int GetLoopId(WhileCmd wc)
+        {
+            AssertCmd inv = wc.Invariants[0] as AssertCmd;
+            Debug.Assert(inv.Attributes.Key.Contains("loophead_"));
+            return Convert.ToInt32(inv.Attributes.Key.Substring("loophead_".Length));
+        }
+
+        private void SetNonUniform(string procedureName)
+        {
+            uniformityInfo[procedureName] = new KeyValuePair<bool,Dictionary<string,bool>>
+                (false, uniformityInfo[procedureName].Value);
+            RecordProcedureChanged();
+        }
+
+        private void SetNonUniform(string procedureName, WhileCmd wc)
+        {
+            nonUniformLoops[procedureName].Add(GetLoopId(wc));
+            RecordProcedureChanged();
+        }
+
+        public bool IsUniform(string procedureName)
+        {
+            if (!uniformityInfo.ContainsKey(procedureName))
+            {
+                return false;
+            }
+            return uniformityInfo[procedureName].Key;
+        }
+
+        public bool IsUniform(string procedureName, Block b)
+        {
+            if (!nonUniformBlocks.ContainsKey(procedureName))
+            {
+                return false;
+            }
+            return !nonUniformBlocks[procedureName].Contains(b);
+        }
+
+        class UniformExpressionAnalysisVisitor : StandardVisitor {
+
+          private bool isUniform = true;
+          private Dictionary<string, bool> uniformityInfo;
+
+          public UniformExpressionAnalysisVisitor(Dictionary<string, bool> uniformityInfo) {
+            this.uniformityInfo = uniformityInfo;
+          }
+
+          public override Variable VisitVariable(Variable v) {
+            if (!uniformityInfo.ContainsKey(v.Name)) {
+              isUniform = isUniform && (v is Constant);
+            } else if (!uniformityInfo[v.Name]) {
+              isUniform = false;
+            }
+
+            return v;
+          }
+
+          internal bool IsUniform() {
+            return isUniform;
+          }
+        }
+
+        public bool IsUniform(string procedureName, Expr expr)
+        {
+            UniformExpressionAnalysisVisitor visitor = new UniformExpressionAnalysisVisitor(uniformityInfo[procedureName].Value);
+            visitor.VisitExpr(expr);
+            return visitor.IsUniform();
+        }
+
+        public bool IsUniform(string procedureName, string v)
+        {
+            if (!uniformityInfo.ContainsKey(procedureName))
+            {
+                return false;
+            }
+
+            if (!uniformityInfo[procedureName].Value.ContainsKey(v))
+            {
+                return false;
+            }
+            return uniformityInfo[procedureName].Value[v];
+        }
+
+        private void SetUniform(string procedureName, string v)
+        {
+            uniformityInfo[procedureName].Value[v] = true;
+            RecordProcedureChanged();
+        }
+
+        private void RecordProcedureChanged()
+        {
+            ProcedureChanged = true;
+        }
+
+        private void SetNonUniform(string procedureName, string v)
+        {
+            uniformityInfo[procedureName].Value[v] = false;
+            RecordProcedureChanged();
+        }
+
+        public void dump()
+        {
+            foreach (string p in uniformityInfo.Keys)
+            {
+                Console.WriteLine("Procedure " + p + ": "
+                    + (uniformityInfo[p].Key ? "uniform" : "nonuniform"));
+                foreach (string v in uniformityInfo[p].Value.Keys)
+                {
+                    Console.WriteLine("  " + v + ": " +
+                        (uniformityInfo[p].Value[v] ? "uniform" : "nonuniform"));
+                }
+                Console.Write("Ins [");
+                for (int i = 0; i < inParameters[p].Count; i++)
+                {
+                    Console.Write((i == 0 ? "" : ", ") + inParameters[p][i]);
+                }
+                Console.WriteLine("]");
+                Console.Write("Outs [");
+                for (int i = 0; i < outParameters[p].Count; i++)
+                {
+                    Console.Write((i == 0 ? "" : ", ") + outParameters[p][i]);
+                }
+                Console.WriteLine("]");
+                Console.Write("Non-uniform loops:");
+                foreach (int l in nonUniformLoops[p])
+                {
+                    Console.Write(" " + l);
+                }
+                Console.WriteLine();
+                Console.Write("Non-uniform blocks:");
+                foreach (Block b in nonUniformBlocks[p])
+                {
+                    Console.Write(" " + b.Label);
+                }
+                Console.WriteLine();
+            }
+        }
+
+
+        public string GetInParameter(string procName, int i)
+        {
+            return inParameters[procName][i];
+        }
+
+        public string GetOutParameter(string procName, int i)
+        {
+            return outParameters[procName][i];
+        }
+
+
+        public bool knowsOf(string p)
+        {
+            return uniformityInfo.ContainsKey(p);
+        }
+
+        public void AddNonUniform(string proc, string v)
+        {
+            if (uniformityInfo.ContainsKey(proc))
+            {
+                Debug.Assert(!uniformityInfo[proc].Value.ContainsKey(v));
+                uniformityInfo[proc].Value[v] = false;
+            }
+        }
+
+        public bool IsUniform(string proc, WhileCmd wc)
+        {
+            if (unstructured)
+                return false;
+
+            return !nonUniformLoops[proc].Contains(GetLoopId(wc));
+        }
+
+        public bool HasNonuniformReturn(string proc, WhileCmd whileCmd)
+        {
+            return loopsWithNonuniformReturn[proc].Contains(GetLoopId(whileCmd));
+        }
+    }
+
+}
diff --git a/Source/VCGeneration/VCGeneration.csproj b/Source/VCGeneration/VCGeneration.csproj
index 780e4891..fe7ddc70 100644
--- a/Source/VCGeneration/VCGeneration.csproj
+++ b/Source/VCGeneration/VCGeneration.csproj
@@ -1,227 +1,228 @@
-<?xml version="1.0" encoding="utf-8"?>

-<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">

-  <PropertyGroup>

-    <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>

-    <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>

-    <ProductVersion>9.0.21022</ProductVersion>

-    <SchemaVersion>2.0</SchemaVersion>

-    <ProjectGuid>{E1F10180-C7B9-4147-B51F-FA1B701966DC}</ProjectGuid>

-    <OutputType>Library</OutputType>

-    <AppDesignerFolder>Properties</AppDesignerFolder>

-    <RootNamespace>VCGeneration</RootNamespace>

-    <AssemblyName>VCGeneration</AssemblyName>

-    <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>

-    <FileAlignment>512</FileAlignment>

-    <CodeContractsAssemblyMode>1</CodeContractsAssemblyMode>

-    <SignAssembly>true</SignAssembly>

-    <AssemblyOriginatorKeyFile>..\InterimKey.snk</AssemblyOriginatorKeyFile>

-    <FileUpgradeFlags>

-    </FileUpgradeFlags>

-    <OldToolsVersion>3.5</OldToolsVersion>

-    <UpgradeBackupLocation />

-    <PublishUrl>publish\</PublishUrl>

-    <Install>true</Install>

-    <InstallFrom>Disk</InstallFrom>

-    <UpdateEnabled>false</UpdateEnabled>

-    <UpdateMode>Foreground</UpdateMode>

-    <UpdateInterval>7</UpdateInterval>

-    <UpdateIntervalUnits>Days</UpdateIntervalUnits>

-    <UpdatePeriodically>false</UpdatePeriodically>

-    <UpdateRequired>false</UpdateRequired>

-    <MapFileExtensions>true</MapFileExtensions>

-    <ApplicationRevision>0</ApplicationRevision>

-    <ApplicationVersion>1.0.0.%2a</ApplicationVersion>

-    <IsWebBootstrapper>false</IsWebBootstrapper>

-    <UseApplicationTrust>false</UseApplicationTrust>

-    <BootstrapperEnabled>true</BootstrapperEnabled>

-    <TargetFrameworkProfile>Client</TargetFrameworkProfile>

-  </PropertyGroup>

-  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">

-    <DebugSymbols>true</DebugSymbols>

-    <DebugType>full</DebugType>

-    <Optimize>false</Optimize>

-    <OutputPath>bin\Debug\</OutputPath>

-    <DefineConstants>DEBUG;TRACE</DefineConstants>

-    <ErrorReport>prompt</ErrorReport>

-    <WarningLevel>4</WarningLevel>

-    <CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>

-    <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>

-    <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>

-    <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>

-    <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>

-    <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>

-    <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>

-    <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>

-    <CodeContractsPointerObligations>False</CodeContractsPointerObligations>

-    <CodeContractsContainerAnalysis>False</CodeContractsContainerAnalysis>

-    <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>

-    <CodeContractsRunInBackground>True</CodeContractsRunInBackground>

-    <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>

-    <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>

-    <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>

-    <CodeContractsCustomRewriterAssembly>

-    </CodeContractsCustomRewriterAssembly>

-    <CodeContractsCustomRewriterClass>

-    </CodeContractsCustomRewriterClass>

-    <CodeContractsLibPaths>

-    </CodeContractsLibPaths>

-    <CodeContractsExtraRewriteOptions>

-    </CodeContractsExtraRewriteOptions>

-    <CodeContractsExtraAnalysisOptions>

-    </CodeContractsExtraAnalysisOptions>

-    <CodeContractsBaseLineFile>

-    </CodeContractsBaseLineFile>

-    <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>

-    <CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>

-    <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>

-  </PropertyGroup>

-  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">

-    <DebugType>pdbonly</DebugType>

-    <Optimize>true</Optimize>

-    <OutputPath>bin\Release\</OutputPath>

-    <DefineConstants>TRACE</DefineConstants>

-    <ErrorReport>prompt</ErrorReport>

-    <WarningLevel>4</WarningLevel>

-    <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>

-  </PropertyGroup>

-  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'z3apidebug|AnyCPU' ">

-    <DebugSymbols>true</DebugSymbols>

-    <OutputPath>bin\z3apidebug\</OutputPath>

-    <DefineConstants>DEBUG;TRACE</DefineConstants>

-    <DebugType>full</DebugType>

-    <PlatformTarget>AnyCPU</PlatformTarget>

-    <CodeAnalysisRuleAssemblies>

-    </CodeAnalysisRuleAssemblies>

-    <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>

-    <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>

-    <ErrorReport>prompt</ErrorReport>

-    <CodeAnalysisRuleSet>Migrated rules for VCGeneration.ruleset</CodeAnalysisRuleSet>

-    <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>

-  </PropertyGroup>

-  <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|AnyCPU'">

-    <DebugSymbols>true</DebugSymbols>

-    <OutputPath>bin\Checked\</OutputPath>

-    <DefineConstants>DEBUG;TRACE</DefineConstants>

-    <DebugType>full</DebugType>

-    <PlatformTarget>AnyCPU</PlatformTarget>

-    <CodeAnalysisLogFile>bin\Debug\VCGeneration.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>

-    <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>

-    <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>

-    <ErrorReport>prompt</ErrorReport>

-    <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>

-    <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>

-    <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>

-    <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>

-    <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>

-    <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>

-    <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>

-    <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>

-    <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>

-    <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>

-    <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>

-    <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>

-    <CodeContractsEnumObligations>False</CodeContractsEnumObligations>

-    <CodeContractsPointerObligations>False</CodeContractsPointerObligations>

-    <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>

-    <CodeContractsRunInBackground>True</CodeContractsRunInBackground>

-    <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>

-    <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>

-    <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>

-    <CodeContractsCustomRewriterAssembly />

-    <CodeContractsCustomRewriterClass />

-    <CodeContractsLibPaths />

-    <CodeContractsExtraRewriteOptions />

-    <CodeContractsExtraAnalysisOptions />

-    <CodeContractsBaseLineFile />

-    <CodeContractsCacheAnalysisResults>False</CodeContractsCacheAnalysisResults>

-    <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>

-    <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>

-    <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>

-  </PropertyGroup>

-  <ItemGroup>

-    <Reference Include="System" />

-    <Reference Include="System.Data" />

-    <Reference Include="System.Xml" />

-  </ItemGroup>

-  <ItemGroup>

-    <Compile Include="BlockPredicator.cs" />

-    <Compile Include="Check.cs" />

-    <Compile Include="ConditionGeneration.cs" />

-    <Compile Include="Context.cs" />

-    <Compile Include="DoomCheck.cs" />

-    <Compile Include="DoomedLoopUnrolling.cs" />

-    <Compile Include="DoomedStrategy.cs" />

-    <Compile Include="DoomErrorHandler.cs" />

-    <Compile Include="GraphAlgorithms.cs" />

-    <Compile Include="HasseDiagram.cs" />

-    <Compile Include="OrderingAxioms.cs" />

-    <Compile Include="SmartBlockPredicator.cs" />

-    <Compile Include="StratifiedVC.cs" />

-    <Compile Include="VC.cs" />

-    <Compile Include="VCDoomed.cs" />

-    <Compile Include="..\version.cs" />

-    <Compile Include="Wlp.cs" />

-  </ItemGroup>

-  <ItemGroup>

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

-      <Project>{39B0658D-C955-41C5-9A43-48C97A1EF5FD}</Project>

-      <Name>AIFramework</Name>

-    </ProjectReference>

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

-      <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>

-      <Name>Basetypes</Name>

-    </ProjectReference>

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

-      <Project>{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}</Project>

-      <Name>CodeContractsExtender</Name>

-    </ProjectReference>

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

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

-      <Name>Core</Name>

-    </ProjectReference>

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

-      <Project>{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}</Project>

-      <Name>Graph</Name>

-    </ProjectReference>

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

-      <Project>{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}</Project>

-      <Name>Model</Name>

-    </ProjectReference>

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

-      <Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project>

-      <Name>ParserHelper</Name>

-    </ProjectReference>

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

-      <Project>{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}</Project>

-      <Name>VCExpr</Name>

-    </ProjectReference>

-  </ItemGroup>

-  <ItemGroup>

-    <Folder Include="Properties\" />

-  </ItemGroup>

-  <ItemGroup>

-    <BootstrapperPackage Include="Microsoft.Net.Client.3.5">

-      <Visible>False</Visible>

-      <ProductName>.NET Framework 3.5 SP1 Client Profile</ProductName>

-      <Install>false</Install>

-    </BootstrapperPackage>

-    <BootstrapperPackage Include="Microsoft.Net.Framework.3.5.SP1">

-      <Visible>False</Visible>

-      <ProductName>.NET Framework 3.5 SP1</ProductName>

-      <Install>true</Install>

-    </BootstrapperPackage>

-    <BootstrapperPackage Include="Microsoft.Windows.Installer.3.1">

-      <Visible>False</Visible>

-      <ProductName>Windows Installer 3.1</ProductName>

-      <Install>true</Install>

-    </BootstrapperPackage>

-  </ItemGroup>

-  <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />

-  <!-- To modify your build process, add your task inside one of the targets below and uncomment it. 

-       Other similar extension points exist, see Microsoft.Common.targets.

-  <Target Name="BeforeBuild">

-  </Target>

-  <Target Name="AfterBuild">

-  </Target>

-  -->

-</Project>

+<?xml version="1.0" encoding="utf-8"?>
+<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
+  <PropertyGroup>
+    <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
+    <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
+    <ProductVersion>9.0.21022</ProductVersion>
+    <SchemaVersion>2.0</SchemaVersion>
+    <ProjectGuid>{E1F10180-C7B9-4147-B51F-FA1B701966DC}</ProjectGuid>
+    <OutputType>Library</OutputType>
+    <AppDesignerFolder>Properties</AppDesignerFolder>
+    <RootNamespace>VCGeneration</RootNamespace>
+    <AssemblyName>VCGeneration</AssemblyName>
+    <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
+    <FileAlignment>512</FileAlignment>
+    <CodeContractsAssemblyMode>1</CodeContractsAssemblyMode>
+    <SignAssembly>true</SignAssembly>
+    <AssemblyOriginatorKeyFile>..\InterimKey.snk</AssemblyOriginatorKeyFile>
+    <FileUpgradeFlags>
+    </FileUpgradeFlags>
+    <OldToolsVersion>3.5</OldToolsVersion>
+    <UpgradeBackupLocation />
+    <PublishUrl>publish\</PublishUrl>
+    <Install>true</Install>
+    <InstallFrom>Disk</InstallFrom>
+    <UpdateEnabled>false</UpdateEnabled>
+    <UpdateMode>Foreground</UpdateMode>
+    <UpdateInterval>7</UpdateInterval>
+    <UpdateIntervalUnits>Days</UpdateIntervalUnits>
+    <UpdatePeriodically>false</UpdatePeriodically>
+    <UpdateRequired>false</UpdateRequired>
+    <MapFileExtensions>true</MapFileExtensions>
+    <ApplicationRevision>0</ApplicationRevision>
+    <ApplicationVersion>1.0.0.%2a</ApplicationVersion>
+    <IsWebBootstrapper>false</IsWebBootstrapper>
+    <UseApplicationTrust>false</UseApplicationTrust>
+    <BootstrapperEnabled>true</BootstrapperEnabled>
+    <TargetFrameworkProfile>Client</TargetFrameworkProfile>
+  </PropertyGroup>
+  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
+    <DebugSymbols>true</DebugSymbols>
+    <DebugType>full</DebugType>
+    <Optimize>false</Optimize>
+    <OutputPath>bin\Debug\</OutputPath>
+    <DefineConstants>DEBUG;TRACE</DefineConstants>
+    <ErrorReport>prompt</ErrorReport>
+    <WarningLevel>4</WarningLevel>
+    <CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>
+    <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
+    <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
+    <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
+    <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
+    <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>
+    <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>
+    <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
+    <CodeContractsPointerObligations>False</CodeContractsPointerObligations>
+    <CodeContractsContainerAnalysis>False</CodeContractsContainerAnalysis>
+    <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
+    <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
+    <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>
+    <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
+    <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
+    <CodeContractsCustomRewriterAssembly>
+    </CodeContractsCustomRewriterAssembly>
+    <CodeContractsCustomRewriterClass>
+    </CodeContractsCustomRewriterClass>
+    <CodeContractsLibPaths>
+    </CodeContractsLibPaths>
+    <CodeContractsExtraRewriteOptions>
+    </CodeContractsExtraRewriteOptions>
+    <CodeContractsExtraAnalysisOptions>
+    </CodeContractsExtraAnalysisOptions>
+    <CodeContractsBaseLineFile>
+    </CodeContractsBaseLineFile>
+    <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
+    <CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>
+    <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
+  </PropertyGroup>
+  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
+    <DebugType>pdbonly</DebugType>
+    <Optimize>true</Optimize>
+    <OutputPath>bin\Release\</OutputPath>
+    <DefineConstants>TRACE</DefineConstants>
+    <ErrorReport>prompt</ErrorReport>
+    <WarningLevel>4</WarningLevel>
+    <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
+  </PropertyGroup>
+  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'z3apidebug|AnyCPU' ">
+    <DebugSymbols>true</DebugSymbols>
+    <OutputPath>bin\z3apidebug\</OutputPath>
+    <DefineConstants>DEBUG;TRACE</DefineConstants>
+    <DebugType>full</DebugType>
+    <PlatformTarget>AnyCPU</PlatformTarget>
+    <CodeAnalysisRuleAssemblies>
+    </CodeAnalysisRuleAssemblies>
+    <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
+    <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
+    <ErrorReport>prompt</ErrorReport>
+    <CodeAnalysisRuleSet>Migrated rules for VCGeneration.ruleset</CodeAnalysisRuleSet>
+    <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
+  </PropertyGroup>
+  <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|AnyCPU'">
+    <DebugSymbols>true</DebugSymbols>
+    <OutputPath>bin\Checked\</OutputPath>
+    <DefineConstants>DEBUG;TRACE</DefineConstants>
+    <DebugType>full</DebugType>
+    <PlatformTarget>AnyCPU</PlatformTarget>
+    <CodeAnalysisLogFile>bin\Debug\VCGeneration.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>
+    <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
+    <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
+    <ErrorReport>prompt</ErrorReport>
+    <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
+    <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
+    <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
+    <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>
+    <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
+    <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
+    <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
+    <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
+    <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
+    <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>
+    <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>
+    <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
+    <CodeContractsEnumObligations>False</CodeContractsEnumObligations>
+    <CodeContractsPointerObligations>False</CodeContractsPointerObligations>
+    <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
+    <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
+    <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>
+    <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
+    <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
+    <CodeContractsCustomRewriterAssembly />
+    <CodeContractsCustomRewriterClass />
+    <CodeContractsLibPaths />
+    <CodeContractsExtraRewriteOptions />
+    <CodeContractsExtraAnalysisOptions />
+    <CodeContractsBaseLineFile />
+    <CodeContractsCacheAnalysisResults>False</CodeContractsCacheAnalysisResults>
+    <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
+    <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>
+    <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
+  </PropertyGroup>
+  <ItemGroup>
+    <Reference Include="System" />
+    <Reference Include="System.Data" />
+    <Reference Include="System.Xml" />
+  </ItemGroup>
+  <ItemGroup>
+    <Compile Include="BlockPredicator.cs" />
+    <Compile Include="Check.cs" />
+    <Compile Include="ConditionGeneration.cs" />
+    <Compile Include="Context.cs" />
+    <Compile Include="DoomCheck.cs" />
+    <Compile Include="DoomedLoopUnrolling.cs" />
+    <Compile Include="DoomedStrategy.cs" />
+    <Compile Include="DoomErrorHandler.cs" />
+    <Compile Include="GraphAlgorithms.cs" />
+    <Compile Include="HasseDiagram.cs" />
+    <Compile Include="OrderingAxioms.cs" />
+    <Compile Include="SmartBlockPredicator.cs" />
+    <Compile Include="StratifiedVC.cs" />
+    <Compile Include="UniformityAnalyser.cs" />
+    <Compile Include="VC.cs" />
+    <Compile Include="VCDoomed.cs" />
+    <Compile Include="..\version.cs" />
+    <Compile Include="Wlp.cs" />
+  </ItemGroup>
+  <ItemGroup>
+    <ProjectReference Include="..\AIFramework\AIFramework.csproj">
+      <Project>{39B0658D-C955-41C5-9A43-48C97A1EF5FD}</Project>
+      <Name>AIFramework</Name>
+    </ProjectReference>
+    <ProjectReference Include="..\Basetypes\Basetypes.csproj">
+      <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>
+      <Name>Basetypes</Name>
+    </ProjectReference>
+    <ProjectReference Include="..\CodeContractsExtender\CodeContractsExtender.csproj">
+      <Project>{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}</Project>
+      <Name>CodeContractsExtender</Name>
+    </ProjectReference>
+    <ProjectReference Include="..\Core\Core.csproj">
+      <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>
+      <Name>Core</Name>
+    </ProjectReference>
+    <ProjectReference Include="..\Graph\Graph.csproj">
+      <Project>{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}</Project>
+      <Name>Graph</Name>
+    </ProjectReference>
+    <ProjectReference Include="..\Model\Model.csproj">
+      <Project>{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}</Project>
+      <Name>Model</Name>
+    </ProjectReference>
+    <ProjectReference Include="..\ParserHelper\ParserHelper.csproj">
+      <Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project>
+      <Name>ParserHelper</Name>
+    </ProjectReference>
+    <ProjectReference Include="..\VCExpr\VCExpr.csproj">
+      <Project>{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}</Project>
+      <Name>VCExpr</Name>
+    </ProjectReference>
+  </ItemGroup>
+  <ItemGroup>
+    <Folder Include="Properties\" />
+  </ItemGroup>
+  <ItemGroup>
+    <BootstrapperPackage Include="Microsoft.Net.Client.3.5">
+      <Visible>False</Visible>
+      <ProductName>.NET Framework 3.5 SP1 Client Profile</ProductName>
+      <Install>false</Install>
+    </BootstrapperPackage>
+    <BootstrapperPackage Include="Microsoft.Net.Framework.3.5.SP1">
+      <Visible>False</Visible>
+      <ProductName>.NET Framework 3.5 SP1</ProductName>
+      <Install>true</Install>
+    </BootstrapperPackage>
+    <BootstrapperPackage Include="Microsoft.Windows.Installer.3.1">
+      <Visible>False</Visible>
+      <ProductName>Windows Installer 3.1</ProductName>
+      <Install>true</Install>
+    </BootstrapperPackage>
+  </ItemGroup>
+  <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />
+  <!-- To modify your build process, add your task inside one of the targets below and uncomment it. 
+       Other similar extension points exist, see Microsoft.Common.targets.
+  <Target Name="BeforeBuild">
+  </Target>
+  <Target Name="AfterBuild">
+  </Target>
+  -->
+</Project>
\ No newline at end of file