Merge

16 files changed, 529 insertions, 111 deletions

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index db7551ce..5c18ddfe 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -397,6 +397,9 @@ namespace Microsoft.Boogie {
     public bool IntraproceduralInfer = true;

     public bool ContractInfer = false;

     public bool ExplainHoudini = false;

+    public bool ConcurrentHoudini = false;

+    public bool ModifyTopologicalSorting = false;

+    public bool DebugConcurrentHoudini = false;

     public bool HoudiniUseCrossDependencies = false;

     public string StagedHoudini = null;

     public bool DebugStagedHoudini = false;

@@ -643,6 +646,16 @@ namespace Microsoft.Boogie {
     }

     public AiFlags/*!*/ Ai = new AiFlags();

 

+    public class ConcurrentHoudiniOptions

+    {

+      public List<string> ProverOptions = new List<string>();

+      public int ProverCCLimit = 5;

+      public bool DisableLoopInvEntryAssert = false;

+      public bool DisableLoopInvMaintainedAssert = false;

+      public bool ModifyTopologicalSorting = false;

+    }

+    public List<ConcurrentHoudiniOptions> Cho = new List<ConcurrentHoudiniOptions>();

+

     protected override bool ParseOption(string name, CommandLineOptionEngine.CommandLineParseState ps) {

       var args = ps.args;  // convenient synonym

       switch (name) {

@@ -1165,6 +1178,24 @@ namespace Microsoft.Boogie {
           }

           return true;

 

+        case "concurrentHoudini":

+          if (ps.ConfirmArgumentCount(0)) {

+            ConcurrentHoudini = true;

+          }

+          return true;

+

+        case "modifyTopologicalSorting":

+          if (ps.ConfirmArgumentCount(0)) {

+            ModifyTopologicalSorting = true;

+          }

+          return true;

+

+        case "debugConcurrentHoudini":

+          if (ps.ConfirmArgumentCount(0)) {

+            DebugConcurrentHoudini = true;

+          }

+          return true;

+

         case "vcBrackets":

           ps.GetNumericArgument(ref BracketIdsInVC, 2);

           return true;

diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs
index 9a35e9f4..06ef2c27 100644
--- a/Source/Core/DeadVarElim.cs
+++ b/Source/Core/DeadVarElim.cs
@@ -419,7 +419,12 @@ namespace Microsoft.Boogie {
         }

       }

 

-      IEnumerable<Block> sortedNodes = dag.TopologicalSort();

+      IEnumerable<Block> sortedNodes;

+      if (CommandLineOptions.Clo.ModifyTopologicalSorting) {

+        sortedNodes = dag.TopologicalSort(true);

+      } else {

+        sortedNodes = dag.TopologicalSort();

+      }

       foreach (Block/*!*/ block in sortedNodes) {

         Contract.Assert(block != null);

         HashSet<Variable/*!*/>/*!*/ liveVarsAfter = new HashSet<Variable/*!*/>();

diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs
index 1d221bb7..ef958fa6 100644
--- a/Source/Core/Duplicator.cs
+++ b/Source/Core/Duplicator.cs
@@ -121,7 +121,7 @@ namespace Microsoft.Boogie {
     public override List<Cmd> VisitCmdSeq(List<Cmd> cmdSeq) {

       //Contract.Requires(cmdSeq != null);

       Contract.Ensures(Contract.Result<List<Cmd>>() != null);

-      return base.VisitCmdSeq(cmdSeq);

+      return base.VisitCmdSeq(new List<Cmd>(cmdSeq));

     }

     public override Constant VisitConstant(Constant node) {

       //Contract.Requires(node != null);

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index 96973cc8..92cc7429 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -689,7 +689,6 @@ namespace Microsoft.Boogie
       }

     }

 

-

     /// <summary>

     /// Given a resolved and type checked Boogie program, infers invariants for the program

     /// and then attempts to verify it.  Returns:

diff --git a/Source/Graph/Graph.cs b/Source/Graph/Graph.cs
index b6fe8cfc..4a78c27f 100644
--- a/Source/Graph/Graph.cs
+++ b/Source/Graph/Graph.cs
@@ -522,14 +522,14 @@ namespace Microsoft.Boogie.GraphUtil {
       return dominees == null ? new List<Node>() : dominees;

     }

 

-    public IEnumerable<Node/*?*/> TopologicalSort() {

+    public IEnumerable<Node/*?*/> TopologicalSort(bool reversed = false) {

       bool acyclic;

       List<Node> sortedList;

-      this.TarjanTopSort(out acyclic, out sortedList);

+      this.TarjanTopSort(out acyclic, out sortedList, reversed);

       return acyclic ? sortedList : new List<Node>();

     }

     // From Tarjan 1972

-    public void TarjanTopSort(out bool acyclic, out List<Node> sortedNodes) {

+    public void TarjanTopSort(out bool acyclic, out List<Node> sortedNodes, bool reversed = false) {

       int n = this.Nodes.Count;

       if (n == 0) {

         acyclic = true;

@@ -558,10 +558,19 @@ namespace Microsoft.Boogie.GraphUtil {
       while (sortedIndex < n) {

         // find a root (i.e., its index)

         int rootIndex = -1;

-        for (int i = 0; i < n; i++) {

-          if (incomingEdges[i] == 0) {

-            rootIndex = i;

-            break;

+        if (reversed) {

+          for (int i = n-1; i >= 0; i--) {

+            if (incomingEdges[i] == 0) {

+              rootIndex = i;

+              break;

+            }

+          }

+        } else {

+          for (int i = 0; i < n; i++) {

+            if (incomingEdges[i] == 0) {

+              rootIndex = i;

+              break;

+            }

           }

         }

         if (rootIndex == -1) {

diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs
index 170b5212..252321b6 100644
--- a/Source/Houdini/Checker.cs
+++ b/Source/Houdini/Checker.cs
@@ -130,13 +130,13 @@ namespace Microsoft.Boogie.Houdini {
       return false;

     }

 

-    public HoudiniSession(Houdini houdini, VCGen vcgen, ProverInterface proverInterface, Program program, Implementation impl, HoudiniStatistics stats) {

+    public HoudiniSession(Houdini houdini, VCGen vcgen, ProverInterface proverInterface, Program program, Implementation impl, HoudiniStatistics stats, int taskID = -1) {

       this.descriptiveName = impl.Name;

       this.stats = stats;

       collector = new ConditionGeneration.CounterexampleCollector();

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

 

-      vcgen.ConvertCFG2DAG(impl);

+      vcgen.ConvertCFG2DAG(impl, taskID: taskID);

       ModelViewInfo mvInfo;

       var gotoCmdOrigins = vcgen.PassifyImpl(impl, out mvInfo);

 

@@ -222,7 +222,7 @@ namespace Microsoft.Boogie.Houdini {
       return expr;

     }

 

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

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

       collector.examples.Clear();

 

       if (CommandLineOptions.Clo.Trace) {

@@ -232,7 +232,7 @@ namespace Microsoft.Boogie.Houdini {
 

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

       proverInterface.BeginCheck(descriptiveName, vc, handler);

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

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

 

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

       stats.proverTime += queryTime;

diff --git a/Source/Houdini/ConcurrentHoudini.cs b/Source/Houdini/ConcurrentHoudini.cs
new file mode 100644
index 00000000..b16370e9
--- /dev/null
+++ b/Source/Houdini/ConcurrentHoudini.cs
@@ -0,0 +1,300 @@
+using System;
+using System.IO;
+using System.Collections.Generic;
+using System.Collections.Concurrent;
+using System.Diagnostics;
+using System.Diagnostics.Contracts;
+using System.Text.RegularExpressions;
+using System.Linq;
+using VC;
+
+namespace Microsoft.Boogie.Houdini
+{
+  public class ConcurrentHoudini : Houdini
+  {
+    int id;
+
+    private static ConcurrentDictionary<string, RefutedAnnotation> refutedSharedAnnotations;
+
+    public static ConcurrentDictionary<string, RefutedAnnotation> RefutedSharedAnnotations { get { return refutedSharedAnnotations; } }
+
+    public ConcurrentHoudini(int id, Program program, HoudiniSession.HoudiniStatistics stats, string cexTraceFile = "houdiniCexTrace.bpl") {
+      Contract.Assert(id >= 0);
+
+      this.id = id;
+      this.program = program;
+      this.cexTraceFile = cexTraceFile;
+
+      if (CommandLineOptions.Clo.Trace)
+        Console.WriteLine("Collecting existential constants...");
+      this.houdiniConstants = CollectExistentialConstants();
+
+      if (CommandLineOptions.Clo.Trace)
+        Console.WriteLine("Building call graph...");
+      this.callGraph = Program.BuildCallGraph(program);
+      if (CommandLineOptions.Clo.Trace)
+        Console.WriteLine("Number of implementations = {0}", callGraph.Nodes.Count);
+
+      if (CommandLineOptions.Clo.HoudiniUseCrossDependencies)
+      {
+        if (CommandLineOptions.Clo.Trace) Console.WriteLine("Computing procedure cross dependencies ...");
+        this.crossDependencies = new CrossDependencies(this.houdiniConstants);
+        this.crossDependencies.Visit(program);
+      }
+
+      Inline();
+
+      this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, new List<Checker>());
+      this.proverInterface = ProverInterface.CreateProver(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, CommandLineOptions.Clo.ProverKillTime, id);
+
+      vcgenFailures = new HashSet<Implementation>();
+      Dictionary<Implementation, HoudiniSession> houdiniSessions = new Dictionary<Implementation, HoudiniSession>();
+      if (CommandLineOptions.Clo.Trace)
+        Console.WriteLine("Beginning VC generation for Houdini...");
+      foreach (Implementation impl in callGraph.Nodes) {
+        try {
+          if (CommandLineOptions.Clo.Trace)
+            Console.WriteLine("Generating VC for {0}", impl.Name);
+          HoudiniSession session = new HoudiniSession(this, vcgen, proverInterface, program, impl, stats, taskID: id);
+          houdiniSessions.Add(impl, session);
+        }
+        catch (VCGenException) {
+          if (CommandLineOptions.Clo.Trace)
+            Console.WriteLine("VC generation failed");
+          vcgenFailures.Add(impl);
+        }
+      }
+      this.houdiniSessions = new ReadOnlyDictionary<Implementation, HoudiniSession>(houdiniSessions);
+
+      if (CommandLineOptions.Clo.ExplainHoudini)
+      {
+        // Print results of ExplainHoudini to a dotty file
+        explainHoudiniDottyFile = new StreamWriter("explainHoudini.dot");
+        explainHoudiniDottyFile.WriteLine("digraph explainHoudini {");
+        foreach (var constant in houdiniConstants)
+          explainHoudiniDottyFile.WriteLine("{0} [ label = \"{0}\" color=black ];", constant.Name);
+        explainHoudiniDottyFile.WriteLine("TimeOut [label = \"TimeOut\" color=red ];");
+      }
+    }
+
+    static ConcurrentHoudini()
+    {
+      refutedSharedAnnotations = new ConcurrentDictionary<string, RefutedAnnotation>();
+    }
+
+    private bool ExchangeRefutedAnnotations()
+    {
+      int count = 0;
+
+      if (CommandLineOptions.Clo.DebugConcurrentHoudini)
+        Console.WriteLine("# number of shared refuted annotations: " + refutedSharedAnnotations.Count);
+
+      foreach (string key in refutedSharedAnnotations.Keys) {
+        KeyValuePair<Variable, bool> kv = currentHoudiniState.Assignment.FirstOrDefault(entry => entry.Key.Name.Equals(key) && entry.Value);
+
+        if (kv.Key != null) {
+          RefutedAnnotation ra = null;
+          Implementation refutationSite = null;
+
+          foreach (var r in program.TopLevelDeclarations.OfType<Implementation>()) {
+            if (r.Name.Equals(refutedSharedAnnotations[key].RefutationSite.Name)) {
+              refutationSite = r;
+              break;
+            }
+          }
+          Debug.Assert(refutationSite != null);
+
+          if (refutedSharedAnnotations[key].Kind == RefutedAnnotationKind.REQUIRES) {
+            Procedure proc = null;
+            foreach (var p in program.TopLevelDeclarations.OfType<Procedure>()) {
+              if (p.Name.Equals(refutedSharedAnnotations[key].CalleeProc.Name)) {
+                proc = p;
+                break;
+              }
+            }
+            Debug.Assert(proc != null);
+            ra = RefutedAnnotation.BuildRefutedRequires(kv.Key, proc, refutationSite);
+          } else if (refutedSharedAnnotations[key].Kind == RefutedAnnotationKind.ENSURES)
+            ra = RefutedAnnotation.BuildRefutedEnsures(kv.Key, refutationSite);
+          else if (refutedSharedAnnotations[key].Kind == RefutedAnnotationKind.ASSERT)
+            ra = RefutedAnnotation.BuildRefutedAssert(kv.Key, refutationSite);
+          Debug.Assert(ra != null);
+
+          if (CommandLineOptions.Clo.DebugConcurrentHoudini)
+            Console.WriteLine("(+) " + ra.Constant + "," + ra.Kind + "," + ra.CalleeProc + "," + ra.RefutationSite);
+
+          AddRelatedToWorkList(ra);
+          UpdateAssignment(ra);
+          count++;
+        }
+      }
+
+      return count > 0 ? true : false;
+    }
+
+    protected override bool UpdateAssignmentWorkList(ProverInterface.Outcome outcome,
+                                                     List<Counterexample> errors)
+    {
+      Contract.Assume(currentHoudiniState.Implementation != null);
+      bool dequeue = true;
+
+      switch (outcome) {
+        case ProverInterface.Outcome.Valid:
+        //yeah, dequeue
+        break;
+
+        case ProverInterface.Outcome.Invalid:
+        Contract.Assume(errors != null);
+
+        foreach (Counterexample error in errors) {
+          RefutedAnnotation refutedAnnotation = ExtractRefutedAnnotation(error);
+          // some candidate annotation removed
+          if (refutedAnnotation != null) {
+            refutedSharedAnnotations.TryAdd(refutedAnnotation.Constant.Name, refutedAnnotation);
+            AddRelatedToWorkList(refutedAnnotation);
+            UpdateAssignment(refutedAnnotation);
+            dequeue = false;
+
+            #region Extra debugging output
+            if (CommandLineOptions.Clo.Trace) {
+              using (var cexWriter = new System.IO.StreamWriter(cexTraceFile, true)) {
+                cexWriter.WriteLine("Counter example for " + refutedAnnotation.Constant);
+                cexWriter.Write(error.ToString());
+                cexWriter.WriteLine();
+                using (var writer = new Microsoft.Boogie.TokenTextWriter(cexWriter))
+                  foreach (Microsoft.Boogie.Block blk in error.Trace)
+                    blk.Emit(writer, 15);
+                //cexWriter.WriteLine(); 
+              }
+            }
+            #endregion
+          }
+        }
+
+        if (ExchangeRefutedAnnotations()) dequeue = false;
+
+        break;
+        default:
+        if (CommandLineOptions.Clo.Trace) {
+          Console.WriteLine("Timeout/Spaceout while verifying " + currentHoudiniState.Implementation.Name);
+        }
+
+        HoudiniSession houdiniSession;
+        houdiniSessions.TryGetValue(currentHoudiniState.Implementation, out houdiniSession);
+
+        foreach (Variable v in houdiniSession.houdiniAssertConstants) {
+          if (CommandLineOptions.Clo.Trace) {
+            Console.WriteLine("Removing " + v);
+          }
+          currentHoudiniState.Assignment.Remove(v);
+          currentHoudiniState.Assignment.Add(v, false);
+          this.NotifyConstant(v.Name);
+        }
+
+        currentHoudiniState.addToBlackList(currentHoudiniState.Implementation.Name);
+        break;
+      }
+
+      return dequeue;
+    }
+
+    public override HoudiniOutcome PerformHoudiniInference(int stage = 0, 
+                                                           IEnumerable<int> completedStages = null,
+                                                           Dictionary<string, bool> initialAssignment = null)
+    {
+      this.NotifyStart(program, houdiniConstants.Count);
+
+      currentHoudiniState = new HoudiniState(BuildWorkList(program), BuildAssignment(houdiniConstants));
+
+      if(initialAssignment != null) {
+        foreach(var v in currentHoudiniState.Assignment.Keys.ToList()) {
+          currentHoudiniState.Assignment[v] = initialAssignment[v.Name];
+        }
+      }
+
+      foreach (Implementation impl in vcgenFailures) {
+        currentHoudiniState.addToBlackList(impl.Name);
+      }
+
+      while (currentHoudiniState.WorkQueue.Count > 0) {
+        this.NotifyIteration();
+
+        ExchangeRefutedAnnotations();
+        currentHoudiniState.Implementation = currentHoudiniState.WorkQueue.Peek();
+        this.NotifyImplementation(currentHoudiniState.Implementation);
+
+        HoudiniSession session;
+        this.houdiniSessions.TryGetValue(currentHoudiniState.Implementation, out session);
+        HoudiniVerifyCurrent(session, stage, completedStages);
+      }
+
+      this.NotifyEnd(true);
+      Dictionary<string, bool> assignment = new Dictionary<string, bool>();
+      foreach (var x in currentHoudiniState.Assignment)
+        assignment[x.Key.Name] = x.Value;
+      currentHoudiniState.Outcome.assignment = assignment;
+      return currentHoudiniState.Outcome;
+    }
+
+    protected override void HoudiniVerifyCurrent(HoudiniSession session, int stage, IEnumerable<int> completedStages)
+    {
+      while (true) {
+        this.NotifyAssignment(currentHoudiniState.Assignment);
+
+        //check the VC with the current assignment
+        List<Counterexample> errors;
+        ProverInterface.Outcome outcome = TryCatchVerify(session, stage, completedStages, out errors);
+        this.NotifyOutcome(outcome);
+
+        DebugRefutedCandidates(currentHoudiniState.Implementation, errors);
+
+        #region Explain Houdini
+        if (CommandLineOptions.Clo.ExplainHoudini && outcome == ProverInterface.Outcome.Invalid)
+        {
+          Contract.Assume(errors != null);
+          // make a copy of this variable
+          errors = new List<Counterexample>(errors);
+          var refutedAnnotations = new List<RefutedAnnotation>();
+          foreach (Counterexample error in errors)
+          {
+            RefutedAnnotation refutedAnnotation = ExtractRefutedAnnotation(error);
+            if (refutedAnnotation == null || refutedAnnotation.Kind == RefutedAnnotationKind.ASSERT) continue;
+            refutedAnnotations.Add(refutedAnnotation);
+          }
+          foreach (var refutedAnnotation in refutedAnnotations)
+          {
+            session.Explain(proverInterface, currentHoudiniState.Assignment, refutedAnnotation.Constant);
+          }
+        }
+        #endregion
+
+        if (UpdateHoudiniOutcome(currentHoudiniState.Outcome, currentHoudiniState.Implementation, outcome, errors)) { // abort
+          currentHoudiniState.WorkQueue.Dequeue();
+          this.NotifyDequeue();
+          FlushWorkList(stage, completedStages);
+          return;
+        }
+        else if (UpdateAssignmentWorkList(outcome, errors)) {
+          if (CommandLineOptions.Clo.UseUnsatCoreForContractInfer && outcome == ProverInterface.Outcome.Valid)
+            session.UpdateUnsatCore(proverInterface, currentHoudiniState.Assignment);
+          currentHoudiniState.WorkQueue.Dequeue();
+          this.NotifyDequeue();
+          return;
+        }
+      } 
+    }
+
+    protected override ProverInterface.Outcome TryCatchVerify(HoudiniSession session, int stage, IEnumerable<int> completedStages, out List<Counterexample> errors) {
+      ProverInterface.Outcome outcome;
+      try {
+        outcome = session.Verify(proverInterface, GetAssignmentWithStages(stage, completedStages), out errors, taskID: id);
+      }
+      catch (UnexpectedProverOutputException upo) {
+        Contract.Assume(upo != null);
+        errors = null;
+        outcome = ProverInterface.Outcome.Undetermined;
+      }
+      return outcome;
+    }
+  }
+}
diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index afae3143..c3575800 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -17,7 +17,7 @@ using System.Diagnostics;
 

 namespace Microsoft.Boogie.Houdini {

 

-  class ReadOnlyDictionary<K, V> {

+  internal class ReadOnlyDictionary<K, V> {

     private Dictionary<K, V> dictionary;

     public ReadOnlyDictionary(Dictionary<K, V> dictionary) {

       this.dictionary = dictionary;

@@ -305,22 +305,24 @@ namespace Microsoft.Boogie.Houdini {
   }

 

   public class Houdini : ObservableHoudini {

-    private Program program;

-    private HashSet<Variable> houdiniConstants;

-    private ReadOnlyDictionary<Implementation, HoudiniSession> houdiniSessions;

-    private VCGen vcgen;

-    private ProverInterface proverInterface;

-    private Graph<Implementation> callGraph;

-    private HashSet<Implementation> vcgenFailures;

-    private HoudiniState currentHoudiniState;

-    private CrossDependencies crossDependencies;

-

-    private string cexTraceFile;

+    protected Program program;

+    protected HashSet<Variable> houdiniConstants;

+    protected VCGen vcgen;

+    protected ProverInterface proverInterface;

+    protected Graph<Implementation> callGraph;

+    protected HashSet<Implementation> vcgenFailures;

+    protected HoudiniState currentHoudiniState;

+    protected CrossDependencies crossDependencies;

+    internal ReadOnlyDictionary<Implementation, HoudiniSession> houdiniSessions;

+

+    protected string cexTraceFile;

 

     public HoudiniState CurrentHoudiniState { get { return currentHoudiniState; } }    

 

     public static TextWriter explainHoudiniDottyFile;

 

+    protected Houdini() { }

+

     public Houdini(Program program, HoudiniSession.HoudiniStatistics stats, string cexTraceFile = "houdiniCexTrace.bpl") {

       this.program = program;

       this.cexTraceFile = cexTraceFile;

@@ -377,7 +379,7 @@ namespace Microsoft.Boogie.Houdini {
       }

     }

 

-    private void Inline() {

+    protected void Inline() {

       if (CommandLineOptions.Clo.InlineDepth < 0)

         return;

 

@@ -434,7 +436,7 @@ namespace Microsoft.Boogie.Houdini {
       }

     }

 

-    private HashSet<Variable> CollectExistentialConstants() {

+    protected HashSet<Variable> CollectExistentialConstants() {

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

       foreach (Declaration decl in program.TopLevelDeclarations) {

         Constant constant = decl as Constant;

@@ -496,7 +498,7 @@ namespace Microsoft.Boogie.Houdini {
         public Dictionary<string, HashSet<Implementation>> assumedInImpl { get; private set; }

     }

     

-    private WorkQueue BuildWorkList(Program program) {

+    protected WorkQueue BuildWorkList(Program program) {

       // adding implementations to the workqueue from the bottom of the call graph upwards

       WorkQueue queue = new WorkQueue();

       StronglyConnectedComponents<Implementation> sccs =

@@ -634,7 +636,7 @@ namespace Microsoft.Boogie.Houdini {
         return null;

     }

 

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

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

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

       foreach (var constant in constants)

         initial.Add(constant, true);

@@ -659,7 +661,7 @@ namespace Microsoft.Boogie.Houdini {
 

     // Record most current non-candidate errors found

     // Return true if there was at least one non-candidate error

-    private bool UpdateHoudiniOutcome(HoudiniOutcome houdiniOutcome,

+    protected bool UpdateHoudiniOutcome(HoudiniOutcome houdiniOutcome,

                                       Implementation implementation,

                                       ProverInterface.Outcome outcome,

                                       List<Counterexample> errors) {

@@ -677,7 +679,7 @@ namespace Microsoft.Boogie.Houdini {
       return nonCandidateErrors.Count > 0;

     }

 

-    private void FlushWorkList(int stage, IEnumerable<int> completedStages) {

+    protected void FlushWorkList(int stage, IEnumerable<int> completedStages) {

       this.NotifyFlushStart();

       while (currentHoudiniState.WorkQueue.Count > 0) {

         this.NotifyIteration();

@@ -698,7 +700,7 @@ namespace Microsoft.Boogie.Houdini {
       this.NotifyFlushFinish();

     }

 

-    private void UpdateAssignment(RefutedAnnotation refAnnot) {

+    protected void UpdateAssignment(RefutedAnnotation refAnnot) {

       if (CommandLineOptions.Clo.Trace) {

         Console.WriteLine("Removing " + refAnnot.Constant);

         using (var cexWriter = new System.IO.StreamWriter(cexTraceFile, true))

@@ -709,9 +711,9 @@ namespace Microsoft.Boogie.Houdini {
       this.NotifyConstant(refAnnot.Constant.Name);

     }

 

-    private void AddRelatedToWorkList(RefutedAnnotation refutedAnnotation) {

+    protected void AddRelatedToWorkList(RefutedAnnotation refutedAnnotation) {

       Contract.Assume(currentHoudiniState.Implementation != null);

-      foreach (Implementation implementation in FindImplementationsToEnqueue(refutedAnnotation, currentHoudiniState.Implementation)) {

+      foreach (Implementation implementation in FindImplementationsToEnqueue(refutedAnnotation, refutedAnnotation.RefutationSite)) {

         if (!currentHoudiniState.isBlackListed(implementation.Name)) {

           currentHoudiniState.WorkQueue.Enqueue(implementation);

           this.NotifyEnqueue(implementation);

@@ -721,7 +723,7 @@ namespace Microsoft.Boogie.Houdini {
 

     // Updates the worklist and current assignment

     // @return true if the current function is dequeued

-    private bool UpdateAssignmentWorkList(ProverInterface.Outcome outcome,

+    protected virtual bool UpdateAssignmentWorkList(ProverInterface.Outcome outcome,

                                           List<Counterexample> errors) {

       Contract.Assume(currentHoudiniState.Implementation != null);

       bool dequeue = true;

@@ -731,34 +733,36 @@ namespace Microsoft.Boogie.Houdini {
           case ProverInterface.Outcome.Valid:

               //yeah, dequeue

               break;

+

           case ProverInterface.Outcome.Invalid:

               Contract.Assume(errors != null);

+

               foreach (Counterexample error in errors)

               {

-                  RefutedAnnotation refutedAnnotation = ExtractRefutedAnnotation(error);

-                  if (refutedAnnotation != null)

-                  { // some candidate annotation removed

-                      AddRelatedToWorkList(refutedAnnotation);

-                      UpdateAssignment(refutedAnnotation);

-                      dequeue = false;

-                      #region Extra debugging output

-                      if (CommandLineOptions.Clo.Trace)

-                      {

-                          using (var cexWriter = new System.IO.StreamWriter(cexTraceFile, true))

-                          {

-                              cexWriter.WriteLine("Counter example for " + refutedAnnotation.Constant);

-                              cexWriter.Write(error.ToString());

-                              cexWriter.WriteLine();

-                              using (var writer = new Microsoft.Boogie.TokenTextWriter(cexWriter))

-                                  foreach (Microsoft.Boogie.Block blk in error.Trace)

-                                      blk.Emit(writer, 15);

-                              //cexWriter.WriteLine(); 

-                          }

-                      }

-                      #endregion

-

+                RefutedAnnotation refutedAnnotation = ExtractRefutedAnnotation(error);

+                if (refutedAnnotation != null)

+                { // some candidate annotation removed

+                  AddRelatedToWorkList(refutedAnnotation);

+                  UpdateAssignment(refutedAnnotation);

+                  dequeue = false;

+                  #region Extra debugging output

+                  if (CommandLineOptions.Clo.Trace)

+                  {

+                    using (var cexWriter = new System.IO.StreamWriter(cexTraceFile, true))

+                    {

+                      cexWriter.WriteLine("Counter example for " + refutedAnnotation.Constant);

+                      cexWriter.Write(error.ToString());

+                      cexWriter.WriteLine();

+                      using (var writer = new Microsoft.Boogie.TokenTextWriter(cexWriter))

+                        foreach (Microsoft.Boogie.Block blk in error.Trace)

+                          blk.Emit(writer, 15);

+                      //cexWriter.WriteLine(); 

+                    }

                   }

+                  #endregion

+                }

               }

+              

               break;

           default:

               if (CommandLineOptions.Clo.Trace)

@@ -849,7 +853,7 @@ namespace Microsoft.Boogie.Houdini {
       }

     }

 

-    public HoudiniOutcome PerformHoudiniInference(int stage = 0, 

+    public virtual HoudiniOutcome PerformHoudiniInference(int stage = 0, 

                                                   IEnumerable<int> completedStages = null,

                                                   Dictionary<string, bool> initialAssignment = null) {

       this.NotifyStart(program, houdiniConstants.Count);

@@ -940,17 +944,19 @@ namespace Microsoft.Boogie.Houdini {
       return implementations;

     }

 

-    private enum RefutedAnnotationKind { REQUIRES, ENSURES, ASSERT };

+    public enum RefutedAnnotationKind { REQUIRES, ENSURES, ASSERT };

 

-    private class RefutedAnnotation {

+    public class RefutedAnnotation {

       private Variable _constant;

       private RefutedAnnotationKind _kind;

       private Procedure _callee;

+      private Implementation _refutationSite;

 

-      private RefutedAnnotation(Variable constant, RefutedAnnotationKind kind, Procedure callee) {

+      private RefutedAnnotation(Variable constant, RefutedAnnotationKind kind, Procedure callee, Implementation refutationSite) {

         this._constant = constant;

         this._kind = kind;

         this._callee = callee;

+        this._refutationSite = refutationSite;

       }

       public RefutedAnnotationKind Kind {

         get { return this._kind; }

@@ -961,14 +967,47 @@ namespace Microsoft.Boogie.Houdini {
       public Procedure CalleeProc {

         get { return this._callee; }

       }

-      public static RefutedAnnotation BuildRefutedRequires(Variable constant, Procedure callee) {

-        return new RefutedAnnotation(constant, RefutedAnnotationKind.REQUIRES, callee);

+      public Implementation RefutationSite {

+        get { return this._refutationSite; }

+      }

+      public static RefutedAnnotation BuildRefutedRequires(Variable constant, Procedure callee, Implementation refutationSite) {

+        return new RefutedAnnotation(constant, RefutedAnnotationKind.REQUIRES, callee, refutationSite);

       }

-      public static RefutedAnnotation BuildRefutedEnsures(Variable constant) {

-        return new RefutedAnnotation(constant, RefutedAnnotationKind.ENSURES, null);

+      public static RefutedAnnotation BuildRefutedEnsures(Variable constant, Implementation refutationSite) {

+        return new RefutedAnnotation(constant, RefutedAnnotationKind.ENSURES, null, refutationSite);

       }

-      public static RefutedAnnotation BuildRefutedAssert(Variable constant) {

-        return new RefutedAnnotation(constant, RefutedAnnotationKind.ASSERT, null);

+      public static RefutedAnnotation BuildRefutedAssert(Variable constant, Implementation refutationSite) {

+        return new RefutedAnnotation(constant, RefutedAnnotationKind.ASSERT, null, refutationSite);

+      }

+

+      public override int GetHashCode()

+      {

+        unchecked {

+          int hash = 17;

+          hash = hash * 23 + this.Constant.GetHashCode();

+          hash = hash * 23 + this.Kind.GetHashCode();

+          if (this.CalleeProc != null)

+            hash = hash * 23 + this.CalleeProc.GetHashCode();

+          hash = hash * 23 + this.RefutationSite.GetHashCode();

+          return hash;

+        }

+      }

+

+      public override bool Equals(object obj) {

+        bool result = true;

+        var other = obj as RefutedAnnotation;

+

+        if (other == null) {

+          result = false;

+        } else {

+          result = result && String.Equals(other.Constant, this.Constant);

+          result = result && String.Equals(other.Kind, this.Kind);

+          if (other.CalleeProc != null && this.CalleeProc != null)

+            result = result && String.Equals(other.CalleeProc, this.CalleeProc);

+          result = result && String.Equals(other.RefutationSite, this.RefutationSite);

+        }

+

+        return result;

       }

     }

 

@@ -996,7 +1035,7 @@ namespace Microsoft.Boogie.Houdini {
       }

     }

 

-    private void DebugRefutedCandidates(Implementation curFunc, List<Counterexample> errors) {

+    protected void DebugRefutedCandidates(Implementation curFunc, List<Counterexample> errors) {

       XmlSink xmlRefuted = CommandLineOptions.Clo.XmlRefuted;

       if (xmlRefuted != null && errors != null) {

         DateTime start = DateTime.UtcNow;

@@ -1016,7 +1055,7 @@ namespace Microsoft.Boogie.Houdini {
       }

     }

 

-    private RefutedAnnotation ExtractRefutedAnnotation(Counterexample error) {

+    protected RefutedAnnotation ExtractRefutedAnnotation(Counterexample error) {

       Variable houdiniConstant;

       CallCounterexample callCounterexample = error as CallCounterexample;

       if (callCounterexample != null) {

@@ -1024,7 +1063,7 @@ namespace Microsoft.Boogie.Houdini {
         Requires failingRequires = callCounterexample.FailingRequires;

         if (MatchCandidate(failingRequires.Condition, out houdiniConstant)) {

           Contract.Assert(houdiniConstant != null);

-          return RefutedAnnotation.BuildRefutedRequires(houdiniConstant, failingProcedure);

+          return RefutedAnnotation.BuildRefutedRequires(houdiniConstant, failingProcedure, currentHoudiniState.Implementation);

         }

       }

       ReturnCounterexample returnCounterexample = error as ReturnCounterexample;

@@ -1032,7 +1071,7 @@ namespace Microsoft.Boogie.Houdini {
         Ensures failingEnsures = returnCounterexample.FailingEnsures;

         if (MatchCandidate(failingEnsures.Condition, out houdiniConstant)) {

           Contract.Assert(houdiniConstant != null);

-          return RefutedAnnotation.BuildRefutedEnsures(houdiniConstant);

+          return RefutedAnnotation.BuildRefutedEnsures(houdiniConstant, currentHoudiniState.Implementation);

         }

       }

       AssertCounterexample assertCounterexample = error as AssertCounterexample;

@@ -1040,14 +1079,14 @@ namespace Microsoft.Boogie.Houdini {
         AssertCmd failingAssert = assertCounterexample.FailingAssert;

         if (MatchCandidate(failingAssert.OrigExpr, out houdiniConstant)) {

           Contract.Assert(houdiniConstant != null);

-          return RefutedAnnotation.BuildRefutedAssert(houdiniConstant);

+          return RefutedAnnotation.BuildRefutedAssert(houdiniConstant, currentHoudiniState.Implementation);

         }

       }

 

       return null;

     }

 

-    private ProverInterface.Outcome TryCatchVerify(HoudiniSession session, int stage, IEnumerable<int> completedStages, out List<Counterexample> errors) {

+    protected virtual ProverInterface.Outcome TryCatchVerify(HoudiniSession session, int stage, IEnumerable<int> completedStages, out List<Counterexample> errors) {

       ProverInterface.Outcome outcome;

       try {

         outcome = session.Verify(proverInterface, GetAssignmentWithStages(stage, completedStages), out errors);

@@ -1060,7 +1099,7 @@ namespace Microsoft.Boogie.Houdini {
       return outcome;

     }

 

-    private Dictionary<Variable, bool> GetAssignmentWithStages(int currentStage, IEnumerable<int> completedStages)

+    protected Dictionary<Variable, bool> GetAssignmentWithStages(int currentStage, IEnumerable<int> completedStages)

     {

       Dictionary<Variable, bool> result = new Dictionary<Variable, bool>(currentHoudiniState.Assignment);

       foreach (var c in program.TopLevelDeclarations.OfType<Constant>())

@@ -1079,7 +1118,7 @@ namespace Microsoft.Boogie.Houdini {
       return result;

     }

 

-    private void HoudiniVerifyCurrent(HoudiniSession session, int stage, IEnumerable<int> completedStages) {

+    protected virtual void HoudiniVerifyCurrent(HoudiniSession session, int stage, IEnumerable<int> completedStages) {

       while (true) {

         this.NotifyAssignment(currentHoudiniState.Assignment);

 

diff --git a/Source/Houdini/Houdini.csproj b/Source/Houdini/Houdini.csproj
index 6c98c2a8..140d40aa 100644
--- a/Source/Houdini/Houdini.csproj
+++ b/Source/Houdini/Houdini.csproj
@@ -54,12 +54,18 @@
     <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>

     <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>

     <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>

-    <CodeContractsCustomRewriterAssembly />

-    <CodeContractsCustomRewriterClass />

-    <CodeContractsLibPaths />

-    <CodeContractsExtraRewriteOptions />

-    <CodeContractsExtraAnalysisOptions />

-    <CodeContractsBaseLineFile />

+    <CodeContractsCustomRewriterAssembly>

+    </CodeContractsCustomRewriterAssembly>

+    <CodeContractsCustomRewriterClass>

+    </CodeContractsCustomRewriterClass>

+    <CodeContractsLibPaths>

+    </CodeContractsLibPaths>

+    <CodeContractsExtraRewriteOptions>

+    </CodeContractsExtraRewriteOptions>

+    <CodeContractsExtraAnalysisOptions>

+    </CodeContractsExtraAnalysisOptions>

+    <CodeContractsBaseLineFile>

+    </CodeContractsBaseLineFile>

     <CodeContractsCacheAnalysisResults>False</CodeContractsCacheAnalysisResults>

     <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>

     <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>

@@ -85,6 +91,7 @@
     <Compile Include="CandidateDependenceAnalyser.cs" />

     <Compile Include="Houdini.cs" />

     <Compile Include="StagedHoudini.cs" />

+    <Compile Include="ConcurrentHoudini.cs" />

   </ItemGroup>

   <ItemGroup>

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

diff --git a/Source/Predication/UniformityAnalyser.cs b/Source/Predication/UniformityAnalyser.cs
index 040cb227..6119d522 100644
--- a/Source/Predication/UniformityAnalyser.cs
+++ b/Source/Predication/UniformityAnalyser.cs
@@ -234,14 +234,7 @@ namespace Microsoft.Boogie
                 }

 

                 foreach (Block b in Impl.Blocks) {

-                  foreach (Cmd c in b.Cmds) {

-                    CallCmd callCmd = c as CallCmd;

-                    if (callCmd != null) {

-                      if (IsUniform(callCmd.callee)) {

-                        SetNonUniform(callCmd.callee);

-                      }

-                    }

-                  }

+                  Analyse(Impl, b.Cmds, false);

                 }

                         

                 return;

@@ -254,12 +247,6 @@ namespace Microsoft.Boogie
             ctrlDep.TransitiveClosure();

 

             var nonUniformBlockSet = new HashSet<Block>();

-            /*// If procedure is non-uniform, so are all of its blocks

-            if (!uniformityInfo[Impl.Name].Key) {

-              foreach (var block in Impl.Blocks) {

-                nonUniformBlockSet.Add(block);

-              }

-            }*/

             nonUniformBlocks[Impl.Name] = nonUniformBlockSet;

 

             bool changed;

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 95662d84..b46e6fea 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -793,11 +793,11 @@ namespace Microsoft.Boogie.SMTLib
     }

 

     [NoDefaultContract]

-    public override Outcome CheckOutcome(ErrorHandler handler)

+    public override Outcome CheckOutcome(ErrorHandler handler, int taskID = -1)

     {

       Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

 

-      var result = CheckOutcomeCore(handler);

+      var result = CheckOutcomeCore(handler, taskID: taskID);

       SendThisVC("(pop 1)");

       FlushLogFile();

 

@@ -805,7 +805,7 @@ namespace Microsoft.Boogie.SMTLib
     }

 

     [NoDefaultContract]

-    public override Outcome CheckOutcomeCore(ErrorHandler handler)

+    public override Outcome CheckOutcomeCore(ErrorHandler handler, int taskID = -1)

     {  

       Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

       

@@ -819,6 +819,12 @@ namespace Microsoft.Boogie.SMTLib
         FlushProverWarnings();

 

         var errorsLeft = CommandLineOptions.Clo.ProverCCLimit;

+

+        if (CommandLineOptions.Clo.ConcurrentHoudini) {

+          Contract.Assert(taskID >= 0);

+          errorsLeft = CommandLineOptions.Clo.Cho[taskID].ProverCCLimit;

+        }

+

         if (errorsLeft < 1)

           errorsLeft = 1;

 

@@ -1314,7 +1320,7 @@ namespace Microsoft.Boogie.SMTLib
             i++;

         }

         Check();

-

+        

         var outcome = CheckOutcomeCore(handler);

 

         if (outcome != Outcome.Valid) {

diff --git a/Source/Provers/SMTLib/SMTLibProverOptions.cs b/Source/Provers/SMTLib/SMTLibProverOptions.cs
index 3f4ef5ac..0cfa65d8 100644
--- a/Source/Provers/SMTLib/SMTLibProverOptions.cs
+++ b/Source/Provers/SMTLib/SMTLibProverOptions.cs
@@ -87,15 +87,17 @@ namespace Microsoft.Boogie.SMTLib
       string SolverStr = null;

       if (ParseString(opt, "SOLVER", ref SolverStr)) {

         switch (SolverStr) {

+          case "Z3":

           case "z3":

             Solver = SolverKind.Z3;

             break;

+          case "CVC4":

           case "cvc4":

             Solver = SolverKind.CVC4;

-			if (Logic.Equals("")) Logic = "ALL_SUPPORTED";

+			      if (Logic.Equals("")) Logic = "ALL_SUPPORTED";

             break;

           default:

-            ReportError("Invalid SOLVER value; must be 'z3' or 'cvc4'");

+            ReportError("Invalid SOLVER value; must be 'Z3' or 'CVC4'");

             return false;

         }

         return true;

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index 2237c2fc..549c700a 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -378,7 +378,7 @@ namespace Microsoft.Boogie {
   // -----------------------------------------------------------------------------------------------

 

   public abstract class ProverInterface {

-    public static ProverInterface CreateProver(Program prog, string/*?*/ logFilePath, bool appendLogFile, int timeout) {

+    public static ProverInterface CreateProver(Program prog, string/*?*/ logFilePath, bool appendLogFile, int timeout, int taskID = -1) {

       Contract.Requires(prog != null);

 

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

@@ -393,7 +393,11 @@ namespace Microsoft.Boogie {
         options.TimeLimit = timeout * 1000;

       }

 

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

+      if (taskID >= 0) {

+        options.Parse(CommandLineOptions.Clo.Cho[taskID].ProverOptions);

+      } else {

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

+      }

 

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

 

@@ -492,7 +496,7 @@ namespace Microsoft.Boogie {
         throw new System.NotImplementedException();

     }

     [NoDefaultContract]

-    public abstract Outcome CheckOutcome(ErrorHandler handler);

+    public abstract Outcome CheckOutcome(ErrorHandler handler, int taskID = -1);

     public virtual string[] CalculatePath(int controlFlowConstant) {

       throw new System.NotImplementedException();

     }

@@ -560,7 +564,7 @@ namespace Microsoft.Boogie {
       throw new NotImplementedException();

     }

 

-    public virtual Outcome CheckOutcomeCore(ErrorHandler handler)

+    public virtual Outcome CheckOutcomeCore(ErrorHandler handler, int taskID = -1)

     {

         throw new NotImplementedException();

     }

@@ -619,7 +623,7 @@ namespace Microsoft.Boogie {
       throw new NotImplementedException();

     }

     [NoDefaultContract]

-    public override Outcome CheckOutcome(ErrorHandler handler) {

+    public override Outcome CheckOutcome(ErrorHandler handler, int taskID = -1) {

       //Contract.Requires(handler != null);

       Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

       throw new NotImplementedException();

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index ca5772ed..8fe4a5c6 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -1342,7 +1342,14 @@ namespace VC {
           }

         }

       }

-      IEnumerable sortedNodes = dag.TopologicalSort();

+

+      IEnumerable sortedNodes;

+      if (CommandLineOptions.Clo.ModifyTopologicalSorting) {

+        sortedNodes = dag.TopologicalSort(true);

+      } else {

+        sortedNodes = dag.TopologicalSort();

+      }

+

       Contract.Assert(sortedNodes != null);

       #endregion

 

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index bf3f267f..086dde15 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -1079,6 +1079,7 @@ namespace VC {
       private Outcome CheckVC() {

         prover.Check();

         ProverInterface.Outcome outcome = prover.CheckOutcomeCore(reporter);

+

         return ConditionGeneration.ProverInterfaceOutcomeToConditionGenerationOutcome(outcome);

       }

 

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index e9ca2fe6..2abe4a1b 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -2016,7 +2016,7 @@ namespace VC {
           }

       }

 

-    public void ConvertCFG2DAG(Implementation impl, Dictionary<Block,List<Block>> edgesCut = null)

+    public void ConvertCFG2DAG(Implementation impl, Dictionary<Block,List<Block>> edgesCut = null, int taskID = -1)

     {

     Contract.Requires(impl != null);

       impl.PruneUnreachableBlocks();  // This is needed for VCVariety.BlockNested, and is otherwise just an optimization

@@ -2081,11 +2081,32 @@ namespace VC {
           {

             if (a is AssertCmd) {

               Bpl.AssertCmd c = (AssertCmd) a;

-              Bpl.AssertCmd b = new Bpl.LoopInitAssertCmd(c.tok, c.Expr);

+              Bpl.AssertCmd b = null;

+

+              if (CommandLineOptions.Clo.ConcurrentHoudini) {

+                Contract.Assert(taskID >= 0);

+                if (CommandLineOptions.Clo.Cho[taskID].DisableLoopInvEntryAssert)

+                  b = new Bpl.LoopInitAssertCmd(c.tok, Expr.True);

+                else

+                  b = new Bpl.LoopInitAssertCmd(c.tok, c.Expr);

+              } else {

+                b = new Bpl.LoopInitAssertCmd(c.tok, c.Expr);

+              }

+

               b.Attributes = c.Attributes;

               b.ErrorData = c.ErrorData;

               prefixOfPredicateCmdsInit.Add(b);

-              b = new Bpl.LoopInvMaintainedAssertCmd(c.tok, c.Expr);

+

+              if (CommandLineOptions.Clo.ConcurrentHoudini) {

+                Contract.Assert(taskID >= 0);

+                if (CommandLineOptions.Clo.Cho[taskID].DisableLoopInvMaintainedAssert)

+                  b = new Bpl.LoopInvMaintainedAssertCmd(c.tok, Expr.True);

+                else

+                  b = new Bpl.LoopInvMaintainedAssertCmd(c.tok, c.Expr);

+              } else {

+                b = new Bpl.LoopInvMaintainedAssertCmd(c.tok, c.Expr);

+              }

+

               b.Attributes = c.Attributes; 

               b.ErrorData = c.ErrorData;

               prefixOfPredicateCmdsMaintained.Add(b);