1 files changed, 43 insertions, 14 deletions
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index 9b7b6e36..d74497c0 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -734,7 +734,7 @@ namespace Microsoft.Boogie {
       Undetermined
     }
     public class ErrorHandler {
-      public virtual void OnModel(IList<string>/*!>!*/ labels, ErrorModel errModel) {
+      public virtual void OnModel(IList<string> labels, ErrorModel errModel) {
         Contract.Requires(cce.NonNullElements(labels));
       }
 
@@ -743,7 +743,6 @@ namespace Microsoft.Boogie {
       }
 
       public virtual void OnProverWarning(string message)
-        //modifies Console.Out.*, Console.Error.*;
       {
         Contract.Requires(message != null);
         switch (CommandLineOptions.Clo.PrintProverWarnings) {
@@ -761,7 +760,6 @@ namespace Microsoft.Boogie {
         }
       }
 
-
       public virtual Absy Label2Absy(string label) {
         Contract.Requires(label != null);
         Contract.Ensures(Contract.Result<Absy>() != null);
@@ -772,6 +770,9 @@ namespace Microsoft.Boogie {
     public abstract void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler);
     [NoDefaultContract]
     public abstract Outcome CheckOutcome(ErrorHandler handler);
+    public virtual string[] CalculatePath(int controlFlowConstant) {
+      throw new System.NotImplementedException();
+    }
     public virtual void LogComment(string comment) {
       Contract.Requires(comment != null);
     }
@@ -804,6 +805,44 @@ namespace Microsoft.Boogie {
       throw new NotImplementedException();
     }
 
+    // (assert vc)
+    public virtual void Assert(VCExpr vc, bool polarity)
+    {
+        throw new NotImplementedException();
+    }
+
+    // (assert implicit-axioms)
+    public virtual void AssertAxioms()
+    {
+        throw new NotImplementedException();
+    }
+
+    // (check-sat)
+    public virtual void Check()
+    {
+        throw new NotImplementedException();
+    }
+
+    // (check-sat + get-unsat-core)
+    public virtual void CheckAssumptions(List<VCExpr> assumptions, out List<int> unsatCore)
+    {
+        throw new NotImplementedException();
+    }
+
+    public virtual Outcome CheckOutcomeCore(ErrorHandler handler)
+    {
+        throw new NotImplementedException();
+    }
+
+    // (push 1)
+    public virtual void Push()
+    {
+        throw new NotImplementedException();
+    }
+
+    // Set theorem prover timeout for the next "check-sat"
+    public virtual void SetTimeOut(int ms)
+    { }
 
     public abstract ProverContext Context {
       get;
@@ -812,6 +851,7 @@ namespace Microsoft.Boogie {
       get;
     }
   }
+
   public class ProverInterfaceContracts : ProverInterface {
     public override ProverContext Context {
       get {
@@ -840,17 +880,6 @@ namespace Microsoft.Boogie {
     }
   }
 
-  // Exposes an api in line with z3's api
-  public abstract class ApiProverInterface : ProverInterface
-  {
-      public abstract void Assert(VCExpr vc, bool polarity);
-      public abstract void AssertAxioms();
-      public abstract void Check();
-      public abstract void CheckAssumptions(List<VCExpr> assumptions, out List<int> unsatCore);
-      public abstract void Push();
-      public virtual void SetTimeOut(int ms) { }
-  }
-
   public class ProverException : Exception {
     public ProverException(string s)
       : base(s) {