Fixes for duality under corral

1 files changed, 7 insertions, 0 deletions

diff --git a/Source/VCGeneration/Context.cs b/Source/VCGeneration/Context.cs
index bf27144b..484ce226 100644
--- a/Source/VCGeneration/Context.cs
+++ b/Source/VCGeneration/Context.cs
@@ -34,6 +34,7 @@ namespace Microsoft.Boogie
     public abstract Boogie2VCExprTranslator BoogieExprTranslator { get; }

     public abstract VCGenerationOptions VCGenOptions { get; }

     public abstract object Clone();

+    public abstract void Clear();

   }

   

 [ContractClassFor(typeof(ProverContext))]

@@ -114,6 +115,12 @@ public abstract class ProverContextContracts:ProverContext{
       exprTranslator = null;

     }

 

+    public override void Clear()

+    {

+        distincts = new List<Variable>();

+        axiomConjuncts = new List<VCExpr>();

+    }

+

     protected DeclFreeProverContext(DeclFreeProverContext ctxt) {

       Contract.Requires(ctxt != null);

       this.gen = ctxt.gen;