17 files changed, 1590 insertions, 1821 deletions

diff --git a/Source/AbsInt/AbstractInterpretation.cs b/Source/AbsInt/AbstractInterpretation.cs
index e29a6d4a..698141bb 100644
--- a/Source/AbsInt/AbstractInterpretation.cs
+++ b/Source/AbsInt/AbstractInterpretation.cs
@@ -153,15 +153,6 @@ namespace Microsoft.Boogie.AbstractInterpretation {
       return this.lattice.Meet(atReturn, knownAtCallSite);

     }

 

-      /*

-    private Cci.IGraphNavigator callGraph;

-    public Cci.IGraphNavigator CallGraph {

-      get {

-        return this.callGraph;

-      }

-    }

-      */

-

     /// <summary>

     /// Compute the invariants for the program using the underlying abstract domain

     /// </summary>

diff --git a/Source/Boogie.sln b/Source/Boogie.sln
index 6b5723c8..e91b47c8 100644
--- a/Source/Boogie.sln
+++ b/Source/Boogie.sln
@@ -39,6 +39,8 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ParserHelper", "ParserHelpe
 EndProject

 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "TPTP", "Provers\TPTP\TPTP.csproj", "{A598ED5A-93AD-4125-A555-3921A2F936FA}"

 EndProject

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

+EndProject

 Global

 	GlobalSection(SolutionConfigurationPlatforms) = preSolution

 		Checked|.NET = Checked|.NET

@@ -495,6 +497,30 @@ Global
 		{A598ED5A-93AD-4125-A555-3921A2F936FA}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU

 		{A598ED5A-93AD-4125-A555-3921A2F936FA}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU

 		{A598ED5A-93AD-4125-A555-3921A2F936FA}.z3apidebug|x86.ActiveCfg = Release|Any CPU

+		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Checked|.NET.ActiveCfg = Release|Any CPU

+		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Checked|Any CPU.ActiveCfg = Release|Any CPU

+		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Checked|Any CPU.Build.0 = Release|Any CPU

+		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Checked|Mixed Platforms.ActiveCfg = Release|Any CPU

+		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Checked|Mixed Platforms.Build.0 = Release|Any CPU

+		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Checked|x86.ActiveCfg = Release|Any CPU

+		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Debug|.NET.ActiveCfg = Debug|Any CPU

+		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Debug|Any CPU.ActiveCfg = Debug|Any CPU

+		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Debug|Any CPU.Build.0 = Debug|Any CPU

+		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU

+		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU

+		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Debug|x86.ActiveCfg = Debug|Any CPU

+		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Release|.NET.ActiveCfg = Release|Any CPU

+		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Release|Any CPU.ActiveCfg = Release|Any CPU

+		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Release|Any CPU.Build.0 = Release|Any CPU

+		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU

+		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Release|Mixed Platforms.Build.0 = Release|Any CPU

+		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Release|x86.ActiveCfg = Release|Any CPU

+		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.z3apidebug|.NET.ActiveCfg = Release|Any CPU

+		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.z3apidebug|Any CPU.ActiveCfg = Release|Any CPU

+		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.z3apidebug|Any CPU.Build.0 = Release|Any CPU

+		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU

+		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU

+		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.z3apidebug|x86.ActiveCfg = Release|Any CPU

 	EndGlobalSection

 	GlobalSection(SolutionProperties) = preSolution

 		HideSolutionNode = FALSE

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index 88d8bdaa..82c864d5 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -429,6 +429,21 @@ namespace Microsoft.Boogie {
       // Abstract interpretation -> Always use (at least) intervals, if not specified otherwise (e.g. with the "/noinfer" switch)

       Microsoft.Boogie.AbstractInterpretation.AbstractInterpretation.RunAbstractInterpretation(program);

 

+      if (CommandLineOptions.Clo.ContractInfer) {

+        Houdini.Houdini houdini = new Houdini.Houdini(program, true);

+        Houdini.HoudiniOutcome outcome = houdini.PerformHoudiniInference();

+        Console.WriteLine("Assignment computed by Houdini:");

+        foreach (var x in outcome.assignment) {

+          Console.WriteLine(x.Key + " = " + x.Value);

+        }

+        errorCount = outcome.ErrorCount;

+        verified = outcome.Verified;

+        inconclusives = outcome.Inconclusives;

+        timeOuts = outcome.TimeOuts;

+        outOfMemories = 0;

+        return PipelineOutcome.Done;

+      }

+

       if (CommandLineOptions.Clo.LoopUnrollCount != -1) {

         program.UnrollLoops(CommandLineOptions.Clo.LoopUnrollCount);

       }

diff --git a/Source/BoogieDriver/BoogieDriver.csproj b/Source/BoogieDriver/BoogieDriver.csproj
index 95078433..52714dc9 100644
--- a/Source/BoogieDriver/BoogieDriver.csproj
+++ b/Source/BoogieDriver/BoogieDriver.csproj
@@ -172,6 +172,10 @@
       <Project>{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}</Project>

       <Name>Graph</Name>

     </ProjectReference>

+    <ProjectReference Include="..\Houdini\Houdini.csproj">

+      <Project>{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}</Project>

+      <Name>Houdini</Name>

+    </ProjectReference>

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

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

       <Name>ParserHelper</Name>

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 56116601..e1136150 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -299,7 +299,6 @@ namespace Microsoft.Boogie {
     public int VcsCores = 1;

     public bool VcsDumpSplits = false;

 

-    public bool houdiniEnabled = false;

     public bool DebugRefuted = false;

 

     public XmlSink XmlRefuted {

@@ -401,7 +400,6 @@ namespace Microsoft.Boogie {
       Contract.Invariant(cce.NonNullElements(methodsToTranslateMethodQualified, true));

       Contract.Invariant(cce.NonNullElements(methodsToTranslateSubstring, true));

       Contract.Invariant(Ai != null);

-      Contract.Invariant(houdiniFlags != null);

     }

 

     [Rep]

@@ -441,13 +439,6 @@ namespace Microsoft.Boogie {
     }

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

 

-    public class HoudiniFlags {

-      public bool continueAtError = false;

-      public bool incremental = false;

-    }

-

-    public HoudiniFlags/*!*/ houdiniFlags = new HoudiniFlags();

-

     [Verify(false)]

     private CommandLineOptions() {

       // this is just to suppress verification.

@@ -979,8 +970,6 @@ namespace Microsoft.Boogie {
           case "-contractInfer":

           case "/contractInfer":

             ContractInfer = true;

-            TheProverFactory = ProverFactory.Load("ContractInference");

-            ProverName = "ContractInference".ToUpper();

             break;

 

           case "-subsumption":

@@ -1367,28 +1356,6 @@ namespace Microsoft.Boogie {
             }

             break;

 

-          case "-Houdini":

-          case "/Houdini":

-            this.houdiniEnabled = true;

-            if (ps.hasColonArgument) {

-              if (ps.ConfirmArgumentCount(1)) {

-                foreach (char c in cce.NonNull(args[ps.i])) {

-                  switch (c) {

-                    case 'c':

-                      houdiniFlags.continueAtError = true;

-                      break;

-                    case 'i':

-                      houdiniFlags.incremental = true;

-                      break;

-                    default:

-                      ps.Error("Unknown houdini flag: " + c + "\n");

-                      break;

-                  }

-                }

-              }

-            }

-            break;

-

           case "-z3exe":

           case "/z3exe":

             if (ps.ConfirmArgumentCount(1)) {

@@ -2172,10 +2139,6 @@ namespace Microsoft.Boogie {
                          of every block

   /printInstrumented : print Boogie program after it has been

                    instrumented with invariants

-  /Houdini[:<flags>] : perform procedure Houdini

-                     c = continue when an error found

-                     i = use incremental queries

-  /dbgRefuted    : log refuted Houdini candidates to XmlSink

 

   ---- Debugging and general tracing options ---------------------------------

 

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 098dbad2..5e2bc911 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -3715,6 +3715,9 @@ namespace Microsoft.Dafny {
         return UsesSpecFeatures(e.Seq) ||

                (e.E0 != null && UsesSpecFeatures(e.E0)) ||

                (e.E1 != null && UsesSpecFeatures(e.E1));

+      } else if (expr is MultiSelectExpr) {

+        MultiSelectExpr e = (MultiSelectExpr)expr;

+        return UsesSpecFeatures(e.Array) || e.Indices.Exists(ee => UsesSpecFeatures(ee));

       } else if (expr is SeqUpdateExpr) {

         SeqUpdateExpr e = (SeqUpdateExpr)expr;

         return UsesSpecFeatures(e.Seq) ||

diff --git a/Source/Graph/Graph.cs b/Source/Graph/Graph.cs
index 99df97cd..21336545 100644
--- a/Source/Graph/Graph.cs
+++ b/Source/Graph/Graph.cs
@@ -344,7 +344,6 @@ namespace Graphing {
       Contract.Invariant(naturalLoops == null || Contract.ForAll(naturalLoops.Keys, p => p.Item2 != null && p.Item1 != null));

     }

 

-

     private class PreHeader {

       Node/*!*/ myHeader;

       [ContractInvariantMethod]

@@ -464,7 +463,7 @@ namespace Graphing {
       }

     }

 

-    internal IEnumerable<Node> Predecessors(Node n) {

+    public IEnumerable<Node> Predecessors(Node n) {

       // original A#

       //Set<Node> result = Set{ x : x in Nodes, Edge(x,n) };

 

@@ -472,7 +471,7 @@ namespace Graphing {
       return predCache[n];

     }

 

-    internal IEnumerable<Node> Successors(Node n) {

+    public IEnumerable<Node> Successors(Node n) {

       ComputePredSuccCaches();

       return succCache[n];

     }

diff --git a/Source/Houdini/AssemblyInfo.ssc b/Source/Houdini/AssemblyInfo.ssc
deleted file mode 100644
index 6ed99a25..00000000
--- a/Source/Houdini/AssemblyInfo.ssc
+++ /dev/null
@@ -1,4 +0,0 @@
-using System.Reflection;

-using System.Runtime.CompilerServices;

-

-[assembly: AssemblyKeyFile("..\\InterimKey.snk")]

diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs
new file mode 100644
index 00000000..437dbc98
--- /dev/null
+++ b/Source/Houdini/Checker.cs
@@ -0,0 +1,90 @@
+//-----------------------------------------------------------------------------

+//

+// Copyright (C) Microsoft Corporation.  All Rights Reserved.

+//

+//-----------------------------------------------------------------------------

+using System;

+using System.Diagnostics.Contracts;

+using System.Collections.Generic;

+using Microsoft.Boogie;

+using Microsoft.Boogie.VCExprAST;

+using Microsoft.Boogie.Simplify;

+using Microsoft.Boogie.Z3;

+using System.Collections;

+using System.IO;

+using System.Threading;

+using VC;

+

+namespace Microsoft.Boogie.Houdini {

+  public class HoudiniVCGen : VCGen {

+    private Checker checker;

+    private string descriptiveName;

+    private VCExpr conjecture;

+    private ProverInterface.ErrorHandler handler;

+    CounterexampleCollector collector;

+

+    public VCExpressionGenerator VCExprGenerator {

+      get {

+        return checker.VCExprGen;

+      }

+    }

+

+    public Boogie2VCExprTranslator BooogieExprTranslator {

+      get {

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

+        return proverContext.BoogieExprTranslator;

+      }

+    }

+

+    public HoudiniVCGen(Program program, Implementation impl, string logFilePath, bool appendLogFile) 

+    : base(program, logFilePath, appendLogFile) {

+      descriptiveName = impl.Name;

+      collector = new CounterexampleCollector();

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

+      if (CommandLineOptions.Clo.SoundnessSmokeTest) {

+        throw new Exception("HoudiniVCGen does not support Soundness smoke test.");

+      }

+

+      ConvertCFG2DAG(impl, program);

+      ModelViewInfo mvInfo;

+      Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = PassifyImpl(impl, program, out mvInfo);

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

+      checker = new Checker(this, program, logFilePath, appendLogFile, impl, CommandLineOptions.Clo.ProverKillTime);

+      if (!(checker.TheoremProver is Z3ProcessTheoremProver)) {

+        throw new Exception("HdnChecker only works with z3");

+      }

+      conjecture = GenerateVC(impl, null, out label2absy, checker);

+

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

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

+      }

+      else {

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

+      }

+    }

+

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

+      collector.examples.Clear();

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

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

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

+

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

+      if (proverOutcome == ProverInterface.Outcome.Invalid) {

+        Contract.Assume(collector.examples != null);

+        if (collector.examples.Count == 0) {

+          string memStr = System.Convert.ToString(System.GC.GetTotalMemory(false));

+          if (memStr != null)

+            memStr = "?";

+          throw new UnexpectedProverOutputException("Outcome.Errors w/ 0 counter examples. " + memStr + " memory used");

+        }

+        errors = collector.examples;

+      }

+      else {

+        errors = null;

+      }

+      return proverOutcome;

+    }

+

+  }

+}
\ No newline at end of file
diff --git a/Source/Houdini/Checker.ssc b/Source/Houdini/Checker.ssc
deleted file mode 100644
index 03c2beda..00000000
--- a/Source/Houdini/Checker.ssc
+++ /dev/null
@@ -1,460 +0,0 @@
-//-----------------------------------------------------------------------------

-//

-// Copyright (C) Microsoft Corporation.  All Rights Reserved.

-//

-//-----------------------------------------------------------------------------

-using System;

-using Microsoft.Contracts;

-using System.Collections.Generic;

-using Microsoft.Boogie;

-using Microsoft.Boogie.Simplify.AST;

-using VC;

-using Microsoft.Boogie.Z3;

-using Microsoft.AbstractInterpretationFramework;

-using Microsoft.Boogie.AbstractInterpretation;

-using System.Collections;

-using System.Compiler;

-using System.IO;

-using System.Threading;

-

-namespace Microsoft.Boogie.Houdini {

-

-  public abstract class HdnCheckerFactory {

-    public static HdnChecker! BuildHdnChecker(Checker! checker) {

-      if (checker.TheoremProver is Z3ThreadTheoremProver)

-        return new HoudiniZ3ApiChecker(checker);

-      else if (checker.TheoremProver is Z3ProcessTheoremProver) {

-        if (CommandLineOptions.Clo.houdiniFlags.incremental) {

-          return new HoudiniZ3CheckerIncr(checker);

-        } else {

-          return new HoudiniZ3Checker(checker);

-        }        

-      } else

-        throw new Exception("HdnChecker only works with z3");

-    }

-  }

-

-  public abstract class HdnChecker {

-    public abstract void PrepareCheck(string! _descriptiveName, 

-        VCExpr! _vc, ProverInterface.ErrorHandler! _handler);

-    public abstract void PushAxiom(VCExpr! vc);

-    public abstract void Pop();

-    public abstract void Check();

-    public abstract ProverInterface.Outcome ReadOutcome()

-      throws UnexpectedProverOutputException;

-  }

-  

-  public class HoudiniZ3ApiChecker:HdnChecker {

-

-    private Z3ThreadTheoremProver! z3prover;

-    

-    private ProverInterface.ErrorHandler handler;

-    private ProverInterface.Outcome outcome;

-    private UnexpectedProverOutputException outputExn;

-

-    internal HoudiniZ3ApiChecker(Checker! checker)

-    requires checker.TheoremProver!=null;

-    requires checker.TheoremProver is Z3ThreadTheoremProver;

-    {

-      this.z3prover = (Z3ThreadTheoremProver)checker.TheoremProver;

-    }

-

-    public override void PrepareCheck(string! _descriptiveName, VCExpr! _vc, ProverInterface.ErrorHandler! _handler) {

-      handler = _handler;

-      z3prover.LogComment(_descriptiveName);

-      z3prover.PrepareCheck(_descriptiveName,_vc);

-    }

-    

-    public override void PushAxiom(VCExpr! vc) {

-      z3prover.PushAxiom(vc);

-    }

-    

-    public override void Pop() {

-      z3prover.Pop();

-    }

-    

-    public override void Check() {

-      z3prover.BeginPreparedCheck();

-      try {

-        outcome = z3prover.CheckOutcome((!)handler);

-      } catch (UnexpectedProverOutputException e) {

-        outputExn = e;

-      }

-    }

-

-    public override ProverInterface.Outcome ReadOutcome()

-      throws UnexpectedProverOutputException;

-    {

-      if (outputExn != null) {

-        throw outputExn;

-      }

-      return outcome;

-    }

-  }

-  

-  // version of Z3PTP exposing more of the prover process functionality

-  public class Z3ProcessTPExposed : Z3ProcessTheoremProver { 

-    

-    [NotDelayed]

-    public Z3ProcessTPExposed (TextWriter/*?*/ logFileWriter, VCExpressionGenerator! gen, DeclFreeProverContext! ctx, int timeout, bool typed)

-      throws UnexpectedProverOutputException;

-    {

-      base(logFileWriter, gen, ctx, timeout, typed, "z3.exe");

-    }

-    

-    

-    //MOVED Directly Z3 ProverInterface for now...

-    //To introduce this cleanly, need to add a new subproject under Provers

-    //and must use the commandline option for that, instead of saying /prover:z3

-    //That way, the class is constructed in class Checker the same way

-    //all the other provers are constructed

-  

-  }

-  

-  public class Z3ExposedFactory : Z3.Factory {

-

-  }

-  

-  

-  //Old version

-  public class HoudiniZ3Checker:HdnChecker {

-    private Stack<VCExpr!>! axioms = new Stack<VCExpr!>();

-    private Checker! checker;

-    private string descriptiveName;

-    private VCExpr conjecture;

-    private ProverInterface.ErrorHandler handler;

-        

-    internal HoudiniZ3Checker(Checker! checker) 

-    requires checker.TheoremProver!=null;

-    requires checker.TheoremProver is Z3ProcessTheoremProver;

-    {

-      this.checker = checker;

-    }

-    

-    public override void PrepareCheck(string! _descriptiveName, VCExpr! _vc, ProverInterface.ErrorHandler! _handler) 

-    {

-      this.descriptiveName = _descriptiveName;

-      this.conjecture = _vc;

-      this.handler = _handler;

-    }

-    public override void PushAxiom(VCExpr! vc) {

-      axioms.Push(vc);

-    }

-    public override void Pop() {

-      axioms.Pop();

-    }    

-    private VCExpr! BuildVCAxioms(Stack<VCExpr!>! axioms) 

-    requires axioms.Count>0;

-    {

-      VCExpr vc_axioms = null;

-      foreach (VCExpr! axiom in axioms) {

-        if (vc_axioms==null)

-          vc_axioms=axiom;

-        else

-          vc_axioms = checker.VCExprGen.And(vc_axioms,axiom);

-      }

-      return (!)vc_axioms;

-    }

-    

-    public override void Check() 

-    {

-      assert (descriptiveName!=null);

-      assert (conjecture!=null);

-      assert (handler!=null);

-      outcome = ProverInterface.Outcome.Undetermined;

-      

-      VCExpr! vc;

-      if (axioms.Count>0) {

-        VCExpr vc_axioms = BuildVCAxioms(axioms);

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

-      } else        

-        vc = conjecture;

-

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

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

-    }

-   

-    private ProverInterface.Outcome outcome;

-    private UnexpectedProverOutputException outputExn;

-

-    public override ProverInterface.Outcome ReadOutcome()

-      throws UnexpectedProverOutputException;

-    {

-      try {

-        outcome = checker.ReadOutcome();

-      } catch (UnexpectedProverOutputException e) {

-        throw e;

-      }

-      return outcome;

-    }

-  }

-

-  //new version

-  public class HoudiniZ3CheckerIncr:HdnChecker {

-    private Checker! checker;

-    private string descriptiveName;

-    private VCExpr conjecture;

-    private ProverInterface.ErrorHandler handler;

-    

-    // Hack to delay the exception throwing (from Push/Pop...) for now

-    private UnexpectedProverOutputException delayedExc;

-    private Z3ProcessTheoremProver! thmProver;

-    

-    internal HoudiniZ3CheckerIncr(Checker! checker) 

-    requires checker.TheoremProver!=null;

-    requires checker.TheoremProver is Z3ProcessTheoremProver;

-    {

-      this.checker = checker;

-      this.thmProver = (Z3ProcessTheoremProver!)checker.TheoremProver;

-    }

-    

-    private void delayException(UnexpectedProverOutputException exc) {  

-         if (delayedExc == null) { delayedExc = exc; }

-    }

-    

-    public override void PrepareCheck(string! _descriptiveName, VCExpr! _vc, 

-        ProverInterface.ErrorHandler! _handler) 

-    {

-      this.descriptiveName = _descriptiveName;

-      this.conjecture = _vc;

-      this.handler = _handler;

-      this.thmProver.LogComment(_descriptiveName);

-      try {

-         this.thmProver.PrepareCheck(_descriptiveName,_vc);

-      } catch (UnexpectedProverOutputException exc) {

-         delayException(exc);

-      }

-    }

-    public override void PushAxiom(VCExpr! vc) {

-      string! vcStr = vc.ToString();

-      try {

-         thmProver.PushAxioms(vcStr);

-      } catch (UnexpectedProverOutputException exc) {

-         delayException(exc);

-      }

-    }

-    public override void Pop() {

-      try {

-         thmProver.PopAxioms();

-      } catch (UnexpectedProverOutputException exc) {

-         delayException(exc);

-      }

-    }    

-    

-    public override void Check()

-    {

-      assert (descriptiveName!=null);

-      assert (conjecture!=null);

-      assert (handler!=null);

-      outcome = ProverInterface.Outcome.Undetermined;

-      

-      VCExpr! vc = checker.VCExprGen.False;

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

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

-    }

-   

-    private ProverInterface.Outcome outcome;

-    private UnexpectedProverOutputException outputExn;

-

-    public override ProverInterface.Outcome ReadOutcome()

-      throws UnexpectedProverOutputException;

-    {

-      // HACK

-      if (delayedExc != null) {

-        UnexpectedProverOutputException temp = delayedExc;

-        delayedExc = null;

-        throw temp;

-      }

-      // Normal stuff

-      try {

-        outcome = checker.ReadOutcome();

-      } catch (UnexpectedProverOutputException e) {

-        throw e;

-      }

-      return outcome;

-    }

-  }

-  

-  public abstract class HdnVCGenFactory {

-    public abstract HdnVCGen! BuildVCGen(Program! program, string logFilePath, bool appendLogFile);

-  }

-  public class Z3APIHdnVCGenFactory:HdnVCGenFactory {

-    public override HdnVCGen! BuildVCGen(Program! program, string logFilePath, bool appendLogFile) {

-      return new Z3ApiHdnVCGen(program, logFilePath, appendLogFile);

-    }

-  }

-  public class Z3HdnVCGenFactory:HdnVCGenFactory {

-    public override HdnVCGen! BuildVCGen(Program! program, string logFilePath, bool appendLogFile) {

-      return new Z3HdnVCGen(program, logFilePath, appendLogFile);

-    }

-  }

-  

-  public abstract class HdnVCGen {

-    public abstract void PrepareVerification(Implementation! impl, Program! program);

-    public abstract void PushAxiom(Axiom! axiom);

-    public abstract void Pop();

-    public abstract VC.VCGen.Outcome Verify(out List<Counterexample!>? errors)       

-      throws UnexpectedProverOutputException;

-      

-  }

-  

-  public class Z3HdnVCGen: HdnVCGen {

-    private Program! program;

-    private string logFilePath;

-    private bool appendLogFile;

-    private Implementation implementation;

-    private Axiom axiom;

-    

-    private ExtVCGen vcgen;

-    

-    public Z3HdnVCGen(Program! program, string logFilePath, bool appendLogFile) {

-      this.program = program;

-      this.logFilePath = logFilePath;

-      this.appendLogFile= appendLogFile;

-    }

-

-	public override void PrepareVerification(Implementation! impl, Program! program) {	  

-	  this.implementation = impl;

-	  this.program = program;

-      this.vcgen = new ExtVCGen(program,logFilePath,appendLogFile);

-      this.vcgen.PrepareVerification(this.implementation,this.program); 

-      //watch out for > 1 call -- don't want CFG conversion to happen too many times!!!

-    }

-        

-    public override  void PushAxiom(Axiom! axiom) {

-      assert this.vcgen != null;

-      this.axiom=axiom;

-      this.vcgen.PushAxiom(this.axiom);

-    }

-    

-    public override void Pop() {

-      assert this.vcgen != null;

-      this.vcgen.Pop();

-      this.axiom = null;

-    }

-    

-    public override VC.VCGen.Outcome Verify(out List<Counterexample!>? errors)       

-      throws UnexpectedProverOutputException; {

-      assert(this.vcgen!=null);

-      

-      return vcgen.Verify(out errors);

-    }

-  

-  }

-  

-  public class Z3ApiHdnVCGen: HdnVCGen {

-    private ExtVCGen! vcgen;

-    

-    public Z3ApiHdnVCGen(Program! program, string logFilePath, bool appendLogFile) {

-      this.vcgen = new ExtVCGen(program,logFilePath,appendLogFile);

-    }

-    

-    public override void PrepareVerification(Implementation! impl, Program! program) {

-      vcgen.PrepareVerification(impl,program);

-    }

-    

-    public override  void PushAxiom(Axiom! axiom) {

-      vcgen.PushAxiom(axiom);

-    }

-    

-    public override void Pop() {

-      vcgen.Pop();

-    }

-    

-    public override VC.VCGen.Outcome Verify(out List<Counterexample!>? errors)       

-      throws UnexpectedProverOutputException; {

-      return vcgen.Verify(out errors);

-    }

-      

-  }

-  

-  

-  

-  public class ExtVCGen : VCGen {

-    

-    private HdnChecker hdnChecker;

-    private VCExpressionGenerator gen;

-    CounterexampleCollector! collector = new CounterexampleCollector();

-    

-    public ExtVCGen(Program! program, string logFilePath, bool appendLogFile) {

-      base(program,logFilePath,appendLogFile);

-    }

-    

-    public void PrepareVerification(Implementation! impl, Program! program) {

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

-      if (CommandLineOptions.Clo.SoundnessSmokeTest) {

-        throw new Exception("HoudiniVCGen does not support Soundness smoke test.");

-      }

-      

-      ConvertCFG2DAG(impl, program);

-      Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = PassifyImpl(impl, program);

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

-      Checker! checker = new Checker(program, this.logFilePath, this.appendLogFile, impl, CommandLineOptions.Clo.ProverKillTime); 

-      VCExpr! vc = GenerateVC(impl, out label2absy, checker);

-              

-      ErrorReporter reporter;

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

-        reporter = new ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, incarnationOriginMap, collector);

-      } else {

-        reporter = new ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, incarnationOriginMap, collector);

-      }

-      this.gen = checker.VCExprGen;

-      this.hdnChecker = HdnCheckerFactory.BuildHdnChecker(checker);

-      this.hdnChecker.PrepareCheck((!) impl.Name, vc, reporter);

-    }

-    

-    

-    public void PushAxiom(Axiom! axiom) 

-    {

-      assume (hdnChecker!=null);

-      assume (gen!=null);

-      VCExpr vc = axiom.Expr.VCView(gen);

-      this.hdnChecker.PushAxiom(vc);

-    }

-    public void Pop() {

-      assume (hdnChecker!=null);

-      hdnChecker.Pop();

-    }

-    

-    public Outcome Verify(out List<Counterexample!>? errors)       

-    throws UnexpectedProverOutputException; {

-      assume (hdnChecker!=null);

-      collector.examples.Clear();

-      hdnChecker.Check();

-      ProverInterface.Outcome proverOutcome;

-      proverOutcome = hdnChecker.ReadOutcome();

-      Outcome verifyOutcome = ReadOutcome(proverOutcome);

-      if (verifyOutcome == Outcome.Errors) {

-        assume (collector.examples!=null);

-        if (collector.examples.Count == 0) {

-            string memStr = System.Convert.ToString(System.GC.GetTotalMemory(false));

-            if (memStr != null)

-                memStr = "?";

-            throw new UnexpectedProverOutputException("Outcome.Errors w/ 0 counter examples. " + memStr + " memory used");

-        }

-        errors = collector.examples;

-      } else {

-        errors = null;

-      }

-      return verifyOutcome;

-    }

-

-    private Outcome ReadOutcome(ProverInterface.Outcome proverOutcome) {

-      switch (proverOutcome) {

-          case ProverInterface.Outcome.Valid:

-            return Outcome.Correct;

-          case ProverInterface.Outcome.Invalid:

-            return Outcome.Errors;

-          case ProverInterface.Outcome.TimeOut:

-            return Outcome.TimedOut;

-          case ProverInterface.Outcome.Undetermined:

-            return Outcome.Inconclusive;

-          default:

-            throw new Exception("Unknown Prover Interface outcome while reading outcome.");

-        }

-    }

-

-  }

-  

-  

-}
\ No newline at end of file
diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
new file mode 100644
index 00000000..714ecd3b
--- /dev/null
+++ b/Source/Houdini/Houdini.cs
@@ -0,0 +1,1139 @@
+//-----------------------------------------------------------------------------

+//

+// Copyright (C) Microsoft Corporation.  All Rights Reserved.

+//

+//-----------------------------------------------------------------------------

+using System;

+using System.Diagnostics.Contracts;

+using System.Collections.Generic;

+using Microsoft.Boogie;

+using Microsoft.Boogie.VCExprAST;

+using Microsoft.Boogie.Simplify;

+using VC;

+using Microsoft.Boogie.Z3;

+using System.Collections;

+using System.IO;

+using Microsoft.AbstractInterpretationFramework;

+using Graphing;

+

+namespace Microsoft.Boogie.Houdini {

+

+  class ReadOnlyDictionary<K, V> {

+    private Dictionary<K, V> dictionary;

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

+      this.dictionary = dictionary;

+    }

+

+    public Dictionary<K, V>.KeyCollection Keys {

+      get { return this.dictionary.Keys; }

+    }

+

+    public bool TryGetValue(K k, out V v) {

+      return this.dictionary.TryGetValue(k, out v);

+    }

+

+    public bool ContainsKey(K k) {

+      return this.dictionary.ContainsKey(k);

+    }

+  }

+

+  public abstract class HoudiniObserver {

+    public virtual void UpdateStart(Program program, int numConstants) { }

+    public virtual void UpdateIteration() { }

+    public virtual void UpdateImplementation(Implementation implementation) { }

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

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

+    public virtual void UpdateEnqueue(Implementation implementation) { }

+    public virtual void UpdateDequeue() { }

+    public virtual void UpdateConstant(string constantName) { }

+    public virtual void UpdateEnd(bool isNormalEnd) { }

+    public virtual void UpdateFlushStart() { }

+    public virtual void UpdateFlushFinish() { }

+    public virtual void SeeException(string msg) { }

+  }

+

+  public class IterationTimer<K> {

+    private Dictionary<K, List<double>> times;

+

+    public IterationTimer() {

+      times = new Dictionary<K, List<double>>();

+    }

+

+    public void AddTime(K key, double timeMS) {

+      List<double> oldList;

+      times.TryGetValue(key, out oldList);

+      if (oldList == null) {

+        oldList = new List<double>();

+      }

+      else {

+        times.Remove(key);

+      }

+      oldList.Add(timeMS);

+      times.Add(key, oldList);

+    }

+

+    public void PrintTimes(TextWriter wr) {

+      wr.WriteLine("Total procedures: {0}", times.Count);

+      double total = 0;

+      int totalIters = 0;

+      foreach (KeyValuePair<K, List<double>> kv in times) {

+        int curIter = 0;

+        wr.WriteLine("Times for {0}:", kv.Key);

+        foreach (double v in kv.Value) {

+          wr.WriteLine("  ({0})\t{1}ms", curIter, v);

+          total += v;

+          curIter++;

+        }

+        totalIters += curIter;

+      }

+      total = total / 1000.0;

+      wr.WriteLine("Total time: {0} (s)", total);

+      wr.WriteLine("Avg: {0} (s/iter)", total / totalIters);

+    }

+  }

+

+  public class HoudiniTimer : HoudiniObserver {

+    private DateTime startT;

+    private Implementation curImp;

+    private IterationTimer<string> times;

+    private TextWriter wr;

+

+    public HoudiniTimer(TextWriter wr) {

+      this.wr = wr;

+      times = new IterationTimer<string>();

+    }

+    public override void UpdateIteration() {

+      startT = DateTime.Now;

+    }

+    public override void UpdateImplementation(Implementation implementation) {

+      curImp = implementation;

+    }

+    public override void UpdateOutcome(ProverInterface.Outcome o) {

+      Contract.Assert(curImp != null);

+      DateTime endT = DateTime.Now;

+      times.AddTime(curImp.Name, (endT - startT).TotalMilliseconds); // assuming names are unique

+    }

+    public void PrintTimes() {

+      wr.WriteLine("-----------------------------------------");

+      wr.WriteLine("Times for each iteration for each procedure");

+      wr.WriteLine("-----------------------------------------");

+      times.PrintTimes(wr);

+    }

+  }

+

+  public class HoudiniTextReporter : HoudiniObserver {

+    private TextWriter wr;

+    private int currentIteration = -1;

+

+    public HoudiniTextReporter(TextWriter wr) {

+      this.wr = wr;

+    }

+    public override void UpdateStart(Program program, int numConstants) {

+      wr.WriteLine("Houdini started:" + program.ToString() + " #constants: " + numConstants.ToString());

+      currentIteration = -1;

+      wr.Flush();

+    }

+    public override void UpdateIteration() {

+      currentIteration++;

+      wr.WriteLine("---------------------------------------");

+      wr.WriteLine("Houdini iteration #" + currentIteration);

+      wr.Flush();

+    }

+    public override void UpdateImplementation(Implementation implementation) {

+      wr.WriteLine("implementation under analysis :" + implementation.Name);

+      wr.Flush();

+    }

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

+      bool firstTime = true;

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

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

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

+        string valString; // ugliness to get it lower cased

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

+        wr.Write(kv.Key + " == " + valString);

+      }

+      wr.WriteLine(");");

+      wr.Flush();

+    }

+    public override void UpdateOutcome(ProverInterface.Outcome outcome) {

+      wr.WriteLine("analysis outcome :" + outcome);

+      wr.Flush();

+    }

+    public override void UpdateEnqueue(Implementation implementation) {

+      wr.WriteLine("worklist enqueue :" + implementation.Name);

+      wr.Flush();

+    }

+    public override void UpdateDequeue() {

+      wr.WriteLine("worklist dequeue");

+      wr.Flush();

+    }

+    public override void UpdateConstant(string constantName) {

+      wr.WriteLine("constant disabled : " + constantName);

+      wr.Flush();

+    }

+    public override void UpdateEnd(bool isNormalEnd) {

+      wr.WriteLine("Houdini ended: " + (isNormalEnd ? "Normal" : "Abnormal"));

+      wr.WriteLine("Number of iterations: " + (this.currentIteration + 1));

+      wr.Flush();

+    }

+    public override void UpdateFlushStart() {

+      wr.WriteLine("***************************************");

+      wr.WriteLine("Flushing remaining implementations");

+      wr.Flush();

+    }

+    public override void UpdateFlushFinish() {

+      wr.WriteLine("***************************************");

+      wr.WriteLine("Flushing finished");

+      wr.Flush();

+    }

+    public override void SeeException(string msg) {

+      wr.WriteLine("Caught exception: " + msg);

+      wr.Flush();

+    }

+

+  }

+

+

+  public abstract class ObservableHoudini {

+    private List<HoudiniObserver> observers = new List<HoudiniObserver>();

+

+    public void AddObserver(HoudiniObserver observer) {

+      if (!observers.Contains(observer))

+        observers.Add(observer);

+    }

+    private delegate void NotifyDelegate(HoudiniObserver observer);

+

+    private void Notify(NotifyDelegate notifyDelegate) {

+      foreach (HoudiniObserver observer in observers) {

+        notifyDelegate(observer);

+      }

+    }

+    protected void NotifyStart(Program program, int numConstants) {

+      NotifyDelegate notifyDelegate = (NotifyDelegate)delegate(HoudiniObserver r) { r.UpdateStart(program, numConstants); };

+      Notify(notifyDelegate);

+    }

+    protected void NotifyIteration() {

+      Notify((NotifyDelegate)delegate(HoudiniObserver r) { r.UpdateIteration(); });

+    }

+    protected void NotifyImplementation(Implementation implementation) {

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

+    }

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

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

+    }

+    protected void NotifyOutcome(ProverInterface.Outcome outcome) {

+      Notify((NotifyDelegate)delegate(HoudiniObserver r) { r.UpdateOutcome(outcome); });

+    }

+    protected void NotifyEnqueue(Implementation implementation) {

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

+    }

+    protected void NotifyDequeue() {

+      Notify((NotifyDelegate)delegate(HoudiniObserver r) { r.UpdateDequeue(); });

+    }

+    protected void NotifyConstant(string constantName) {

+      Notify((NotifyDelegate)delegate(HoudiniObserver r) { r.UpdateConstant(constantName); });

+    }

+    protected void NotifyEnd(bool isNormalEnd) {

+      Notify((NotifyDelegate)delegate(HoudiniObserver r) { r.UpdateEnd(isNormalEnd); });

+    }

+    protected void NotifyFlushStart() {

+      Notify((NotifyDelegate)delegate(HoudiniObserver r) { r.UpdateFlushStart(); });

+    }

+    protected void NotifyFlushFinish() {

+      Notify((NotifyDelegate)delegate(HoudiniObserver r) { r.UpdateFlushFinish(); });

+    }

+

+    protected void NotifyException(string msg) {

+      Notify((NotifyDelegate)delegate(HoudiniObserver r) { r.SeeException(msg); });

+    }

+  }

+

+  public class Houdini : ObservableHoudini {

+    private Program program;

+    private ReadOnlyDictionary<string, IdentifierExpr> houdiniConstants;

+    private ReadOnlyDictionary<Implementation, HoudiniVCGen> vcgenSessions;

+    private Graph<Implementation> callGraph;

+    private bool continueAtError;

+

+    public Houdini(Program program, bool continueAtError) {

+      this.program = program;

+      this.callGraph = BuildCallGraph();

+      this.continueAtError = continueAtError;

+      this.houdiniConstants = CollectExistentialConstants();

+      this.vcgenSessions = PrepareVCGenSessions();

+    }

+

+    private ReadOnlyDictionary<Implementation, HoudiniVCGen> PrepareVCGenSessions() {

+      HashSet<Implementation> impls = new HashSet<Implementation>();

+      Dictionary<Implementation, HoudiniVCGen> vcgenSessions = new Dictionary<Implementation, HoudiniVCGen>();

+      foreach (Declaration decl in program.TopLevelDeclarations) {

+        Implementation impl = decl as Implementation;

+        if (impl != null) {

+          impls.Add(impl);

+        }

+      }

+      foreach (Implementation impl in impls) {

+        // make a different simplify log file for each function

+        String simplifyLog = null;

+        if (CommandLineOptions.Clo.SimplifyLogFilePath != null) {

+          simplifyLog = impl.ToString() + CommandLineOptions.Clo.SimplifyLogFilePath;

+        }

+        HoudiniVCGen vcgen = new HoudiniVCGen(program, impl, simplifyLog, CommandLineOptions.Clo.SimplifyLogFileAppend);

+        vcgenSessions.Add(impl, vcgen);

+      }

+      return new ReadOnlyDictionary<Implementation, HoudiniVCGen>(vcgenSessions);

+    }

+

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

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

+      foreach (Declaration decl in program.TopLevelDeclarations) {

+        Constant constant = decl as Constant;

+        if (constant != null) {

+          bool result = false;

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

+            if (result == true)

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

+          }

+        }

+      }

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

+    }

+

+    private Graph<Implementation> BuildCallGraph() {

+      Graph<Implementation> callGraph = new Graph<Implementation>();

+      Dictionary<Procedure, HashSet<Implementation>> procToImpls = new Dictionary<Procedure, HashSet<Implementation>>();

+      foreach (Declaration decl in program.TopLevelDeclarations) {

+        Procedure proc = decl as Procedure;

+        if (proc == null) continue;

+        procToImpls[proc] = new HashSet<Implementation>();

+      } 

+      foreach (Declaration decl in program.TopLevelDeclarations) {

+        Implementation impl = decl as Implementation;

+        if (impl == null) continue;

+        callGraph.AddSource(impl);

+        procToImpls[impl.Proc].Add(impl);

+      }

+      foreach (Declaration decl in program.TopLevelDeclarations) {

+        Implementation impl = decl as Implementation;

+        if (impl == null) continue;

+        foreach (Block b in impl.Blocks) {

+          foreach (Cmd c in b.Cmds) {

+            CallCmd cc = c as CallCmd;

+            if (cc == null) continue;

+            foreach (Implementation callee in procToImpls[cc.Proc]) {

+              callGraph.AddEdge(impl, callee);

+            }

+          }

+        }

+      }

+      return callGraph;

+    }

+

+    private Queue<Implementation> BuildWorkList(Program program) {

+      Queue<Implementation> queue = new Queue<Implementation>();

+      foreach (Declaration decl in program.TopLevelDeclarations) {

+        Implementation impl = decl as Implementation;

+        if (impl != null) {

+          queue.Enqueue(impl);

+        }

+      }

+      return queue;

+    }

+

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

+      candidateConstant = null;

+      IExpr antecedent;

+      IExpr expr = boogieExpr as IExpr;

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

+        IdentifierExpr.ConstantFunApp constantFunApp = antecedent as IdentifierExpr.ConstantFunApp;

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

+          candidateConstant = constantFunApp.IdentifierExpr.Name;

+          return true;

+        }

+      }

+      return false;

+    }

+

+    private VCExpr BuildAxiom(HoudiniVCGen vcgen, Dictionary<string, bool> currentAssignment) {

+      Boogie2VCExprTranslator exprTranslator = vcgen.BooogieExprTranslator;

+      VCExpressionGenerator exprGen = vcgen.VCExprGenerator;

+

+      VCExpr expr = VCExpressionGenerator.True;

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

+        IdentifierExpr constantExpr;

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

+        Contract.Assume(constantExpr != null);

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

+        if (kv.Value) {

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

+        }

+        else {

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

+        }

+      }

+      return expr;

+    }

+

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

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

+      foreach (string constant in constants)

+        initial.Add(constant, true);

+      return initial;

+    }

+

+    private ProverInterface.Outcome VerifyUsingAxiom(Implementation implementation, VCExpr axiom, out List<Counterexample> errors) {

+      HoudiniVCGen vcgen;

+      vcgenSessions.TryGetValue(implementation, out vcgen);

+      if (vcgen == null)

+        throw new Exception("HdnVCGen not found for implementation: " + implementation.Name);

+      ProverInterface.Outcome outcome = TryCatchVerify(vcgen, axiom, out errors);

+      return outcome;

+    }

+

+    // the main procedure that checks a procedure and updates the

+    // assignment and the worklist

+    private ProverInterface.Outcome HoudiniVerifyCurrent(HoudiniState current,

+                                        Program program,

+                                        out List<Counterexample> errors,

+                                        out bool exc) {

+      HoudiniVCGen vcgen;

+      if (current.Implementation == null)

+        throw new Exception("HoudiniVerifyCurrent has null implementation");

+

+      Implementation implementation = current.Implementation;

+      vcgenSessions.TryGetValue(implementation, out vcgen);

+      if (vcgen == null)

+        throw new Exception("HdnVCGen not found for implementation: " + implementation.Name);

+

+      ProverInterface.Outcome outcome = HoudiniVerifyCurrentAux(current, program, vcgen, out errors, out exc);

+      return outcome;

+    }

+

+    private ProverInterface.Outcome VerifyCurrent(HoudiniState current,

+                                        Program program,

+                                        out List<Counterexample> errors,

+                                        out bool exc) {

+      HoudiniVCGen vcgen;

+      if (current.Implementation != null) {

+        Implementation implementation = current.Implementation;

+        vcgenSessions.TryGetValue(implementation, out vcgen);

+        if (vcgen == null)

+          throw new Exception("HdnVCGen not found for implementation: " + implementation.Name);

+

+        ProverInterface.Outcome outcome = TrySpinSameFunc(current, program, vcgen, out errors, out exc);

+        return outcome;

+      }

+      else {

+        throw new Exception("VerifyCurrent has null implementation");

+      }

+    }

+

+    private bool IsOutcomeNotHoudini(ProverInterface.Outcome outcome, List<Counterexample> errors) {

+      switch (outcome) {

+        case ProverInterface.Outcome.Valid:

+          return false;

+        case ProverInterface.Outcome.Invalid:

+          Contract.Assume(errors != null);

+          foreach (Counterexample error in errors) {

+            if (ExtractRefutedAnnotation(error) == null)

+              return true;

+          }

+          return false;

+        default:

+          return true;

+      }

+    }

+

+    // returns true if at least one of the violations is non-candidate

+    private bool AnyNonCandidateViolation(ProverInterface.Outcome outcome, List<Counterexample> errors) {

+      switch (outcome) {

+        case ProverInterface.Outcome.Invalid:

+          Contract.Assert(errors != null);

+          foreach (Counterexample error in errors) {

+            if (ExtractRefutedAnnotation(error) == null)

+              return true;

+          }

+          return false;

+        default:

+          return false;

+      }

+    }

+

+    private List<Counterexample> emptyList = new List<Counterexample>();

+

+    // Record most current Non-Candidate errors found by Boogie, etc.

+    private void UpdateHoudiniOutcome(HoudiniOutcome houdiniOutcome,

+                                      Implementation implementation,

+                                      ProverInterface.Outcome verificationOutcome,

+                                      List<Counterexample> errors) {

+      string implName = implementation.ToString();

+      houdiniOutcome.implementationOutcomes.Remove(implName);

+      List<Counterexample> nonCandidateErrors = new List<Counterexample>();

+

+      switch (verificationOutcome) {

+        case ProverInterface.Outcome.Invalid:

+          Contract.Assume(errors != null);

+          foreach (Counterexample error in errors) {

+            if (ExtractRefutedAnnotation(error) == null)

+              nonCandidateErrors.Add(error);

+          }

+          break;

+        default:

+          break;

+      }

+      houdiniOutcome.implementationOutcomes.Add(implName, new VCGenOutcome(verificationOutcome, nonCandidateErrors));

+    }

+

+    private void FlushWorkList(HoudiniState current) {

+      this.NotifyFlushStart();

+      HoudiniVCGen vcgen;

+      vcgenSessions.TryGetValue(current.Implementation, out vcgen);

+      VCExpr axiom = BuildAxiom(vcgen, current.Assignment);

+      while (current.WorkList.Count > 0) {

+        this.NotifyIteration();

+

+        current.Implementation = current.WorkList.Peek();

+        this.NotifyImplementation(current.Implementation);

+

+        List<Counterexample> errors;

+        ProverInterface.Outcome outcome = VerifyUsingAxiom(current.Implementation, axiom, out errors);

+        UpdateHoudiniOutcome(current.Outcome, current.Implementation, outcome, errors);

+        this.NotifyOutcome(outcome);

+

+        current.WorkList.Dequeue();

+        this.NotifyDequeue();

+

+      }

+      this.NotifyFlushFinish();

+    }

+

+    private void UpdateAssignment(HoudiniState current, RefutedAnnotation refAnnot) {

+      current.Assignment.Remove(refAnnot.Constant);

+      current.Assignment.Add(refAnnot.Constant, false);

+      this.NotifyConstant(refAnnot.Constant);

+    }

+

+    private void AddToWorkList(HoudiniState current, Implementation imp) {

+      if (!current.WorkList.Contains(imp) && !current.isBlackListed(imp.Name)) {

+        current.WorkList.Enqueue(imp);

+        this.NotifyEnqueue(imp);

+      }

+    }

+

+    private void UpdateWorkList(HoudiniState current,

+                                ProverInterface.Outcome outcome,

+                                List<Counterexample> errors) {

+      Contract.Assume(current.Implementation != null);

+

+      switch (outcome) {

+        case ProverInterface.Outcome.Valid:

+          current.WorkList.Dequeue();

+          this.NotifyDequeue();

+          break;

+        case ProverInterface.Outcome.Invalid:

+          Contract.Assume(errors != null);

+          bool dequeue = false;

+          foreach (Counterexample error in errors) {

+            RefutedAnnotation refutedAnnotation = ExtractRefutedAnnotation(error);

+            if (refutedAnnotation != null) {

+              foreach (Implementation implementation in FindImplementationsToEnqueue(refutedAnnotation, current.Implementation)) { AddToWorkList(current, implementation); }

+              UpdateAssignment(current, refutedAnnotation);

+            }

+            else {

+              dequeue = true; //once one non-houdini error is hit dequeue?!

+            }

+          }

+          if (dequeue) {

+            current.WorkList.Dequeue();

+            this.NotifyDequeue();

+          }

+          break;

+        case ProverInterface.Outcome.TimeOut:

+          // TODO: reset session instead of blocking timed out funcs?

+          current.addToBlackList(current.Implementation.Name);

+          current.WorkList.Dequeue();

+          this.NotifyDequeue();

+          break;

+        case ProverInterface.Outcome.OutOfMemory:

+        case ProverInterface.Outcome.Undetermined:

+          current.WorkList.Dequeue();

+          this.NotifyDequeue();

+          break;

+        default:

+          throw new Exception("Unknown vcgen outcome");

+      }

+    }

+

+

+    private void AddRelatedToWorkList(HoudiniState current, RefutedAnnotation refutedAnnotation) {

+      Contract.Assume(current.Implementation != null);

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

+        AddToWorkList(current, implementation);

+      }

+    }

+

+

+    // Updates the worklist and current assignment

+    // @return true if the current function is kept on the queue

+    private bool UpdateAssignmentWorkList(HoudiniState current,

+                                          ProverInterface.Outcome outcome,

+                                          List<Counterexample> errors) {

+      Contract.Assume(current.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);

+            if (refutedAnnotation != null) { // some candidate annotation removed

+              AddRelatedToWorkList(current, refutedAnnotation);

+              UpdateAssignment(current, refutedAnnotation);

+              dequeue = false;

+            }

+          }

+          break;

+

+        case ProverInterface.Outcome.TimeOut:

+          // TODO: reset session instead of blocking timed out funcs?

+          current.addToBlackList(current.Implementation.Name);

+          break;

+        case ProverInterface.Outcome.Undetermined:

+        case ProverInterface.Outcome.OutOfMemory:

+          break;

+        default:

+          throw new Exception("Unknown vcgen outcome");

+      }

+      if (dequeue) {

+        current.WorkList.Dequeue();

+        this.NotifyDequeue();

+      }

+      return !dequeue;

+    }

+

+    private class HoudiniState {

+      private Queue<Implementation> _workList;

+      private HashSet<string> blackList;

+      private Dictionary<string, bool> _assignment;

+      private Implementation _implementation;

+      private HoudiniOutcome _outcome;

+

+      public HoudiniState(Queue<Implementation> workList, Dictionary<string, bool> currentAssignment) {

+        this._workList = workList;

+        this._assignment = currentAssignment;

+        this._implementation = null;

+        this._outcome = new HoudiniOutcome();

+        this.blackList = new HashSet<string>();

+      }

+

+      public Queue<Implementation> WorkList {

+        get { return this._workList; }

+      }

+      public Dictionary<string, bool> Assignment {

+        get { return this._assignment; }

+      }

+      public Implementation Implementation {

+        get { return this._implementation; }

+        set { this._implementation = value; }

+      }

+      public HoudiniOutcome Outcome {

+        get { return this._outcome; }

+      }

+      public bool isBlackListed(string funcName) {

+        return blackList.Contains(funcName);

+      }

+      public void addToBlackList(string funcName) {

+        blackList.Add(funcName);

+      }

+    }

+

+    private void PrintBadList(string kind, List<string> list) {

+      if (list.Count != 0) {

+        Console.WriteLine("----------------------------------------");

+        Console.WriteLine("Functions: {0}", kind);

+        foreach (string fname in list) {

+          Console.WriteLine("\t{0}", fname);

+        }

+        Console.WriteLine("----------------------------------------");

+      }

+    }

+

+    private void PrintBadOutcomes(List<string> timeouts, List<string> inconc, List<string> errors) {

+      PrintBadList("TimedOut", timeouts);

+      PrintBadList("Inconclusive", inconc);

+      PrintBadList("Errors", errors);

+    }

+

+    public HoudiniOutcome VerifyProgram() {

+      HoudiniOutcome outcome = VerifyProgramSameFuncFirst();

+      PrintBadOutcomes(outcome.ListOfTimeouts, outcome.ListOfInconclusives, outcome.ListOfErrors);

+      return outcome;

+    }

+

+    // Old main loop

+    public HoudiniOutcome VerifyProgramUnorderedWork() {

+      HoudiniState current = new HoudiniState(BuildWorkList(program), BuildAssignment(houdiniConstants.Keys));

+      this.NotifyStart(program, houdiniConstants.Keys.Count);

+

+      

+

+      while (current.WorkList.Count > 0) {

+        System.GC.Collect();

+        this.NotifyIteration();

+

+        HoudiniVCGen vcgen;

+        vcgenSessions.TryGetValue(current.Implementation, out vcgen);

+        VCExpr axiom = BuildAxiom(vcgen, current.Assignment);

+        this.NotifyAssignment(current.Assignment);

+

+        current.Implementation = current.WorkList.Peek();

+        this.NotifyImplementation(current.Implementation);

+

+        List<Counterexample> errors;

+        ProverInterface.Outcome outcome = VerifyUsingAxiom(current.Implementation, axiom, out errors);

+        this.NotifyOutcome(outcome);

+

+        UpdateHoudiniOutcome(current.Outcome, current.Implementation, outcome, errors);

+        if (IsOutcomeNotHoudini(outcome, errors) && !continueAtError) {

+          current.WorkList.Dequeue();

+          this.NotifyDequeue();

+          FlushWorkList(current);

+        }

+        else

+          UpdateWorkList(current, outcome, errors);

+      }

+      this.NotifyEnd(true);

+      current.Outcome.assignment = current.Assignment;

+      return current.Outcome;

+    }

+

+    // New main loop

+    public HoudiniOutcome VerifyProgramSameFuncFirst() {

+      HoudiniState current = new HoudiniState(BuildWorkList(program), BuildAssignment(houdiniConstants.Keys));

+      this.NotifyStart(program, houdiniConstants.Keys.Count);

+

+      while (current.WorkList.Count > 0) {

+        bool exceptional = false;

+        System.GC.Collect();

+        this.NotifyIteration();

+

+        current.Implementation = current.WorkList.Peek();

+        this.NotifyImplementation(current.Implementation);

+

+        List<Counterexample> errors;

+        ProverInterface.Outcome outcome = VerifyCurrent(current, program, out errors, out exceptional);

+

+        // updates to worklist already done in VerifyCurrent, unless there was an exception

+        if (exceptional) {

+          this.NotifyOutcome(outcome);

+          UpdateHoudiniOutcome(current.Outcome, current.Implementation, outcome, errors);

+          if (IsOutcomeNotHoudini(outcome, errors) && !continueAtError) {

+            current.WorkList.Dequeue();

+            this.NotifyDequeue();

+            FlushWorkList(current);

+          }

+          else {

+            UpdateAssignmentWorkList(current, outcome, errors);

+          }

+          exceptional = false;

+        }

+      }

+      this.NotifyEnd(true);

+      current.Outcome.assignment = current.Assignment;

+      return current.Outcome;

+    }

+

+    //Clean houdini (Based on "Houdini Spec in Boogie" email 10/22/08

+    //Aborts when there is a violation of non-candidate assertion

+    //This can be used in eager mode (continueAfterError) by simply making

+    //all non-candidate annotations as unchecked (free requires/ensures, assumes)

+    public HoudiniOutcome PerformHoudiniInference() {

+      HoudiniState current = new HoudiniState(BuildWorkList(program), BuildAssignment(houdiniConstants.Keys));

+      this.NotifyStart(program, houdiniConstants.Keys.Count);

+

+      Console.WriteLine("Using the new houdini algorithm\n");

+

+      while (current.WorkList.Count > 0) {

+        bool exceptional = false;

+        System.GC.Collect();

+        this.NotifyIteration();

+

+        current.Implementation = current.WorkList.Peek();

+        this.NotifyImplementation(current.Implementation);

+

+        List<Counterexample> errors;

+        ProverInterface.Outcome outcome = HoudiniVerifyCurrent(current, program, out errors, out exceptional);

+

+        // updates to worklist already done in VerifyCurrent, unless there was an exception

+        if (exceptional) {

+          this.NotifyOutcome(outcome);

+          UpdateHoudiniOutcome(current.Outcome, current.Implementation, outcome, errors);

+          if (AnyNonCandidateViolation(outcome, errors)) { //abort

+            current.WorkList.Dequeue();

+            this.NotifyDequeue();

+            FlushWorkList(current);

+          }

+          else { //continue

+            UpdateAssignmentWorkList(current, outcome, errors);

+          }

+        }

+      }

+      this.NotifyEnd(true);

+      current.Outcome.assignment = current.Assignment;

+      return current.Outcome;

+    }

+

+    private List<Implementation> FindImplementationsToEnqueue(RefutedAnnotation refutedAnnotation, Implementation currentImplementation) {

+      List<Implementation> implementations = new List<Implementation>();

+      switch (refutedAnnotation.Kind) {

+        case RefutedAnnotationKind.REQUIRES:

+          foreach (Implementation callee in callGraph.Successors(currentImplementation)) {

+            Contract.Assume(callee.Proc != null);

+            if (callee.Proc.Equals(refutedAnnotation.CalleeProc))

+              implementations.Add(callee);

+          }

+          break;

+        case RefutedAnnotationKind.ENSURES:

+          foreach (Implementation caller in callGraph.Predecessors(currentImplementation))

+            implementations.Add(caller);

+          break;

+        case RefutedAnnotationKind.ASSERT: //the implementation is already in queue

+          break;

+        default:

+          throw new Exception("Unknown Refuted annotation kind:" + refutedAnnotation.Kind);

+      }

+      return implementations;

+    }

+

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

+

+    private class RefutedAnnotation {

+      private string _constant;

+      private RefutedAnnotationKind _kind;

+      private Procedure _callee;

+

+      private RefutedAnnotation(string constant, RefutedAnnotationKind kind, Procedure callee) {

+        this._constant = constant;

+        this._kind = kind;

+        this._callee = callee;

+      }

+      public RefutedAnnotationKind Kind {

+        get { return this._kind; }

+      }

+      public string Constant {

+        get { return this._constant; }

+      }

+      public Procedure CalleeProc {

+        get { return this._callee; }

+      }

+      public static RefutedAnnotation BuildRefutedRequires(string constant, Procedure callee) {

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

+      }

+      public static RefutedAnnotation BuildRefutedEnsures(string constant) {

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

+      }

+      public static RefutedAnnotation BuildRefutedAssert(string constant) {

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

+      }

+

+    }

+

+    private void PrintRefutedCall(CallCounterexample err, XmlSink xmlOut) {

+      Expr cond = err.FailingRequires.Condition;

+      string houdiniConst;

+      if (MatchCandidate(cond, out houdiniConst)) {

+        xmlOut.WriteError("precondition violation", err.FailingCall.tok, err.FailingRequires.tok, err.Trace);

+      }

+    }

+

+    private void PrintRefutedReturn(ReturnCounterexample err, XmlSink xmlOut) {

+      Expr cond = err.FailingEnsures.Condition;

+      string houdiniConst;

+      if (MatchCandidate(cond, out houdiniConst)) {

+        xmlOut.WriteError("postcondition violation", err.FailingReturn.tok, err.FailingEnsures.tok, err.Trace);

+      }

+    }

+

+    private void PrintRefutedAssert(AssertCounterexample err, XmlSink xmlOut) {

+      Expr cond = err.FailingAssert.OrigExpr;

+      string houdiniConst;

+      if (MatchCandidate(cond, out houdiniConst)) {

+        xmlOut.WriteError("postcondition violation", err.FailingAssert.tok, err.FailingAssert.tok, err.Trace);

+      }

+    }

+

+

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

+      XmlSink xmlRefuted = CommandLineOptions.Clo.XmlRefuted;

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

+        DateTime start = DateTime.Now;

+        xmlRefuted.WriteStartMethod(curFunc.ToString(), start);

+

+        foreach (Counterexample error in errors) {

+          CallCounterexample ce = error as CallCounterexample;

+          if (ce != null) PrintRefutedCall(ce, xmlRefuted);

+          ReturnCounterexample re = error as ReturnCounterexample;

+          if (re != null) PrintRefutedReturn(re, xmlRefuted);

+          AssertCounterexample ae = error as AssertCounterexample;

+          if (ae != null) PrintRefutedAssert(ae, xmlRefuted);

+        }

+

+        DateTime end = DateTime.Now;

+        xmlRefuted.WriteEndMethod("errors", end, end.Subtract(start));

+      }

+    }

+

+    private RefutedAnnotation ExtractRefutedAnnotation(Counterexample error) {

+      string houdiniConstant;

+      CallCounterexample callCounterexample = error as CallCounterexample;

+      if (callCounterexample != null) {

+        Procedure failingProcedure = callCounterexample.FailingCall.Proc;

+        Requires failingRequires = callCounterexample.FailingRequires;

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

+          Contract.Assert(houdiniConstant != null);

+          return RefutedAnnotation.BuildRefutedRequires(houdiniConstant, failingProcedure);

+        }

+      }

+      ReturnCounterexample returnCounterexample = error as ReturnCounterexample;

+      if (returnCounterexample != null) {

+        Ensures failingEnsures = returnCounterexample.FailingEnsures;

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

+          Contract.Assert(houdiniConstant != null);

+          return RefutedAnnotation.BuildRefutedEnsures(houdiniConstant);

+        }

+      }

+      AssertCounterexample assertCounterexample = error as AssertCounterexample;

+      if (assertCounterexample != null) {

+        AssertCmd failingAssert = assertCounterexample.FailingAssert;

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

+          Contract.Assert(houdiniConstant != null);

+          return RefutedAnnotation.BuildRefutedAssert(houdiniConstant);

+        }

+      }

+

+      return null;

+    }

+

+    private ProverInterface.Outcome TryCatchVerify(HoudiniVCGen vcgen, VCExpr axiom, out List<Counterexample> errors) {

+      ProverInterface.Outcome outcome;

+      try {

+        outcome = vcgen.Verify(axiom, out errors);

+      }

+      catch (VCGenException e) {

+        Contract.Assume(e != null);

+        errors = null;

+        outcome = ProverInterface.Outcome.Undetermined;

+      }

+      catch (UnexpectedProverOutputException upo) {

+        Contract.Assume(upo != null);

+        errors = null;

+        outcome = ProverInterface.Outcome.Undetermined;

+      }

+      return outcome;

+    }

+

+    //version of TryCatchVerify that spins on the same function

+    //as long as the current assignment is changing

+    private ProverInterface.Outcome TrySpinSameFunc(HoudiniState current,

+                                          Program program,

+                                          HoudiniVCGen vcgen,

+                                          out List<Counterexample> errors,

+                                          out bool exceptional) {

+      Contract.Assert(current.Implementation != null);

+      ProverInterface.Outcome outcome;

+      errors = null;

+      outcome = ProverInterface.Outcome.Undetermined;

+      try {

+        bool trySameFunc = true;

+        bool pastFirstIter = false; //see if this new loop is even helping

+

+        do {

+          if (pastFirstIter) {

+            System.GC.Collect();

+            this.NotifyIteration();

+          }

+

+          this.vcgenSessions.TryGetValue(current.Implementation, out vcgen);

+          VCExpr currentAx = BuildAxiom(vcgen, current.Assignment);

+          this.NotifyAssignment(current.Assignment);

+

+          outcome = vcgen.Verify(currentAx, out errors);

+          this.NotifyOutcome(outcome);

+

+          DebugRefutedCandidates(current.Implementation, errors);

+          UpdateHoudiniOutcome(current.Outcome, current.Implementation, outcome, errors);

+          if (!continueAtError && IsOutcomeNotHoudini(outcome, errors)) {

+            current.WorkList.Dequeue();

+            this.NotifyDequeue();

+            trySameFunc = false;

+            FlushWorkList(current);

+          }

+          else {

+            trySameFunc = UpdateAssignmentWorkList(current, outcome, errors);

+            //reset for the next round

+            errors = null;

+            outcome = ProverInterface.Outcome.Undetermined;

+          }

+          pastFirstIter = true;

+        } while (trySameFunc && current.WorkList.Count > 0);

+

+      }

+      catch (VCGenException e) {

+        Contract.Assume(e != null);

+        NotifyException("VCGen");

+        exceptional = true;

+        return outcome;

+      }

+      catch (UnexpectedProverOutputException upo) {

+        Contract.Assume(upo != null);

+        NotifyException("UnexpectedProverOutput");

+        exceptional = true;

+        return outcome;

+      }

+      exceptional = false;

+      return outcome;

+    }

+

+    //Similar to TrySpinSameFunc except no Candidate logic

+    private ProverInterface.Outcome HoudiniVerifyCurrentAux(HoudiniState current,

+                                          Program program,

+                                          HoudiniVCGen vcgen,

+                                          out List<Counterexample> errors,

+                                          out bool exceptional) {

+      Contract.Assert(current.Implementation != null);

+      ProverInterface.Outcome outcome;

+      errors = null;

+      outcome = ProverInterface.Outcome.Undetermined;

+      try {

+        bool trySameFunc = true;

+        bool pastFirstIter = false; //see if this new loop is even helping

+

+        do {

+          if (pastFirstIter) {

+            System.GC.Collect();

+            this.NotifyIteration();

+          }

+

+          VCExpr currentAx = BuildAxiom(vcgen, current.Assignment);

+          this.NotifyAssignment(current.Assignment);

+

+          //check the VC with the current assignment

+          outcome = vcgen.Verify(currentAx, out errors);

+          this.NotifyOutcome(outcome);

+

+          DebugRefutedCandidates(current.Implementation, errors);

+          UpdateHoudiniOutcome(current.Outcome, current.Implementation, outcome, errors);

+

+          if (AnyNonCandidateViolation(outcome, errors)) { //abort

+            current.WorkList.Dequeue();

+            this.NotifyDequeue();

+            trySameFunc = false;

+            FlushWorkList(current);

+          }

+          else { //continue

+            trySameFunc = UpdateAssignmentWorkList(current, outcome, errors);

+            //reset for the next round

+            errors = null;

+            outcome = ProverInterface.Outcome.Undetermined;

+          }

+          pastFirstIter = true;

+        } while (trySameFunc && current.WorkList.Count > 0);

+

+      }

+      catch (VCGenException e) {

+        Contract.Assume(e != null);

+        NotifyException("VCGen");

+        exceptional = true;

+        return outcome;

+      }

+      catch (UnexpectedProverOutputException upo) {

+        Contract.Assume(upo != null);

+        NotifyException("UnexpectedProverOutput");

+        exceptional = true;

+        return outcome;

+      }

+      exceptional = false;

+      return outcome;

+    }

+  }

+

+  public enum HoudiniOutcomeKind { Done, FatalError, VerificationCompleted }

+

+  public class VCGenOutcome {

+    public ProverInterface.Outcome outcome;

+    public List<Counterexample> errors;

+    public VCGenOutcome(ProverInterface.Outcome outcome, List<Counterexample> errors) {

+      this.outcome = outcome;

+      this.errors = errors;

+    }

+  }

+

+  public class HoudiniOutcome {

+    // final assignment

+    public Dictionary<string, bool> assignment = new Dictionary<string, bool>();

+    // boogie errors

+    public Dictionary<string, VCGenOutcome> implementationOutcomes = new Dictionary<string, VCGenOutcome>();

+    // outcome kind    

+    public HoudiniOutcomeKind kind;

+

+    // statistics 

+

+    private int CountResults(ProverInterface.Outcome outcome) {

+      int outcomeCount = 0;

+      foreach (VCGenOutcome verifyOutcome in implementationOutcomes.Values) {

+        if (verifyOutcome.outcome == outcome)

+          outcomeCount++;

+      }

+      return outcomeCount;

+    }

+

+    private List<string> ListOutcomeMatches(ProverInterface.Outcome outcome) {

+      List<string> result = new List<string>();

+      foreach (KeyValuePair<string, VCGenOutcome> kvpair in implementationOutcomes) {

+        if (kvpair.Value.outcome == outcome)

+          result.Add(kvpair.Key);

+      }

+      return result;

+    }

+

+    public int ErrorCount {

+      get {

+        return CountResults(ProverInterface.Outcome.Invalid);

+      }

+    }

+    public int Verified {

+      get {

+        return CountResults(ProverInterface.Outcome.Valid);

+      }

+    }

+    public int Inconclusives {

+      get {

+        return CountResults(ProverInterface.Outcome.Undetermined);

+      }

+    }

+    public int TimeOuts {

+      get {

+        return CountResults(ProverInterface.Outcome.TimeOut);

+      }

+    }

+    public List<string> ListOfTimeouts {

+      get {

+        return ListOutcomeMatches(ProverInterface.Outcome.TimeOut);

+      }

+    }

+    public List<string> ListOfInconclusives {

+      get {

+        return ListOutcomeMatches(ProverInterface.Outcome.Undetermined);

+      }

+    }

+    public List<string> ListOfErrors {

+      get {

+        return ListOutcomeMatches(ProverInterface.Outcome.Invalid);

+      }

+    }

+  }

+

+}

diff --git a/Source/Houdini/Houdini.csproj b/Source/Houdini/Houdini.csproj
new file mode 100644
index 00000000..bd4e693b
--- /dev/null
+++ b/Source/Houdini/Houdini.csproj
@@ -0,0 +1,105 @@
+<?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>8.0.30703</ProductVersion>

+    <SchemaVersion>2.0</SchemaVersion>

+    <ProjectGuid>{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}</ProjectGuid>

+    <OutputType>Library</OutputType>

+    <AppDesignerFolder>Properties</AppDesignerFolder>

+    <RootNamespace>Microsoft.Boogie.Houdini</RootNamespace>

+    <AssemblyName>Houdini</AssemblyName>

+    <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>

+    <FileAlignment>512</FileAlignment>

+  </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>

+  </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>

+  </PropertyGroup>

+  <PropertyGroup>

+    <SignAssembly>true</SignAssembly>

+  </PropertyGroup>

+  <PropertyGroup>

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

+  </PropertyGroup>

+  <ItemGroup>

+    <Reference Include="System" />

+    <Reference Include="System.Core" />

+    <Reference Include="System.Xml.Linq" />

+    <Reference Include="System.Data.DataSetExtensions" />

+    <Reference Include="Microsoft.CSharp" />

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

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

+  </ItemGroup>

+  <ItemGroup>

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

+    <Compile Include="Houdini.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="..\ParserHelper\ParserHelper.csproj">

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

+      <Name>ParserHelper</Name>

+    </ProjectReference>

+    <ProjectReference Include="..\Provers\Simplify\Simplify.csproj">

+      <Project>{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}</Project>

+      <Name>Simplify</Name>

+    </ProjectReference>

+    <ProjectReference Include="..\Provers\Z3\Z3.csproj">

+      <Project>{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}</Project>

+      <Name>Z3</Name>

+    </ProjectReference>

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

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

+      <Name>VCExpr</Name>

+    </ProjectReference>

+    <ProjectReference Include="..\VCGeneration\VCGeneration.csproj">

+      <Project>{E1F10180-C7B9-4147-B51F-FA1B701966DC}</Project>

+      <Name>VCGeneration</Name>

+    </ProjectReference>

+  </ItemGroup>

+  <ItemGroup>

+    <Folder Include="Properties\" />

+  </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
diff --git a/Source/Houdini/Houdini.ssc b/Source/Houdini/Houdini.ssc
deleted file mode 100644
index bd8348be..00000000
--- a/Source/Houdini/Houdini.ssc
+++ /dev/null
@@ -1,1188 +0,0 @@
-//-----------------------------------------------------------------------------

-//

-// Copyright (C) Microsoft Corporation.  All Rights Reserved.

-//

-//-----------------------------------------------------------------------------

-using System;

-using Microsoft.Contracts;

-using System.Collections.Generic;

-using Microsoft.Boogie;

-using Microsoft.Boogie.Simplify.AST;

-using VC;

-using Microsoft.Boogie.Z3;

-using Microsoft.AbstractInterpretationFramework;

-using Microsoft.Boogie.AbstractInterpretation;

-using System.Collections;

-using System.Compiler;

-using System.IO;

-

-namespace Microsoft.Boogie.Houdini

-{

-

-    class ReadOnlyDictionary<K,V> {

-        private Dictionary<K,V>! dictionary;

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

-          this.dictionary = dictionary;

-        }

-        

-        public Dictionary<K,V>.KeyCollection Keys {

-          get { return this.dictionary.Keys; }

-        }

-        

-        public bool TryGetValue(K k, out V? v) {

-          return this.dictionary.TryGetValue(k, out v);

-        }

-

-        public bool ContainsKey(K k) {

-          return this.dictionary.ContainsKey(k);

-        }        

-    }

-    

-    public class CallGraph {

-      

-       private IGraphNavigator! aiCallGraph;

-       

-       public CallGraph(IGraphNavigator! aiCallGraph) {

-         this.aiCallGraph = aiCallGraph; 

-       }

-       

-       public IEnumerable! PreviousNodes(Implementation! n) {

-         return (!)this.aiCallGraph.PreviousNodes(n);

-       }       

-       public IEnumerable! NextNodes(Implementation! n) {

-         return (!)this.aiCallGraph.NextNodes(n);

-       }       

-    

-    }

-    

-    public abstract class HoudiniObserver {

-      public virtual void UpdateStart(Program! program, int numConstants) {}

-      public virtual void UpdateIteration() {}

-      public virtual void UpdateImplementation(Implementation! implementation) {}

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

-      public virtual void UpdateOutcome(VCGen.Outcome outcome) {}

-      public virtual void UpdateEnqueue(Implementation! implementation) {}

-      public virtual void UpdateDequeue() {}

-      public virtual void UpdateConstant(string! constantName) {}

-      public virtual void UpdateEnd(bool isNormalEnd) {}

-      public virtual void UpdateFlushStart() {}

-      public virtual void UpdateFlushFinish() {}

-      public virtual void SeeException(string! msg){}

-    }

-

-    public class IterationTimer <K> {

-      private Dictionary<K, List<double>!>! times;

-        

-      public IterationTimer () {

-        times = new Dictionary<K, List<double>!>();

-      }

-        

-      public void AddTime(K key, double timeMS) {

-        List<double> oldList;

-        times.TryGetValue(key, out oldList);

-        if (oldList == null) {

-          oldList = new List<double>();

-        } else {

-          times.Remove(key);

-        }

-        oldList.Add(timeMS);

-        times.Add(key, oldList);

-      }

-        

-      public void PrintTimes(TextWriter! wr) {

-        wr.WriteLine ("Total procedures: {0}", times.Count);

-        double total = 0;

-        int totalIters = 0;

-        foreach(KeyValuePair<K, List<double>!> kv in times) {

-          int curIter = 0;

-          wr.WriteLine("Times for {0}:", kv.Key);

-          foreach(double v in kv.Value) {

-            wr.WriteLine("  ({0})\t{1}ms", curIter, v);

-            total += v;

-            curIter++;

-          }

-          totalIters += curIter;

-        }

-        total = total / 1000.0;

-        wr.WriteLine ("Total time: {0} (s)", total);

-        wr.WriteLine ("Avg: {0} (s/iter)", total/totalIters);

-      }

-    }

-    

-    public class HoudiniTimer : HoudiniObserver {

-      private DateTime startT;

-      private Implementation curImp;

-      private IterationTimer<string!>! times;

-      private TextWriter! wr;

-      

-      public HoudiniTimer(TextWriter! wr) {

-        this.wr = wr;

-        times = new IterationTimer<string!>();

-      }

-      public override void UpdateIteration() {

-        startT = DateTime.Now;

-      }

-      public override void UpdateImplementation(Implementation! implementation){

-        curImp = implementation;

-      }

-      public override void UpdateOutcome (VCGen.Outcome o) {

-        assert curImp != null;

-        DateTime endT = DateTime.Now;

-        times.AddTime(curImp.Name, (endT - startT).TotalMilliseconds); // assuming names are unique

-      }     

-      public void PrintTimes() {

-        wr.WriteLine("-----------------------------------------");

-        wr.WriteLine("Times for each iteration for each procedure");

-        wr.WriteLine("-----------------------------------------");

-        times.PrintTimes(wr);

-      }

-    }

-    

-    public class HoudiniTextReporter: HoudiniObserver {

-      private TextWriter! wr;

-      private int currentIteration = -1;

-      

-      public HoudiniTextReporter(TextWriter! wr) {

-        this.wr = wr;

-      }

-      public override void UpdateStart(Program! program, int numConstants) {

-        wr.WriteLine("Houdini started:" + program.ToString() + " #constants: " + numConstants.ToString());

-        currentIteration = -1;

-        wr.Flush();

-      }

-      public override void UpdateIteration() {

-        currentIteration++;

-        wr.WriteLine("---------------------------------------");

-        wr.WriteLine("Houdini iteration #" + currentIteration);

-        wr.Flush();

-      }

-      public override void UpdateImplementation(Implementation! implementation){

-        wr.WriteLine("implementation under analysis :" + implementation.Name);

-        wr.Flush();

-      }

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

-        bool firstTime = true;

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

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

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

-          string! valString; // ugliness to get it lower cased

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

-          wr.Write(kv.Key + " == " + valString);

-        }

-        wr.WriteLine(");");

-        wr.Flush();

-      }

-      public override void UpdateOutcome(VCGen.Outcome outcome) {

-        wr.WriteLine("analysis outcome :" + outcome);

-        wr.Flush();

-      }

-      public override void UpdateEnqueue(Implementation! implementation) {

-        wr.WriteLine("worklist enqueue :" + implementation.Name);

-        wr.Flush();

-      }

-      public override void UpdateDequeue() {

-        wr.WriteLine("worklist dequeue");

-        wr.Flush();

-      }

-      public override void UpdateConstant(string! constantName) {

-        wr.WriteLine("constant disabled : " + constantName);

-        wr.Flush();

-      }

-      public override void UpdateEnd(bool isNormalEnd) {

-        wr.WriteLine("Houdini ended: " + (isNormalEnd ? "Normal" : "Abnormal"));

-        wr.WriteLine("Number of iterations: " + (this.currentIteration+1));

-        wr.Flush();

-      }

-      public override void UpdateFlushStart() {

-        wr.WriteLine("***************************************");

-        wr.WriteLine("Flushing remaining implementations");

-        wr.Flush();

-      }

-      public override void UpdateFlushFinish() {

-        wr.WriteLine("***************************************");

-        wr.WriteLine("Flushing finished");

-        wr.Flush();

-      }

-      public override void SeeException(string! msg) {

-        wr.WriteLine("Caught exception: " + msg);

-        wr.Flush();

-      }

-

-    }

-    

-    

-    public abstract class ObservableHoudini {

-      private List<HoudiniObserver!>! observers= new List<HoudiniObserver!>();

-      

-      public void AddObserver(HoudiniObserver! observer) {

-        if (!observers.Contains(observer))

-          observers.Add(observer);

-      }

-      private delegate void NotifyDelegate(HoudiniObserver! observer);

-      

-      private void Notify(NotifyDelegate! notifyDelegate) {

-        foreach (HoudiniObserver! observer in observers) {

-          notifyDelegate(observer);

-        }

-      }

-      protected void NotifyStart(Program! program, int numConstants) { 

-        NotifyDelegate notifyDelegate = (NotifyDelegate) delegate (HoudiniObserver! r) { r.UpdateStart(program, numConstants); };

-        Notify(notifyDelegate);

-      }

-      protected void NotifyIteration() {

-        Notify((NotifyDelegate) delegate (HoudiniObserver! r) { r.UpdateIteration(); });

-      }

-      protected void NotifyImplementation(Implementation! implementation) {

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

-      }

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

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

-      }

-      protected void NotifyOutcome(VCGen.Outcome outcome) {

-        Notify((NotifyDelegate) delegate (HoudiniObserver! r) { r.UpdateOutcome(outcome); });

-      }

-      protected void NotifyEnqueue(Implementation! implementation){

-        Notify((NotifyDelegate) delegate (HoudiniObserver! r) { r.UpdateEnqueue(implementation); });

-      }

-      protected void NotifyDequeue(){

-        Notify((NotifyDelegate) delegate (HoudiniObserver! r) { r.UpdateDequeue(); });

-      }

-      protected void NotifyConstant(string! constantName){

-        Notify((NotifyDelegate) delegate (HoudiniObserver! r) { r.UpdateConstant(constantName); });

-      }

-      protected void NotifyEnd(bool isNormalEnd) {

-        Notify((NotifyDelegate) delegate (HoudiniObserver! r) { r.UpdateEnd(isNormalEnd); });

-      }

-      protected void NotifyFlushStart() {

-        Notify((NotifyDelegate) delegate (HoudiniObserver! r) { r.UpdateFlushStart(); });

-      }

-      protected void NotifyFlushFinish() {

-        Notify((NotifyDelegate) delegate (HoudiniObserver! r) { r.UpdateFlushFinish(); });

-      }

-      

-      protected void NotifyException(string! msg) {

-        Notify((NotifyDelegate) delegate (HoudiniObserver! r) { r.SeeException(msg); });

-      }

-    }

-    

-    public enum HoudiniProver { Z3, Z3API }

-    

-    public class Houdini : ObservableHoudini {

-    

-        private Program! program;

-        

-        private ReadOnlyDictionary<string!,IdentifierExpr!>! houdiniConstants;

-        private ReadOnlyDictionary<Implementation!,HdnVCGen!>! vcgenSessions;

-        private CallGraph! callGraph;

-        private bool continueAtError;

-        private HoudiniProver houdiniProver;

-        private HdnVCGenFactory! vcgenFactory;

-

-        public Houdini(Program! program, CallGraph! callgraph, bool continueAtError, HoudiniProver houdiniProver) {

-          this.program=program;

-          this.callGraph = callgraph;

-          this.continueAtError = continueAtError;

-          this.houdiniProver = houdiniProver;

-          HdnVCGenFactory factory;

-          switch (this.houdiniProver) {

-            case HoudiniProver.Z3:

-              factory = new Z3HdnVCGenFactory();

-              break;

-            case HoudiniProver.Z3API:

-            default: 

-              factory = new Z3APIHdnVCGenFactory();

-              break;

-          }

-          this.vcgenFactory = factory;

-          HoudiniHelper helper = new HoudiniHelper(factory);

-          this.houdiniConstants = helper.CollectExistentialConstants(program);

-          this.vcgenSessions = helper.PrepareVCGenSessions(program);

-        }

-

-        private Queue<Implementation!>! BuildWorkList(Program! program) {

-          Queue<Implementation!>! queue = new Queue<Implementation!>();

-          foreach ( Declaration! decl in program.TopLevelDeclarations ) {

-              Implementation impl = decl as Implementation;

-              if (impl!=null) {

-                queue.Enqueue(impl);

-              }

-          }

-          return queue;

-        }

-

-        private class HoudiniHelper {

-          private HdnVCGenFactory! vcgenFactory;

-          public HoudiniHelper(HdnVCGenFactory! vcgenFactory) {

-            this.vcgenFactory = vcgenFactory;

-          }

-        

-          public ReadOnlyDictionary<Implementation!,HdnVCGen!>! PrepareVCGenSessions(Program! program) {

-            Dictionary<Implementation!,HdnVCGen!>! vcgenSessions = new Dictionary<Implementation!,HdnVCGen!>();

-            

-            foreach ( Declaration! decl in program.TopLevelDeclarations ) {

-              Implementation impl = decl as Implementation;

-              if (impl!=null) {

-                // make a different simplify log file for each function

-                String simplifyLog = null;

-                if (CommandLineOptions.Clo.SimplifyLogFilePath != null) {

-                    simplifyLog = impl.ToString() + CommandLineOptions.Clo.SimplifyLogFilePath;

-                }

-                HdnVCGen! vcgen = vcgenFactory.BuildVCGen(program, simplifyLog, CommandLineOptions.Clo.SimplifyLogFileAppend);

-                vcgen.PrepareVerification(impl,program);

-                vcgenSessions.Add(impl,vcgen);

-              }

-            }

-            return new ReadOnlyDictionary<Implementation!,HdnVCGen!>(vcgenSessions);

-          }

-          

-          public ReadOnlyDictionary<string!,IdentifierExpr!>! CollectExistentialConstants(Program! program) {

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

-            foreach ( Declaration! decl in program.TopLevelDeclarations ) {

-              Constant constant = decl as Constant;

-              if (constant!=null) {

-                bool result=false;

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

-                  if (result==true) 

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

-                }

-              }

-            }

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

-          }          

-        }

-        

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

-          candidateConstant = null;

-          IExpr antecedent;

-          IExpr expr = boogieExpr as IExpr;

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

-            IdentifierExpr.ConstantFunApp constantFunApp = antecedent as IdentifierExpr.ConstantFunApp;

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

-              candidateConstant = constantFunApp.IdentifierExpr.Name;

-              return true;

-            }

-          }

-          return false;

-        }

-        

-        

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

-          Expr axiom = null;

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

-            IdentifierExpr constantExpr;

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

-            assume (constantExpr!=null);

-            Expr valueExpr = new LiteralExpr(Token.NoToken, kv.Value);

-            Expr constantAssignment = Expr.Binary(Token.NoToken,BinaryOperator.Opcode.Eq,constantExpr,valueExpr);  

-            if (axiom==null) 

-              axiom = constantAssignment;

-            else

-              axiom = Expr.Binary(Token.NoToken,BinaryOperator.Opcode.And,axiom,constantAssignment);

-          }

-          if (axiom==null)

-            axiom = new LiteralExpr(Token.NoToken, true);

-          return new Axiom(Token.NoToken,axiom);

-        }

-

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

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

-           foreach (string! constant in constants)

-             initial.Add(constant,true);

-           return initial;

-        }

-

-       private VCGen.Outcome VerifyUsingAxiom(Implementation! implementation, Axiom! axiom, out List<Counterexample!>? errors) {

-            HdnVCGen vcgen;

-            vcgenSessions.TryGetValue(implementation,out vcgen);

-            if(vcgen==null)

-              throw new Exception("HdnVCGen not found for implementation: " + implementation.Name);

-	          vcgen.PushAxiom(axiom);

-              VCGen.Outcome outcome = TryCatchVerify(vcgen, out errors);

-			  vcgen.Pop();

-            return outcome;

-       }

-

-	   // the main procedure that checks a procedure and updates the

-	   // assignment and the worklist

-       private VCGen.Outcome HoudiniVerifyCurrent(HoudiniState! current,

-                                           Program! program,

-                                           out List<Counterexample!>? errors,

-                                           out bool exc) {

-            HdnVCGen vcgen;

-			if (current.Implementation == null)

-				throw new Exception("HoudiniVerifyCurrent has null implementation");

-

-            Implementation! implementation = current.Implementation;

-            vcgenSessions.TryGetValue(implementation,out vcgen);

-            if(vcgen==null)

-                throw new Exception("HdnVCGen not found for implementation: " + implementation.Name);

-              

-            VCGen.Outcome outcome = HoudiniVerifyCurrentAux(current, program, vcgen, out errors, out exc);

-            return outcome;            

-       }

-

-       private VCGen.Outcome VerifyCurrent(HoudiniState! current,

-                                           Program! program,

-                                           out List<Counterexample!>? errors,

-                                           out bool exc) {

-            HdnVCGen vcgen;

-            if (current.Implementation != null) {

-                Implementation! implementation = current.Implementation;

-                vcgenSessions.TryGetValue(implementation,out vcgen);

-                if(vcgen==null)

-                    throw new Exception("HdnVCGen not found for implementation: " + implementation.Name);

-              

-                VCGen.Outcome outcome = TrySpinSameFunc(current, program, vcgen, out errors, out exc);

-                return outcome;

-            } else {

-                throw new Exception("VerifyCurrent has null implementation");

-            }

-       }

-

-       private bool IsOutcomeNotHoudini(VCGen.Outcome outcome, List<Counterexample!>? errors) {

-              switch (outcome) {

-                case VCGen.Outcome.Correct: 

-                  return false;

-                  break;

-                case VCGen.Outcome.Errors: 

-                  assume (errors!=null);

-                  foreach (Counterexample error in errors) {

-                    if (ExtractRefutedAnnotation(error)==null)

-                      return true;

-                  }

-                  return false;

-                  break;

-                case VCGen.Outcome.TimedOut: 

-                case VCGen.Outcome.Inconclusive: 

-                default:

-                  return true;

-                  break;

-              }

-       }

-

-

-	  // returns true if at least one of the violations is non-candidate

-       private bool AnyNonCandidateViolation(VCGen.Outcome outcome, List<Counterexample!>? errors) {

-              switch (outcome) {

-                case VCGen.Outcome.Errors: 

-                  assert (errors!=null);

-                  foreach (Counterexample error in errors) {

-                    if (ExtractRefutedAnnotation(error)==null)

-                      return true;

-                  }

-                  return false;

-                  break;

-                case VCGen.Outcome.Correct: 

-                case VCGen.Outcome.TimedOut: 

-                case VCGen.Outcome.Inconclusive: 

-                default:

-                  return false;

-                  break;

-              }

-       }

-	  

-

-       private List<Counterexample!> emptyList = new List<Counterexample!>();

-

-       // Record most current Non-Candidate errors found by Boogie, etc.

-       private void UpdateHoudiniOutcome(HoudiniOutcome! houdiniOutcome, 

-                                         Implementation! implementation, 

-                                         VCGen.Outcome verificationOutcome, 

-                                         List<Counterexample!>? errors) {

-         string! implName = implementation.ToString();

-         houdiniOutcome.implementationOutcomes.Remove(implName);

-         List<Counterexample!> nonCandidateErrors = new List<Counterexample!>();

-         

-         switch (verificationOutcome) {

-           case VCGen.Outcome.Errors: 

-             assume (errors!=null);

-             foreach (Counterexample! error in errors) {

-               if (ExtractRefutedAnnotation(error)==null)

-                 nonCandidateErrors.Add(error);

-             }

-             break;

-           case VCGen.Outcome.TimedOut:

-           case VCGen.Outcome.Correct: 

-           case VCGen.Outcome.Inconclusive:

-           default:

-			 break;

-         }

-         houdiniOutcome.implementationOutcomes.Add(implName,

-						new VCGenOutcome(verificationOutcome, nonCandidateErrors));

-  

-       }

-

-       private void FlushWorkList(HoudiniState! current) {

-            this.NotifyFlushStart();

-            Axiom axiom = BuildAxiom(current.Assignment);

-            while (current.WorkList.Count>0) {

-              this.NotifyIteration();

-              

-              current.Implementation= current.WorkList.Peek();

-              this.NotifyImplementation(current.Implementation);

-              

-              List<Counterexample!>? errors;

-              VCGen.Outcome outcome = VerifyUsingAxiom(current.Implementation,axiom,out errors);

-              UpdateHoudiniOutcome(current.Outcome,current.Implementation,outcome,errors);

-              this.NotifyOutcome(outcome);

-              

-              current.WorkList.Dequeue();

-              this.NotifyDequeue();

-              

-           }

-           this.NotifyFlushFinish();

-       }

-

-       private void UpdateAssignment(HoudiniState! current, RefutedAnnotation! refAnnot){

-            current.Assignment.Remove(refAnnot.Constant);

-            current.Assignment.Add(refAnnot.Constant,false);

-            this.NotifyConstant(refAnnot.Constant);

-       }

-

-       private void AddToWorkList(HoudiniState! current, Implementation! imp) {

-         if (!current.WorkList.Contains(imp) && !current.isBlackListed(imp.Name)) {

-            current.WorkList.Enqueue(imp);

-            this.NotifyEnqueue(imp);

-         }

-       }

-

-       private void UpdateWorkList(HoudiniState! current, 

-                                   VCGen.Outcome outcome, 

-                                   List<Counterexample!>? errors) {

-       assume (current.Implementation!=null);

-       

-              switch (outcome) {

-                case VCGen.Outcome.Correct: 

-                  current.WorkList.Dequeue();

-                  this.NotifyDequeue();

-                  break;

-                case VCGen.Outcome.Errors: 

-                  assume (errors!=null);

-                  bool dequeue = false;

-                  foreach (Counterexample! error in errors) {

-                    RefutedAnnotation refutedAnnotation = ExtractRefutedAnnotation(error);

-                    if (refutedAnnotation!=null) {

-                      foreach (Implementation! implementation in FindImplementationsToEnqueue(refutedAnnotation,current.Implementation))

-                        { AddToWorkList(current, implementation); }

-                      UpdateAssignment(current, refutedAnnotation);

-                    } 

-                    else {

-                      dequeue = true; //once one non-houdini error is hit dequeue?!

-                    }

-                  }

-                  if (dequeue) {

-                    current.WorkList.Dequeue();

-                    this.NotifyDequeue();

-                  }

-                  break;

-                case VCGen.Outcome.TimedOut:

-                  // TODO: reset session instead of blocking timed out funcs?

-                  current.addToBlackList(current.Implementation.Name);

-                  current.WorkList.Dequeue();

-                  this.NotifyDequeue();

-                  break;

-                case VCGen.Outcome.OutOfMemory: 

-                case VCGen.Outcome.Inconclusive:

-                  current.WorkList.Dequeue();

-                  this.NotifyDequeue();

-                  break;

-                default:

-                  throw new Exception("Unknown vcgen outcome");

-              }   

-       }

-       

-       

-       private void AddRelatedToWorkList(HoudiniState! current, RefutedAnnotation! refutedAnnotation) {

-            assume (current.Implementation != null);

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

-                AddToWorkList(current, implementation);

-            }

-       }

-       

-       

-       // Updates the worklist and current assignment

-       // @return true if the current function is kept on the queue

-        private bool UpdateAssignmentWorkList(HoudiniState! current, 

-                                              VCGen.Outcome outcome, 

-                                              List<Counterexample!>? errors) {

-            assume (current.Implementation!=null);

-            bool dequeue = true;

-			

-            switch (outcome) {

-            case VCGen.Outcome.Correct: 

-                //yeah, dequeue

-                break;

-            case VCGen.Outcome.Errors: 

-                assume (errors!=null);

-                foreach (Counterexample! error in errors) {

-                    RefutedAnnotation refutedAnnotation = ExtractRefutedAnnotation(error);

-                    if (refutedAnnotation!=null) { // some candidate annotation removed

-                        AddRelatedToWorkList(current, refutedAnnotation);

-                        UpdateAssignment(current, refutedAnnotation);

-                        dequeue = false;

-                        } 

-                    }

-	            break;

-	            

-	        case VCGen.Outcome.TimedOut:

-	            // TODO: reset session instead of blocking timed out funcs?

-	            current.addToBlackList(current.Implementation.Name);

-                break;

-            case VCGen.Outcome.Inconclusive:

-            case VCGen.Outcome.OutOfMemory:

-                break;

-            default:

-                throw new Exception("Unknown vcgen outcome");

-            }

-            if (dequeue) {

-                current.WorkList.Dequeue();

-                this.NotifyDequeue();

-            }

-            return !dequeue;

-       }

-

-

-

-        private class HoudiniState {

-           private Queue<Implementation!>! _workList;

-           private Set<string!>! blackList;

-           private Dictionary<string!,bool>! _assignment;

-           private Implementation _implementation;

-           private HoudiniOutcome! _outcome;

-           

-           public HoudiniState(Queue<Implementation!>! workList, Dictionary<string!,bool>! currentAssignment) {

-             this._workList = workList;

-             this._assignment = currentAssignment;

-             this._implementation = null;

-             this._outcome = new HoudiniOutcome();

-             this.blackList = new Set<string!>();

-           }

-           

-           public Queue<Implementation!>! WorkList {

-             get { return this._workList; }

-           }

-           public Dictionary<string!,bool>! Assignment {

-             get { return this._assignment; }

-           }

-           public Implementation Implementation {

-             get { return this._implementation; }

-             set { this._implementation = value; }

-           }

-           public HoudiniOutcome! Outcome {

-             get { return this._outcome; }

-           }

-           public bool isBlackListed(string! funcName) {

-             return blackList.Contains(funcName);

-           }

-           public void addToBlackList(string! funcName) {

-             blackList.Add(funcName);

-           }

-        }

-

-        private void PrintBadList(string kind, List<string!>! list) {

-            if(list.Count != 0) {

-                Console.WriteLine("----------------------------------------");

-                Console.WriteLine("Functions: {0}", kind);

-                foreach(string! fname in list) {

-                    Console.WriteLine("\t{0}", fname);

-                }

-                Console.WriteLine("----------------------------------------");

-            }

-        }

-

-        private void PrintBadOutcomes(List<string!>! timeouts, List<string!>! inconc, List<string!>! errors) {

-            PrintBadList("TimedOut", timeouts);

-            PrintBadList("Inconclusive", inconc);

-            PrintBadList("Errors", errors);

-        }

-

-        public HoudiniOutcome! VerifyProgram (Program! program) {

-            HoudiniOutcome outcome;

-            switch (this.houdiniProver) {

-            case HoudiniProver.Z3:

-                outcome = VerifyProgramSameFuncFirst(program);

-                //outcome = PerformHoudiniInference(program);

-                break;

-            case HoudiniProver.Z3API: // not that stable

-                outcome = VerifyProgramUnorderedWork(program);

-                break;

-            default:

-                throw new Exception("Unknown HoudiniProver: " + this.houdiniProver.ToString());

-            }

-            PrintBadOutcomes(outcome.ListOfTimeouts, outcome.ListOfInconclusives, outcome.ListOfErrors);

-            return outcome;

-        }

-

-        // Old main loop

-        public HoudiniOutcome! VerifyProgramUnorderedWork (Program! program) {

-            HoudiniState current = new HoudiniState(BuildWorkList(program),BuildAssignment((!)houdiniConstants.Keys));

-            this.NotifyStart(program, houdiniConstants.Keys.Count);

-

-            while (current.WorkList.Count>0) {

-              System.GC.Collect();

-              this.NotifyIteration();

-            

-              Axiom axiom = BuildAxiom(current.Assignment);

-              this.NotifyAssignment(current.Assignment);

-              

-              current.Implementation= current.WorkList.Peek();

-              this.NotifyImplementation(current.Implementation);

-              

-              List<Counterexample!>? errors; 

-              VCGen.Outcome outcome = VerifyUsingAxiom(current.Implementation, axiom, out errors);

-              this.NotifyOutcome(outcome);

-              

-              UpdateHoudiniOutcome(current.Outcome,current.Implementation,outcome,errors);

-              if (IsOutcomeNotHoudini(outcome,errors) && !continueAtError) {

-                 current.WorkList.Dequeue();

-                 this.NotifyDequeue();

-                 FlushWorkList(current);

-              } else

-                 UpdateWorkList(current,outcome,errors);

-            }

-            this.NotifyEnd(true);

-            current.Outcome.assignment = current.Assignment;

-            return current.Outcome;

-        }

-		

-        // New main loop

-        public HoudiniOutcome! VerifyProgramSameFuncFirst (Program! program) {

-            HoudiniState current = new HoudiniState(BuildWorkList(program),BuildAssignment((!)houdiniConstants.Keys));

-            this.NotifyStart(program, houdiniConstants.Keys.Count);

-

-            while (current.WorkList.Count>0) {

-              bool exceptional = false;

-              System.GC.Collect();

-              this.NotifyIteration();

-            

-              current.Implementation = current.WorkList.Peek();

-              this.NotifyImplementation(current.Implementation);

-              

-              List<Counterexample!>? errors; 

-              VCGen.Outcome outcome = VerifyCurrent(current, program, out errors, out exceptional);

-              

-              // updates to worklist already done in VerifyCurrent, unless there was an exception

-              if (exceptional) {

-                    this.NotifyOutcome(outcome);

-                    UpdateHoudiniOutcome(current.Outcome, current.Implementation, outcome, errors);

-                    if (IsOutcomeNotHoudini(outcome,errors) && !continueAtError){ 

-                        current.WorkList.Dequeue();

-                        this.NotifyDequeue();

-                        FlushWorkList(current);

-                    } else { 

-                        UpdateAssignmentWorkList(current, outcome, errors);

-                    }

-                    exceptional = false;

-               }

-            }

-            this.NotifyEnd(true);

-            current.Outcome.assignment = current.Assignment;

-            return current.Outcome;

-        }

-

-		//Clean houdini (Based on "Houdini Spec in Boogie" email 10/22/08

-		//Aborts when there is a violation of non-candidate assertion

-		//This can be used in eager mode (continueAfterError) by simply making

-		//all non-candidate annotations as unchecked (free requires/ensures, assumes)

-        public HoudiniOutcome! PerformHoudiniInference(Program! program) {

-            HoudiniState current = new HoudiniState(BuildWorkList(program),BuildAssignment((!)houdiniConstants.Keys));

-            this.NotifyStart(program, houdiniConstants.Keys.Count);

-            

-            Console.WriteLine("Using the new houdini algorithm\n");

-

-            while (current.WorkList.Count > 0) {

-              bool exceptional = false;

-              System.GC.Collect();

-              this.NotifyIteration();

-            

-              current.Implementation = current.WorkList.Peek();

-              this.NotifyImplementation(current.Implementation);

-              

-              List<Counterexample!>? errors; 

-              VCGen.Outcome outcome = HoudiniVerifyCurrent(current, program, out errors, out exceptional);

-              

-              // updates to worklist already done in VerifyCurrent, unless there was an exception

-              if (exceptional) {

-                    this.NotifyOutcome(outcome);

-                    UpdateHoudiniOutcome(current.Outcome, current.Implementation, outcome, errors);

-                    if (AnyNonCandidateViolation(outcome, errors)) { //abort

-                        current.WorkList.Dequeue();

-                        this.NotifyDequeue();

-                        FlushWorkList(current);

-                    } else { //continue

-                        UpdateAssignmentWorkList(current, outcome, errors);

-                    }

-			   }

-            }

-            this.NotifyEnd(true);

-            current.Outcome.assignment = current.Assignment;

-            return current.Outcome;

-        }

-

-        

-        private List<Implementation!>! FindImplementationsToEnqueue(RefutedAnnotation! refutedAnnotation, Implementation! currentImplementation) {

-          List<Implementation!>! implementations = new List<Implementation!>();

-          switch (refutedAnnotation.Kind) {

-            case RefutedAnnotationKind.REQUIRES: 

-              foreach (Implementation! callee in callGraph.NextNodes(currentImplementation))  {

-                assume (callee.Proc!=null);

-                if (callee.Proc.Equals(refutedAnnotation.CalleeProc)) 

-                  implementations.Add(callee);

-              }

-            break;

-            case RefutedAnnotationKind.ENSURES: 

-               foreach (Implementation! caller in callGraph.PreviousNodes(currentImplementation))

-                  implementations.Add(caller);

-            break;

-            case RefutedAnnotationKind.ASSERT: //the implementation is already in queue

-            break;

-            default: 

-               throw new Exception("Unknown Refuted annotation kind:" + refutedAnnotation.Kind);

-            break;

-          }

-          return implementations;

-        }

-        

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

-        

-        private class RefutedAnnotation {

-          private string! _constant;

-          private RefutedAnnotationKind _kind;

-          private Procedure _callee;

-          

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

-            this._constant = constant;

-            this._kind = kind;

-            this._callee = callee;

-          }

-          public RefutedAnnotationKind Kind {

-            get { return this._kind; }

-          }

-          public string! Constant {

-            get { return this._constant; }

-          }

-          public Procedure CalleeProc {

-            get { return this._callee; }

-          }

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

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

-          }

-          public static RefutedAnnotation BuildRefutedEnsures(string! constant) {

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

-          }

-          public static RefutedAnnotation BuildRefutedAssert(string! constant) {

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

-          }

-

-        }

-        

-        private void PrintRefutedCall(CallCounterexample! err, XmlSink! xmlOut) {

-            Expr! cond = err.FailingRequires.Condition;

-            string houdiniConst;

-            if (MatchCandidate(cond, out houdiniConst)) {

-                xmlOut.WriteError("precondition violation", err.FailingCall.tok, err.FailingRequires.tok, err.Trace);

-            }

-        }

-        

-        private void PrintRefutedReturn(ReturnCounterexample! err, XmlSink! xmlOut) {

-            Expr! cond = err.FailingEnsures.Condition;

-            string houdiniConst;

-            if (MatchCandidate(cond, out houdiniConst)) {

-                xmlOut.WriteError("postcondition violation", err.FailingReturn.tok, err.FailingEnsures.tok, err.Trace);

-            }

-        }

-        

-        private void PrintRefutedAssert(AssertCounterexample! err, XmlSink! xmlOut) {

-            Expr cond = err.FailingAssert.OrigExpr;

-            string houdiniConst;

-            if (MatchCandidate(cond, out houdiniConst)) {

-                xmlOut.WriteError("postcondition violation", err.FailingAssert.tok, err.FailingAssert.tok, err.Trace);

-            }

-        }

-

-

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

-            XmlSink xmlRefuted = CommandLineOptions.Clo.XmlRefuted;

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

-               DateTime start = DateTime.Now;

-               xmlRefuted.WriteStartMethod(curFunc.ToString(), start);

-            

-               foreach (Counterexample! error in errors) {

-                  CallCounterexample ce = error as CallCounterexample;

-                  if (ce != null) PrintRefutedCall(ce, xmlRefuted);

-                  ReturnCounterexample re = error as ReturnCounterexample;

-                  if (re != null) PrintRefutedReturn(re, xmlRefuted);

-				  AssertCounterexample ae = error as AssertCounterexample;

-                  if (ae != null) PrintRefutedAssert(ae, xmlRefuted);

-               }

-               

-               DateTime end = DateTime.Now;

-               xmlRefuted.WriteEndMethod("errors", end, end.Subtract(start));

-            }

-        }

-        

-        private RefutedAnnotation ExtractRefutedAnnotation(Counterexample error) {

-          string houdiniConstant;

-          CallCounterexample callCounterexample = error as CallCounterexample;

-          if (callCounterexample!=null) {

-            Procedure! failingProcedure = (!)callCounterexample.FailingCall.Proc;

-            Requires! failingRequires  = (!)callCounterexample.FailingRequires;

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

-              assert (houdiniConstant!=null);

-              return RefutedAnnotation.BuildRefutedRequires(houdiniConstant, failingProcedure);

-            }

-          }

-          ReturnCounterexample returnCounterexample = error as ReturnCounterexample;

-          if (returnCounterexample!=null) {

-            Ensures failingEnsures  =returnCounterexample.FailingEnsures;

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

-              assert (houdiniConstant!=null);

-              return RefutedAnnotation.BuildRefutedEnsures(houdiniConstant);

-            }

-          }

-          AssertCounterexample assertCounterexample = error as AssertCounterexample;

-          if (assertCounterexample!=null) {

-            AssertCmd failingAssert  = assertCounterexample.FailingAssert;

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

-              assert (houdiniConstant!=null);

-              return RefutedAnnotation.BuildRefutedAssert(houdiniConstant);

-            }

-          }

-          

-          return null;

-        }

-        

-        private VCGen.Outcome TryCatchVerify(HdnVCGen! vcgen, out List<Counterexample!>? errors) {

-          VCGen.Outcome outcome;

-          try {

-            outcome = vcgen.Verify(out errors);

-          } catch (VCGenException e) {

-            assume(e!=null);

-            errors = null;

-            outcome = VCGen.Outcome.Inconclusive;

-          } catch (UnexpectedProverOutputException upo) {

-            assume(upo!=null);

-            errors = null;

-            outcome = VCGen.Outcome.Inconclusive;

-          }   

-          return outcome;     

-        }

-        

-        //version of TryCatchVerify that spins on the same function

-        //as long as the current assignment is changing

-        private VCGen.Outcome TrySpinSameFunc(HoudiniState! current,

-                                              Program! program,

-                                              HdnVCGen! vcgen, 

-                                              out List<Counterexample!>? errors,

-                                              out bool exceptional) {

-            assert (current.Implementation != null);

-            VCGen.Outcome outcome;

-            bool pushed = false;

-            errors = null;

-            outcome = VCGen.Outcome.Inconclusive;

-            try {

-                bool trySameFunc = true;

-                bool pastFirstIter = false; //see if this new loop is even helping

-								

-                do {

-                    if (pastFirstIter) {

-                        System.GC.Collect();

-                        this.NotifyIteration();

-                    }

-                    Axiom! currentAx = BuildAxiom(current.Assignment);

-                    this.NotifyAssignment(current.Assignment);

-

-                    vcgen.PushAxiom(currentAx);

-                    pushed = true;

-					outcome = vcgen.Verify(out errors);

-					vcgen.Pop();

-					pushed = false;

-					this.NotifyOutcome(outcome);

-

-                    DebugRefutedCandidates(current.Implementation, errors);

-                    UpdateHoudiniOutcome(current.Outcome, current.Implementation, outcome, errors);

-                    if (!continueAtError && IsOutcomeNotHoudini(outcome,errors)) {

-                        current.WorkList.Dequeue();

-                        this.NotifyDequeue();

-                        trySameFunc = false;

-                        FlushWorkList(current);

-                    } else {

-                        trySameFunc = UpdateAssignmentWorkList(current, outcome, errors);

-                        //reset for the next round

-                        errors = null;

-                        outcome = VCGen.Outcome.Inconclusive;

-                    }

-                    pastFirstIter = true;

-                } while (trySameFunc && current.WorkList.Count > 0);

-				

-            } catch (VCGenException e) {

-                assume(e!=null);

-                if (pushed){

-                    vcgen.Pop(); // what if session is dead?

-                }

-                NotifyException("VCGen");

-                exceptional = true;

-                return outcome;

-            } catch (UnexpectedProverOutputException upo) {

-                assume(upo!=null);

-                if (pushed){

-                    vcgen.Pop();

-                }

-                NotifyException("UnexpectedProverOutput");

-                exceptional = true;

-                return outcome;

-            } 

-            exceptional = false;

-            return outcome;

-        }

-    

-

-

-		//Similar to TrySpinSameFunc except no Candidate logic

-        private VCGen.Outcome HoudiniVerifyCurrentAux(HoudiniState! current,

-                                              Program! program,

-                                              HdnVCGen! vcgen, 

-                                              out List<Counterexample!>? errors,

-                                              out bool exceptional) {

-            assert (current.Implementation != null);

-            VCGen.Outcome outcome;

-            bool pushed = false;

-            errors = null;

-            outcome = VCGen.Outcome.Inconclusive;

-            try {

-                bool trySameFunc = true;

-                bool pastFirstIter = false; //see if this new loop is even helping

-								

-                do {

-                    if (pastFirstIter) {

-                        System.GC.Collect();

-                        this.NotifyIteration();

-                    }

-                    

-                    Axiom! currentAx = BuildAxiom(current.Assignment);

-                    this.NotifyAssignment(current.Assignment);

-

-					//check the VC with the current assignment

-                    vcgen.PushAxiom(currentAx);

-                    pushed = true;

-					outcome = vcgen.Verify(out errors);

-					vcgen.Pop();

-					pushed = false;

-					this.NotifyOutcome(outcome);

-

-                    DebugRefutedCandidates(current.Implementation, errors);

-                    UpdateHoudiniOutcome(current.Outcome, current.Implementation, outcome, errors);

-                    

-                    if (AnyNonCandidateViolation(outcome, errors)) { //abort

-                        current.WorkList.Dequeue();

-                        this.NotifyDequeue();

-                        trySameFunc = false;

-                        FlushWorkList(current);

-                    } else { //continue

-                        trySameFunc = UpdateAssignmentWorkList(current, outcome, errors);

-                        //reset for the next round

-                        errors = null;

-                        outcome = VCGen.Outcome.Inconclusive;

-                    }

-                    pastFirstIter = true;

-                } while (trySameFunc && current.WorkList.Count > 0);

-				

-            } catch (VCGenException e) {

-                assume(e!=null);

-                if (pushed){

-                    vcgen.Pop(); // what if session is dead?

-                }

-                NotifyException("VCGen");

-                exceptional = true;

-                return outcome;

-            } catch (UnexpectedProverOutputException upo) {

-                assume(upo!=null);

-                if (pushed){

-                    vcgen.Pop();

-                }

-                NotifyException("UnexpectedProverOutput");

-                exceptional = true;

-                return outcome;

-            } 

-            exceptional = false;

-            return outcome;

-        }

-    }

-

-  public enum HoudiniOutcomeKind { Done, FatalError, VerificationCompleted }

-

-  public class VCGenOutcome {

-    public VCGen.Outcome outcome;

-    public List<Counterexample!> errors;

-    public VCGenOutcome(VCGen.Outcome outcome, List<Counterexample!> errors) {

-      this.outcome = outcome;

-      this.errors = errors;

-    }

-  }

-

-  public class HoudiniOutcome {

-    // final assignment

-    public Dictionary<string!,bool>! assignment = new Dictionary<string!,bool>();

-    // boogie errors

-    public Dictionary<string!,VCGenOutcome!>! implementationOutcomes = new Dictionary<string!,VCGenOutcome!>();

-    // outcome kind    

-    public HoudiniOutcomeKind kind;

-    

-    // statistics 

-    

-    private int CountResults(VCGen.Outcome outcome) {

-        int outcomeCount=0;

-        foreach (VCGenOutcome! verifyOutcome in implementationOutcomes.Values) {

-          if (verifyOutcome.outcome==outcome)

-            outcomeCount++;

-        }

-        return outcomeCount;

-    }

-    

-    private List<string!>! ListOutcomeMatches(VCGen.Outcome outcome) {

-        List<string!>! result = new List<string!>();

-        foreach (KeyValuePair<string!, VCGenOutcome!> kvpair in implementationOutcomes) {

-          if (kvpair.Value.outcome==outcome)

-            result.Add(kvpair.Key);

-        }

-        return result;

-    }

-    

-    public int ErrorCount {

-      get {

-        return CountResults(VCGen.Outcome.Errors);

-      }

-    }

-    public int Verified {

-      get {

-        return CountResults(VCGen.Outcome.Correct);

-      }

-    }

-    public int Inconclusives {

-      get {

-        return CountResults(VCGen.Outcome.Inconclusive);

-      }

-    }    

-    public int TimeOuts {

-      get {

-        return CountResults(VCGen.Outcome.TimedOut);

-      }

-    }

-    public List<string!>! ListOfTimeouts {

-      get {

-        return ListOutcomeMatches(VCGen.Outcome.TimedOut);

-      }

-    }

-    public List<string!>! ListOfInconclusives {

-      get {

-        return ListOutcomeMatches(VCGen.Outcome.Inconclusive);

-      }

-    }

-    public List<string!>! ListOfErrors {

-      get {

-        return ListOutcomeMatches(VCGen.Outcome.Errors);

-      }

-    }

-  }

-

-}

diff --git a/Source/Houdini/Houdini.sscproj b/Source/Houdini/Houdini.sscproj
deleted file mode 100644
index 3f68bb91..00000000
--- a/Source/Houdini/Houdini.sscproj
+++ /dev/null
@@ -1,118 +0,0 @@
-<?xml version="1.0" encoding="utf-8"?>

-<VisualStudioProject>

-  <XEN ProjectType="Local"

-     SchemaVersion="1.0"

-     Name="Houdini"

-     ProjectGuid="40454b39-4f61-48b2-bde3-e9271b24f469"

-    >

-    <Build>

-      <Settings ApplicationIcon=""

-         AssemblyName="Houdini"

-         OutputType="Library"

-         RootNamespace="Houdini"

-         StartupObject=""

-         StandardLibraryLocation=""

-         TargetPlatform="v2"

-         TargetPlatformLocation=""

-        >

-        <Config Name="Debug"

-           AllowUnsafeBlocks="False"

-           BaseAddress="285212672"

-           CheckForOverflowUnderflow="False"

-           ConfigurationOverrideFile=""

-           DefineConstants="DEBUG;TRACE"

-           DocumentationFile=""

-           DebugSymbols="True"

-           FileAlignment="4096"

-           IncrementalBuild="True"

-           Optimize="False"

-           OutputPath="bin\debug"

-           RegisterForComInterop="False"

-           RemoveIntegerChecks="false"

-           TreatWarningsAsErrors="False"

-           WarningLevel="4"

-           CheckContractAdmissibility="True"

-           CheckPurity="False"

-           />

-        <Config Name="Release"

-           AllowUnsafeBlocks="false"

-           BaseAddress="285212672"

-           CheckForOverflowUnderflow="false"

-           ConfigurationOverrideFile=""

-           DefineConstants="TRACE"

-           DocumentationFile=""

-           DebugSymbols="false"

-           FileAlignment="4096"

-           IncrementalBuild="false"

-           Optimize="true"

-           OutputPath="bin\release"

-           RegisterForComInterop="false"

-           RemoveIntegerChecks="false"

-           TreatWarningsAsErrors="false"

-           WarningLevel="4"

-           CheckContractAdmissibility="True"

-           CheckPurity="False"

-           />

-      </Settings>

-      <References>

-        <Reference Name="System"

-             AssemblyName="System"

-             Private="false"

-             />

-        <Reference Name="System.Data"

-             AssemblyName="System.Data"

-             Private="false"

-             />

-        <Reference Name="System.Xml"

-             AssemblyName="System.Xml"

-             Private="false"

-             />

-        <Reference Name="Core"

-             Project="{47BC34F1-A173-40BE-84C2-9332B4418387}"

-             Private="true"

-             />

-        <Reference Name="VCGeneration"

-             Project="{F65666DE-FB56-457C-8782-09BE243450FC}"

-             Private="true"

-             />

-        <Reference Name="Simplify"

-             Project="{F75666DE-FB56-457C-8782-09BE243450FC}"

-             Private="true"

-             />

-        <Reference Name="AIFramework"

-             Project="{24B55172-AD8B-47D1-8952-5A95CFDB9B31}"

-             Private="true"

-             />

-        <Reference Name="AbsInt"

-             Project="{11D06232-2039-4BCA-853B-C596E2A4EDB0}"

-             Private="true"

-             />

-        <Reference Name="System.Compiler.Framework"

-             AssemblyName="System.Compiler.Framework"

-             Private="false"

-             HintPath="../../Binaries/System.Compiler.Framework.dll"

-             />

-        <Reference Name="Z3"

-             Project="{F75666DE-CD56-457C-8782-09BE243450FC}"

-             Private="true"

-             />

-      </References>

-    </Build>

-    <Files>

-      <Include>

-        <File RelPath="Houdini.ssc"

-                 SubType="Code"

-                 BuildAction="Compile"

-                 />

-        <File BuildAction="Compile"

-                 SubType="Code"

-                 RelPath="Checker.ssc"

-                 />

-        <File BuildAction="Compile"

-                 SubType="Code"

-                 RelPath="..\version.ssc"

-                 />

-      </Include>

-    </Files>

-  </XEN>

-</VisualStudioProject>
\ No newline at end of file
diff --git a/Source/ModelViewer/BCTProvider.cs b/Source/ModelViewer/BCTProvider.cs
new file mode 100644
index 00000000..6574daff
--- /dev/null
+++ b/Source/ModelViewer/BCTProvider.cs
@@ -0,0 +1,203 @@
+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+

+namespace Microsoft.Boogie.ModelViewer.BCT {

+  public class Provider : ILanguageProvider {

+    public static Provider Instance = new Provider();

+    private Provider() { }

+

+    public bool IsMyModel(Model m) {

+      return m.TryGetFunc("Alloc") != null;

+    }

+

+    public ILanguageSpecificModel GetLanguageSpecificModel(Model m, ViewOptions opts) {

+      var dm = new BCTModel(m, opts);

+      foreach (var s in m.States) {

+        var sn = new StateNode(dm.states.Count, dm, s);

+        dm.states.Add(sn);

+      }

+      dm.FinishStates();

+      return dm;

+    }

+  }

+

+  class BCTModel : LanguageModel {

+    public readonly Model.Func f_heap_select;

+    public readonly Dictionary<Model.Element, Model.Element[]> ArrayLengths = new Dictionary<Model.Element, Model.Element[]>();

+    public readonly Dictionary<Model.Element, Model.FuncTuple> DatatypeValues = new Dictionary<Model.Element, Model.FuncTuple>();

+    Dictionary<Model.Element, string> typeName = new Dictionary<Model.Element, string>();

+    public List<StateNode> states = new List<StateNode>();

+

+    public BCTModel(Model m, ViewOptions opts)

+      : base(m, opts) {

+      f_heap_select = m.MkFunc("[3]", 3);

+    }

+

+    internal void FinishStates() {

+      GenerateSourceLocations(states);

+    }

+

+    public override IEnumerable<IState> States {

+      get { return states; }

+    }

+

+    public string GetUserVariableName(string name) {

+      if (name.StartsWith("$")) 

+        return null;

+      var hash = name.IndexOf('#');

+      if (0 < hash)

+        return name.Substring(0, hash);

+      return name;

+    }

+

+    public Model.Element Image(Model.Element elt, Model.Func f) {

+      var r = f.AppWithResult(elt);

+      if (r != null)

+        return r.Args[0];

+      return null;

+    }

+    /*

+    public IEnumerable<ElementNode> GetExpansion(StateNode state, Model.Element elt) {

+      List<ElementNode> result = new List<ElementNode>();

+

+      if (elt.Kind != Model.ElementKind.Uninterpreted)

+        return result;

+

+      // Perhaps elt is a known datatype value

+      Model.FuncTuple fnTuple;

+      if (DatatypeValues.TryGetValue(elt, out fnTuple)) {

+        // elt is a datatype value

+        int i = 0;

+        foreach (var arg in fnTuple.Args) {

+          var edgname = new EdgeName(this, i.ToString());

+          result.Add(new FieldNode(state, edgname, arg));

+          i++;

+        }

+        return result;

+      }

+

+      // Perhaps elt is a sequence

+      var seqLen = f_seq_length.AppWithArg(0, elt);

+      if (seqLen != null) {

+        // elt is a sequence

+        foreach (var tpl in f_seq_index.AppsWithArg(0, elt)) {

+          var edgname = new EdgeName(this, "[%0]", tpl.Args[1]);

+          result.Add(new FieldNode(state, edgname, Unbox(tpl.Result)));

+        }

+        return result;

+      }

+

+      // Perhaps elt is a set

+      foreach (var tpl in f_set_select.AppsWithArg(0, elt)) {

+        var setElement = tpl.Args[1];

+        var containment = tpl.Result;

+        var edgname = new EdgeName(this, "[%0]", Unbox(setElement));

+        result.Add(new FieldNode(state, edgname, containment));

+      }

+      if (result.Count != 0)

+        return result;  // elt is a set

+

+      // It seems elt is an object or array

+      Model.Element[] lengths;

+      if (ArrayLengths.TryGetValue(elt, out lengths)) {

+        int i = 0;

+        foreach (var len in lengths) {

+          var name = lengths.Length == 1 ? "Length" : "Length" + i;

+          var edgname = new EdgeName(this, name);

+          result.Add(new FieldNode(state, edgname, len));

+          i++;

+        }

+      }

+      var heap = state.State.TryGet("$Heap");

+      if (heap != null) {

+        foreach (var tpl in f_heap_select.AppsWithArgs(0, heap, 1, elt)) {

+          var field = new FieldName(tpl.Args[2], this);

+          if (field.NameFormat != "alloc") {

+            var edgname = new EdgeName(this, field.NameFormat, field.NameArgs);

+            result.Add(new FieldNode(state, edgname, Unbox(tpl.Result)));

+          }

+        }

+      }

+      return result;

+    }

+     */ 

+  }

+

+  class StateNode : NamedState {

+    internal readonly BCTModel dm;

+    internal readonly List<VariableNode> vars = new List<VariableNode>();

+    internal readonly int index;

+

+    public StateNode(int i, BCTModel parent, Model.CapturedState s)

+      : base(s, parent) {

+      dm = parent;

+      state = s;

+      index = i;

+

+      SetupVars();

+    }

+

+    void SetupVars() {

+      var names = Util.Empty<string>();

+

+      if (dm.states.Count > 0) {

+        var prev = dm.states.Last();

+        names = prev.vars.Map(v => v.realName);

+      }

+

+      names = names.Concat(state.Variables).Distinct();

+

+      var curVars = state.Variables.ToDictionary(x => x);

+      foreach (var v in names) {

+        if (dm.GetUserVariableName(v) != null) {

+          var val = state.TryGet(v);

+          var vn = new VariableNode(this, v, val);

+          vn.updatedHere = dm.states.Count > 0 && curVars.ContainsKey(v);

+          if (curVars.ContainsKey(v))

+            dm.RegisterLocalValue(vn.Name, val);

+          vars.Add(vn);

+        }

+      }

+

+      dm.Flush(Nodes);

+    }

+

+    public override IEnumerable<IDisplayNode> Nodes {

+      get {

+        return vars;

+      }

+    }

+  }

+

+  class ElementNode : DisplayNode {

+    protected StateNode stateNode;

+    protected Model.Element elt;

+    protected BCTModel vm { get { return stateNode.dm; } }

+

+    public ElementNode(StateNode st, EdgeName name, Model.Element elt)

+      : base(st.dm, name, elt) {

+      this.stateNode = st;

+      this.elt = elt;

+    }

+

+    public ElementNode(StateNode st, string name, Model.Element elt)

+      : this(st, new EdgeName(name), elt) { }

+

+    protected override void ComputeChildren() {

+      //children.AddRange(vm.GetExpansion(stateNode, elt));

+    }

+  }

+

+  class VariableNode : ElementNode {

+    public bool updatedHere;

+    public string realName;

+

+    public VariableNode(StateNode par, string realName, Model.Element elt)

+      : base(par, realName, elt) {

+      this.realName = realName;

+      name = new EdgeName(vm.GetUserVariableName(realName));

+    }

+  }

+}

diff --git a/Source/ModelViewer/ModelViewer.csproj b/Source/ModelViewer/ModelViewer.csproj
index 6262ae2f..3a25e5cc 100644
--- a/Source/ModelViewer/ModelViewer.csproj
+++ b/Source/ModelViewer/ModelViewer.csproj
@@ -113,6 +113,7 @@
   </ItemGroup>

   <ItemGroup>

     <Compile Include="BaseProvider.cs" />

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

     <Compile Include="DafnyProvider.cs" />

     <Compile Include="DataModel.cs" />

     <Compile Include="Main.cs">

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index ff106380..87ab590d 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -164,8 +164,8 @@ namespace VC {
       Contract.Invariant(implName2LazyInliningInfo == null || cce.NonNullDictionaryAndValues(implName2LazyInliningInfo));

     }

 

-    private Dictionary<string, LazyInliningInfo> implName2LazyInliningInfo;

-    private GlobalVariable errorVariable;

+    protected Dictionary<string, LazyInliningInfo> implName2LazyInliningInfo;

+    protected GlobalVariable errorVariable;

 

     public void GenerateVCsForLazyInlining(Program program) {

       Contract.Requires(program != null);