bug fixes in z3api

1 files changed, 6 insertions, 0 deletions

diff --git a/Source/VCGeneration/Context.cs b/Source/VCGeneration/Context.cs
index 66f1e9a1..40e454fb 100644
--- a/Source/VCGeneration/Context.cs
+++ b/Source/VCGeneration/Context.cs
@@ -29,6 +29,7 @@ namespace Microsoft.Boogie
     public virtual void AddAxiom(Axiom a, string attributes) {Contract.Requires(a != null); ProcessDeclaration(a); }

     public virtual void DeclareGlobalVariable(GlobalVariable v, string attributes) {Contract.Requires(v != null); ProcessDeclaration(v); }

     public abstract void AddAxiom(VCExpr vc);

+    public abstract string Lookup(VCExprVar var);

     public abstract VCExpressionGenerator ExprGen { get; }

     public abstract Boogie2VCExprTranslator BoogieExprTranslator { get; }

     public abstract VCGenerationOptions VCGenOptions { get; }

@@ -232,6 +233,11 @@ void ObjectInvariant()
       return res;

     }

 

+    public override string Lookup(VCExprVar var)

+    {

+        return exprTranslator.Lookup(var);

+    }

+

     public override VCExpressionGenerator ExprGen { get {Contract.Ensures(Contract.Result<VCExpressionGenerator>() != null);

 

      return gen;