1 files changed, 39 insertions, 12 deletions
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index f0e6b384..d74497c0 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -805,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;
@@ -813,6 +851,7 @@ namespace Microsoft.Boogie {
       get;
     }
   }
+
   public class ProverInterfaceContracts : ProverInterface {
     public override ProverContext Context {
       get {
@@ -841,18 +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 Outcome CheckOutcomeCore(ErrorHandler handler);
-      public abstract void Push();
-      public virtual void SetTimeOut(int ms) { }
-  }
-
   public class ProverException : Exception {
     public ProverException(string s)
       : base(s) {