various changes for using unsat cores in Houdini

7 files changed, 225 insertions, 108 deletions

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

     private ProverInterface.ErrorHandler handler;

     ConditionGeneration.CounterexampleCollector collector;

+    HashSet<Variable> unsatCoreSet;

 

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

+    public bool InUnsatCore(Variable constant) {

+      if (unsatCoreSet == null)

+        return true;

+      return unsatCoreSet.Contains(constant);

+    }

+

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

       descriptiveName = impl.Name;

       collector = new ConditionGeneration.CounterexampleCollector();

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

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

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

 

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

+      var exprGen = proverInterface.Context.ExprGen;

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

       

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

-

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

       if (!CommandLineOptions.Clo.UseLabels) {

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

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

         conjecture = exprGen.Implies(eqExpr, conjecture);

       }

 

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

+      proverInterface.DefineMacro(macro, conjecture);

+      conjecture = exprGen.Function(macro);

+

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

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

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

       }

       else {

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

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

       }

     }

 

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

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

+      ProverContext proverContext = proverInterface.Context;

+      Boogie2VCExprTranslator exprTranslator = proverContext.BoogieExprTranslator;

+      VCExpressionGenerator exprGen = proverInterface.VCExprGen;

+

+      VCExpr expr = VCExpressionGenerator.True;

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

+        Variable constant = kv.Key;

+        VCExprVar exprVar = exprTranslator.LookupVariable(constant);

+        if (kv.Value) {

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

+        }

+        else {

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

+        }

+      }

+      return expr;

+    }

+

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

       collector.examples.Clear();

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

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

 

       if (CommandLineOptions.Clo.Trace) {

         Console.WriteLine("Verifying " + descriptiveName);

       }

       DateTime now = DateTime.UtcNow;

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

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

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

+

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

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

+

+#if UNSAT_CORE

+      Boogie2VCExprTranslator exprTranslator = proverInterface.Context.BoogieExprTranslator;

+      proverInterface.Push();

+      proverInterface.Assert(conjecture, false);

+      foreach (var v in assignment.Keys) {

+        if (assignment[v]) continue;

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

+      }

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

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

+      foreach (var v in assignment.Keys) {

+        if (!assignment[v]) continue;

+        assumptionVars.Add(v);

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

+      }

+      List<int> unsatCore;

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

+      unsatCoreSet = new HashSet<Variable>();

+      foreach (int i in unsatCore)

+        unsatCoreSet.Add(assumptionVars[i]);

+      proverInterface.Pop();

+#endif

+

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

       proverTime += queryTime;

       numProverQueries++;

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

     public virtual void UpdateIteration() { }

     public virtual void UpdateImplementation(Implementation implementation) { }

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

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

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

     public virtual void UpdateEnqueue(Implementation implementation) { }

     public virtual void UpdateDequeue() { }

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

       wr.Flush();

     }

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

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

       bool firstTime = true;

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

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

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

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

         string valString; // ugliness to get it lower cased

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

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

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

     }

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

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

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

     }

     protected void NotifyOutcome(ProverInterface.Outcome outcome) {

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

   }

 

+  public class Macro : Function {

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

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

+  }

+

   public class FreeRequiresVisitor : StandardVisitor {

     public override Requires VisitRequires(Requires requires) {

       if (requires.Free)

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

   public class Houdini : ObservableHoudini {

     private Program program;

-    private ReadOnlyDictionary<string, IdentifierExpr> houdiniConstants;

+    private HashSet<Variable> houdiniConstants;

     private ReadOnlyDictionary<Implementation, HoudiniSession> houdiniSessions;

     private VCGen vcgen;

-    private Checker checker;

+    private ProverInterface proverInterface;

     private Graph<Implementation> callGraph;

     private HashSet<Implementation> vcgenFailures;

 

+

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

+      Contract.Requires(prog != null);

+

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

+

+      if (logFilePath != null) {

+        options.LogFilename = logFilePath;

+        if (appendLogFile)

+          options.AppendLogFile = appendLogFile;

+      }

+

+      if (timeout > 0) {

+        options.TimeLimit = timeout * 1000;

+      }

+

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

+

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

+

+      // set up the context

+      foreach (Declaration decl in prog.TopLevelDeclarations) {

+        Contract.Assert(decl != null);

+        TypeCtorDecl t = decl as TypeCtorDecl;

+        if (t != null) {

+          ctx.DeclareType(t, null);

+        }

+      }

+      foreach (Declaration decl in prog.TopLevelDeclarations) {

+        Contract.Assert(decl != null);

+        Constant c = decl as Constant;

+        if (c != null) {

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

+        }

+        else {

+          Function f = decl as Function;

+          if (f != null) {

+            ctx.DeclareFunction(f, null);

+          }

+        }

+      }

+      foreach (Declaration decl in prog.TopLevelDeclarations) {

+        Contract.Assert(decl != null);

+        Axiom ax = decl as Axiom;

+        if (ax != null) {

+          ctx.AddAxiom(ax, null);

+        }

+      }

+      foreach (Declaration decl in prog.TopLevelDeclarations) {

+        Contract.Assert(decl != null);

+        GlobalVariable v = decl as GlobalVariable;

+        if (v != null) {

+          ctx.DeclareGlobalVariable(v, null);

+        }

+      }

+

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

+    }

+

     public Houdini(Program program) {

       this.program = program;

 

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

       

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

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

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

 

       vcgenFailures = new HashSet<Implementation>();

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

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

           if (CommandLineOptions.Clo.Trace)

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

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

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

           houdiniSessions.Add(impl, session);

         }

         catch (VCGenException) {

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

     }

 

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

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

+    private HashSet<Variable> CollectExistentialConstants() {

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

       foreach (Declaration decl in program.TopLevelDeclarations) {

         Constant constant = decl as Constant;

         if (constant != null) {

           bool result = false;

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

             if (result == true)

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

+              existentialConstants.Add(constant);

           }

         }

       }

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

+      return existentialConstants;

     }

 

     private Graph<Implementation> BuildCallGraph() {

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

     }

 

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

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

       candidateConstant = null;

       IExpr antecedent;

       IExpr expr = boogieExpr as IExpr;

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

         IdentifierExpr.ConstantFunApp constantFunApp = antecedent as IdentifierExpr.ConstantFunApp;

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

-          candidateConstant = constantFunApp.IdentifierExpr.Name;

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

+          candidateConstant = constantFunApp.IdentifierExpr.Decl;

           return true;

         }

       }

       return false;

     }

 

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

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

-      Boogie2VCExprTranslator exprTranslator = proverContext.BoogieExprTranslator;

-      VCExpressionGenerator exprGen = checker.VCExprGen;

-

-      VCExpr expr = VCExpressionGenerator.True;

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

-        IdentifierExpr constantExpr;

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

-        Contract.Assume(constantExpr != null);

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

-        if (kv.Value) {

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

-        }

-        else {

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

-        }

-      }

-      return expr;

-    }

-

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

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

-      foreach (string constant in constants)

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

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

+      foreach (var constant in constants)

         initial.Add(constant, true);

       return initial;

     }

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

     private void FlushWorkList(HoudiniState current) {

       this.NotifyFlushStart();

-      VCExpr axiom = BuildAxiom(current.Assignment);

       while (current.WorkQueue.Count > 0) {

         this.NotifyIteration();

 

@@ -557,7 +599,7 @@ namespace Microsoft.Boogie.Houdini {
         HoudiniSession session;

         houdiniSessions.TryGetValue(current.Implementation, out session);

         List<Counterexample> errors;

-        ProverInterface.Outcome outcome = TryCatchVerify(session, axiom, out errors);

+        ProverInterface.Outcome outcome = TryCatchVerify(session, current.Assignment, out errors);

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

         this.NotifyOutcome(outcome);

 

@@ -573,24 +615,19 @@ namespace Microsoft.Boogie.Houdini {
       }

       current.Assignment.Remove(refAnnot.Constant);

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

-      this.NotifyConstant(refAnnot.Constant);

-    }

-

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

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

-        current.WorkQueue.Enqueue(imp);

-        this.NotifyEnqueue(imp);

-      }

+      this.NotifyConstant(refAnnot.Constant.Name);

     }

 

     private void AddRelatedToWorkList(HoudiniState current, RefutedAnnotation refutedAnnotation) {

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

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

-        AddToWorkList(current, implementation);

+        if (!current.isBlackListed(implementation.Name)) {

+          current.WorkQueue.Enqueue(implementation);

+          this.NotifyEnqueue(implementation);

+        }

       }

     }

 

-

     // Updates the worklist and current assignment

     // @return true if the current function is dequeued

     private bool UpdateAssignmentWorkList(HoudiniState current,

@@ -654,11 +691,11 @@ namespace Microsoft.Boogie.Houdini {
     private class HoudiniState {

       private WorkQueue _workQueue;

       private HashSet<string> blackList;

-      private Dictionary<string, bool> _assignment;

+      private Dictionary<Variable, bool> _assignment;

       private Implementation _implementation;

       private HoudiniOutcome _outcome;

 

-      public HoudiniState(WorkQueue workQueue, Dictionary<string, bool> currentAssignment) {

+      public HoudiniState(WorkQueue workQueue, Dictionary<Variable, bool> currentAssignment) {

         this._workQueue = workQueue;

         this._assignment = currentAssignment;

         this._implementation = null;

@@ -669,7 +706,7 @@ namespace Microsoft.Boogie.Houdini {
       public WorkQueue WorkQueue {

         get { return this._workQueue; }

       }

-      public Dictionary<string, bool> Assignment {

+      public Dictionary<Variable, bool> Assignment {

         get { return this._assignment; }

       }

       public Implementation Implementation {

@@ -688,8 +725,8 @@ namespace Microsoft.Boogie.Houdini {
     }

 

     public HoudiniOutcome PerformHoudiniInference() {

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

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

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

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

       foreach (Implementation impl in vcgenFailures) {

         current.addToBlackList(impl.Name);

       }

@@ -705,23 +742,31 @@ namespace Microsoft.Boogie.Houdini {
         HoudiniVerifyCurrent(session, current);

       }

       this.NotifyEnd(true);

-      current.Outcome.assignment = current.Assignment;

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

+      foreach (var x in current.Assignment)

+        assignment[x.Key.Name] = x.Value;

+      current.Outcome.assignment = assignment;

       return current.Outcome;

     }

 

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

+      HoudiniSession session;

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

       switch (refutedAnnotation.Kind) {

         case RefutedAnnotationKind.REQUIRES:

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

+            houdiniSessions.TryGetValue(callee, out session);

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

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

+            if (callee.Proc.Equals(refutedAnnotation.CalleeProc) && session.InUnsatCore(refutedAnnotation.Constant)) 

               implementations.Add(callee);

           }

           break;

         case RefutedAnnotationKind.ENSURES:

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

-            implementations.Add(caller);

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

+            houdiniSessions.TryGetValue(caller, out session);

+            if (session.InUnsatCore(refutedAnnotation.Constant))

+              implementations.Add(caller);

+          }

           break;

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

           break;

@@ -734,11 +779,11 @@ namespace Microsoft.Boogie.Houdini {
     private enum RefutedAnnotationKind { REQUIRES, ENSURES, ASSERT };

 

     private class RefutedAnnotation {

-      private string _constant;

+      private Variable _constant;

       private RefutedAnnotationKind _kind;

       private Procedure _callee;

 

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

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

         this._constant = constant;

         this._kind = kind;

         this._callee = callee;

@@ -746,19 +791,19 @@ namespace Microsoft.Boogie.Houdini {
       public RefutedAnnotationKind Kind {

         get { return this._kind; }

       }

-      public string Constant {

+      public Variable Constant {

         get { return this._constant; }

       }

       public Procedure CalleeProc {

         get { return this._callee; }

       }

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

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

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

       }

-      public static RefutedAnnotation BuildRefutedEnsures(string constant) {

+      public static RefutedAnnotation BuildRefutedEnsures(Variable constant) {

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

       }

-      public static RefutedAnnotation BuildRefutedAssert(string constant) {

+      public static RefutedAnnotation BuildRefutedAssert(Variable constant) {

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

       }

 

@@ -766,7 +811,7 @@ namespace Microsoft.Boogie.Houdini {
 

     private void PrintRefutedCall(CallCounterexample err, XmlSink xmlOut) {

       Expr cond = err.FailingRequires.Condition;

-      string houdiniConst;

+      Variable houdiniConst;

       if (MatchCandidate(cond, out houdiniConst)) {

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

       }

@@ -774,7 +819,7 @@ namespace Microsoft.Boogie.Houdini {
 

     private void PrintRefutedReturn(ReturnCounterexample err, XmlSink xmlOut) {

       Expr cond = err.FailingEnsures.Condition;

-      string houdiniConst;

+      Variable houdiniConst;

       if (MatchCandidate(cond, out houdiniConst)) {

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

       }

@@ -782,7 +827,7 @@ namespace Microsoft.Boogie.Houdini {
 

     private void PrintRefutedAssert(AssertCounterexample err, XmlSink xmlOut) {

       Expr cond = err.FailingAssert.OrigExpr;

-      string houdiniConst;

+      Variable houdiniConst;

       if (MatchCandidate(cond, out houdiniConst)) {

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

       }

@@ -809,7 +854,7 @@ namespace Microsoft.Boogie.Houdini {
     }

 

     private RefutedAnnotation ExtractRefutedAnnotation(Counterexample error) {

-      string houdiniConstant;

+      Variable houdiniConstant;

       CallCounterexample callCounterexample = error as CallCounterexample;

       if (callCounterexample != null) {

         Procedure failingProcedure = callCounterexample.FailingCall.Proc;

@@ -839,10 +884,10 @@ namespace Microsoft.Boogie.Houdini {
       return null;

     }

 

-    private ProverInterface.Outcome TryCatchVerify(HoudiniSession session, VCExpr axiom, out List<Counterexample> errors) {

+    private ProverInterface.Outcome TryCatchVerify(HoudiniSession session, Dictionary<Variable, bool> assignment, out List<Counterexample> errors) {

       ProverInterface.Outcome outcome;

       try {

-        outcome = session.Verify(checker, axiom, out errors);

+        outcome = session.Verify(proverInterface, assignment, out errors);

       }

       catch (UnexpectedProverOutputException upo) {

         Contract.Assume(upo != null);

@@ -854,12 +899,11 @@ namespace Microsoft.Boogie.Houdini {
 

     private void HoudiniVerifyCurrent(HoudiniSession session, HoudiniState current) {

       while (true) {

-        VCExpr currentAx = BuildAxiom(current.Assignment);

         this.NotifyAssignment(current.Assignment);

 

         //check the VC with the current assignment

         List<Counterexample> errors;

-        ProverInterface.Outcome outcome = TryCatchVerify(session, currentAx, out errors);

+        ProverInterface.Outcome outcome = TryCatchVerify(session, current.Assignment, out errors);

         this.NotifyOutcome(outcome);

 

         DebugRefutedCandidates(current.Implementation, errors);

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 08322ebb..014af458 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -78,14 +78,14 @@ namespace Microsoft.Boogie.SMTLib
 

       SetupProcess();

 

-      if (CommandLineOptions.Clo.StratifiedInlining > 0)

+      if (CommandLineOptions.Clo.StratifiedInlining > 0 || CommandLineOptions.Clo.ContractInfer)

       {

           // Prepare for ApiChecker usage

           if (options.LogFilename != null && currentLogFile == null)

           {

               currentLogFile = OpenOutputFile("");

           }

-          if (CommandLineOptions.Clo.ProcedureCopyBound > 0)

+          if (CommandLineOptions.Clo.ProcedureCopyBound > 0 || CommandLineOptions.Clo.ContractInfer)

           {

               SendThisVC("(set-option :produce-unsat-cores true)");

               this.usingUnsatCore = true;

@@ -770,6 +770,14 @@ namespace Microsoft.Boogie.SMTLib
         SendThisVC(a);

     }

 

+    public override void DefineMacro(Function fun, VCExpr vc) {

+      DeclCollector.AddFunction(fun);

+      string name = Namer.GetName(fun, fun.Name);

+      string a = "(define-fun " + name + "() Bool " + VCExpr2String(vc, 1) + ")";

+      AssertAxioms();

+      SendThisVC(a);

+    }

+

     public override void AssertAxioms()

     {

         FlushAxioms();

@@ -805,7 +813,9 @@ namespace Microsoft.Boogie.SMTLib
             nameCounter++;

             nameToAssumption.Add(name, i);

 

-            SendThisVC(string.Format("(assert (! {0} :named {1}))", VCExpr2String(vc, 1), name));

+            string vcString = VCExpr2String(vc, 1);

+            AssertAxioms();

+            SendThisVC(string.Format("(assert (! {0} :named {1}))", vcString, name));

             i++;

         }

         Check();

diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs
index 05a6caf3..a4bdee51 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -164,6 +164,11 @@ void ObjectInvariant()
       return TypeToString(t);

     }

 

+    public void AddFunction(Function func) {

+      if (KnownFunctions.Contains(func))

+        return;

+      KnownFunctions.Add(func);

+    }

 

     public override bool Visit(VCExprNAry node, bool arg) {

       Contract.Requires(node != null);

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index f9999a74..9ebf4d63 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -851,9 +851,14 @@ namespace Microsoft.Boogie {
     public abstract ProverContext Context {

       get;

     }

+

     public abstract VCExpressionGenerator VCExprGen {

       get;

     }

+

+    public virtual void DefineMacro(Function fun, VCExpr vc) {

+      throw new NotImplementedException();

+    }

   }

 

   public class ProverInterfaceContracts : ProverInterface {

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index fa8a7f0d..ea17983f 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -210,7 +210,7 @@ namespace VC
             var bet = ctx.BoogieExprTranslator;

             VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : bet.LookupVariable(info.controlFlowVariable);

 

-            VCExpr vcexpr = gen.Not(GenerateVC(impl, controlFlowVariableExpr, out label2absy, checker));

+            VCExpr vcexpr = gen.Not(GenerateVC(impl, controlFlowVariableExpr, out label2absy, checker.TheoremProver.Context));

             Contract.Assert(vcexpr != null);

             if (!CommandLineOptions.Clo.UseLabels) {

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

@@ -1266,7 +1266,7 @@ namespace VC
             Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = PassifyImpl(impl, program, out mvInfo);

             var exprGen = checker.TheoremProver.Context.ExprGen;

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

-            vcMain = GenerateVC(impl, controlFlowVariableExpr, out mainLabel2absy, checker);

+            vcMain = GenerateVC(impl, controlFlowVariableExpr, out mainLabel2absy, checker.TheoremProver.Context);

             if (!CommandLineOptions.Clo.UseLabels) {

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

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

@@ -2519,7 +2519,7 @@ namespace VC
             var exprGen = checker.TheoremProver.Context.ExprGen;

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

 

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

+            vc = GenerateVC(impl, controlFlowVariableExpr, out label2absy, checker.TheoremProver.Context);

 

             if (!CommandLineOptions.Clo.UseLabels) {

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

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 008810cb..5761ca70 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -611,7 +611,7 @@ namespace VC {
         var exprGen = ch.TheoremProver.Context.ExprGen;

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

 

-        VCExpr vc = parent.GenerateVC(impl, controlFlowVariableExpr, out label2Absy, ch);

+        VCExpr vc = parent.GenerateVC(impl, controlFlowVariableExpr, out label2Absy, ch.TheoremProver.Context);

         Contract.Assert(vc != null);

 

         if (!CommandLineOptions.Clo.UseLabels) {

@@ -1550,7 +1550,7 @@ namespace VC {
         var exprGen = ctx.ExprGen;

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

 

-        VCExpr vc = parent.GenerateVCAux(impl, controlFlowVariableExpr, label2absy, checker);

+        VCExpr vc = parent.GenerateVCAux(impl, controlFlowVariableExpr, label2absy, checker.TheoremProver.Context);

         Contract.Assert(vc != null);

 

         if (!CommandLineOptions.Clo.UseLabels) {

@@ -1630,20 +1630,20 @@ namespace VC {
     }

     #endregion

 

-    public VCExpr GenerateVC(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, out Hashtable/*<int, Absy!>*//*!*/ label2absy, Checker/*!*/ ch)

+    public VCExpr GenerateVC(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, out Hashtable/*<int, Absy!>*//*!*/ label2absy, ProverContext proverContext)

     {

       Contract.Requires(impl != null);

-      Contract.Requires(ch != null);

+      Contract.Requires(proverContext != null);

       Contract.Ensures(Contract.ValueAtReturn(out label2absy) != null);

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

 

       label2absy = new Hashtable/*<int, Absy!>*/();

-      return GenerateVCAux(impl, controlFlowVariableExpr, label2absy, ch);

+      return GenerateVCAux(impl, controlFlowVariableExpr, label2absy, proverContext);

     }

 

-    protected VCExpr GenerateVCAux(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, Hashtable/*<int, Absy!>*//*!*/ label2absy, Checker/*!*/ ch) {

+    protected VCExpr GenerateVCAux(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, Hashtable/*<int, Absy!>*//*!*/ label2absy, ProverContext proverContext) {

       Contract.Requires(impl != null);

-      Contract.Requires(ch != null);

+      Contract.Requires(proverContext != null);

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

 

       TypecheckingContext tc = new TypecheckingContext(null);

@@ -1653,35 +1653,35 @@ namespace VC {
       int assertionCount;

       switch (CommandLineOptions.Clo.vcVariety) {

         case CommandLineOptions.VCVariety.Structured:

-          vc = VCViaStructuredProgram(impl, label2absy, ch.TheoremProver.Context, out assertionCount);

+          vc = VCViaStructuredProgram(impl, label2absy, proverContext, out assertionCount);

           break;

         case CommandLineOptions.VCVariety.Block:

-          vc = FlatBlockVC(impl, label2absy, false, false, false, ch.TheoremProver.Context, out assertionCount);

+          vc = FlatBlockVC(impl, label2absy, false, false, false, proverContext, out assertionCount);

           break;

         case CommandLineOptions.VCVariety.BlockReach:

-          vc = FlatBlockVC(impl, label2absy, false, true, false, ch.TheoremProver.Context, out assertionCount);

+          vc = FlatBlockVC(impl, label2absy, false, true, false, proverContext, out assertionCount);

           break;

         case CommandLineOptions.VCVariety.Local:

-          vc = FlatBlockVC(impl, label2absy, true, false, false, ch.TheoremProver.Context, out assertionCount);

+          vc = FlatBlockVC(impl, label2absy, true, false, false, proverContext, out assertionCount);

           break;

         case CommandLineOptions.VCVariety.BlockNested:

-          vc = NestedBlockVC(impl, label2absy, false, ch.TheoremProver.Context, out assertionCount);

+          vc = NestedBlockVC(impl, label2absy, false, proverContext, out assertionCount);

           break;

         case CommandLineOptions.VCVariety.BlockNestedReach:

-          vc = NestedBlockVC(impl, label2absy, true, ch.TheoremProver.Context, out assertionCount);

+          vc = NestedBlockVC(impl, label2absy, true, proverContext, out assertionCount);

           break;

         case CommandLineOptions.VCVariety.Dag:

           if (cce.NonNull(CommandLineOptions.Clo.TheProverFactory).SupportsDags) {

-            vc = DagVC(cce.NonNull(impl.Blocks[0]), controlFlowVariableExpr, label2absy, new Hashtable/*<Block, VCExpr!>*/(), ch.TheoremProver.Context, out assertionCount);

+            vc = DagVC(cce.NonNull(impl.Blocks[0]), controlFlowVariableExpr, label2absy, new Hashtable/*<Block, VCExpr!>*/(), proverContext, out assertionCount);

           } else {

-            vc = LetVC(cce.NonNull(impl.Blocks[0]), controlFlowVariableExpr, label2absy, ch.TheoremProver.Context, out assertionCount);

+            vc = LetVC(cce.NonNull(impl.Blocks[0]), controlFlowVariableExpr, label2absy, proverContext, out assertionCount);

           }

           break;

         case CommandLineOptions.VCVariety.DagIterative:

-          vc = LetVCIterative(impl.Blocks, controlFlowVariableExpr, label2absy, ch.TheoremProver.Context, out assertionCount);

+          vc = LetVCIterative(impl.Blocks, controlFlowVariableExpr, label2absy, proverContext, out assertionCount);

           break;

         case CommandLineOptions.VCVariety.Doomed:

-          vc = FlatBlockVC(impl, label2absy, false, false, true, ch.TheoremProver.Context, out assertionCount);

+          vc = FlatBlockVC(impl, label2absy, false, false, true, proverContext, out assertionCount);

           break;

         default:

           Contract.Assert(false);