added FindLeastToVerify to StratfiedVCGenBase as an abstract method

1 files changed, 4 insertions, 2 deletions

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index 89c82a91..563cbf40 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -310,7 +310,7 @@ namespace VC {
     }

   }

 

-  public class StratifiedVCGenBase : VCGen {

+  public abstract class StratifiedVCGenBase : VCGen {

     public readonly static string recordProcName = "boogie_si_record";

     public Dictionary<string, StratifiedInliningInfo> implName2StratifiedInliningInfo;

     public ProverInterface prover;

@@ -468,6 +468,8 @@ namespace VC {
       if (lp == null) return false;

       return true;

     }

+

+    public abstract Outcome FindLeastToVerify(Implementation impl, ref HashSet<string> allBoolVars);

   }

 

   public class StratifiedVCGen : StratifiedVCGenBase {

@@ -1102,7 +1104,7 @@ namespace VC {
       }

     }

 

-    public Outcome FindLeastToVerify(Implementation impl, ref HashSet<string> allBoolVars) {

+    public override Outcome FindLeastToVerify(Implementation impl, ref HashSet<string> allBoolVars) {

       Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

 

       // Record current time