From 9deb757902b312fd17b5d7da2d93945077e5763c Mon Sep 17 00:00:00 2001
From: MichalMoskal <unknown>
Date: Wed, 23 Feb 2011 01:39:05 +0000
Subject: Do typed->untyped translation for -mv variables

---
 Source/Provers/SMTLib/ProverInterface.cs | 16 +++++++++-------
 1 file changed, 9 insertions(+), 7 deletions(-)

(limited to 'Source/Provers/SMTLib/ProverInterface.cs')

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index ee9e5df2..3b48bbbe 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -72,7 +72,7 @@ namespace Microsoft.Boogie.SMTLib
 
       AxBuilder = axBuilder;
       Namer = new SMTLibNamer();
-      ctx.Namer = Namer;
+      ctx.parent = this;
       this.DeclCollector = new TypeDeclCollector((SMTLibProverOptions)options, Namer);
 
       if (this.options.UseZ3) {
@@ -92,8 +92,8 @@ namespace Microsoft.Boogie.SMTLib
       }
     }
 
-    readonly TypeAxiomBuilder AxBuilder;
-    readonly UniqueNamer Namer;
+    internal readonly TypeAxiomBuilder AxBuilder;
+    internal readonly UniqueNamer Namer;
     readonly TypeDeclCollector DeclCollector;
     readonly SMTLibProcess Process;
     readonly List<string> proverErrors = new List<string>();
@@ -567,7 +567,7 @@ namespace Microsoft.Boogie.SMTLib
 
   public class SMTLibProverContext : DeclFreeProverContext
   {
-    internal UniqueNamer Namer;
+    internal SMTLibProcessTheoremProver parent;
 
     public SMTLibProverContext(VCExpressionGenerator gen,
                                VCGenerationOptions genOptions)
@@ -578,8 +578,6 @@ namespace Microsoft.Boogie.SMTLib
     protected SMTLibProverContext(SMTLibProverContext par)
       : base(par)
     {
-      if (par.Namer != null)
-        this.Namer = (UniqueNamer)par.Namer; // .Clone();
     }
 
     public override object Clone()
@@ -589,7 +587,11 @@ namespace Microsoft.Boogie.SMTLib
 
     public override string Lookup(VCExprVar var)
     {
-      return Namer.Lookup(var);
+      VCExprVar v = parent.AxBuilder.TryTyped2Untyped(var);
+      if (v != null) {
+        var = v;
+      }
+      return parent.Namer.Lookup(var);
     }
   }
 
-- 
cgit v1.2.3