Fixedpoint VC catch up with recent changes

1 files changed, 7 insertions, 0 deletions

diff --git a/Source/VCGeneration/Context.cs b/Source/VCGeneration/Context.cs
index 7931a042..83787dc5 100644
--- a/Source/VCGeneration/Context.cs
+++ b/Source/VCGeneration/Context.cs
@@ -35,6 +35,7 @@ namespace Microsoft.Boogie
     public abstract VCGenerationOptions VCGenOptions { get; }

     public abstract object Clone();

     public abstract void Reset();

+    public abstract void Clear();

   }

   

 [ContractClassFor(typeof(ProverContext))]

@@ -128,6 +129,12 @@ public abstract class ProverContextContracts:ProverContext{
       axiomConjuncts = new List<VCExpr>();

     }

 

+    public override void Clear()

+    {

+        distincts = new List<Variable>();

+        axiomConjuncts = new List<VCExpr>();

+    }

+

     protected DeclFreeProverContext(DeclFreeProverContext ctxt) {

       Contract.Requires(ctxt != null);

       this.gen = ctxt.gen;