summaryrefslogtreecommitdiff
path: root/Source/Provers/Z3api/ProverLayer.cs
diff options
context:
space:
mode:
authorGravatar MichalMoskal <unknown>2010-12-10 01:35:46 +0000
committerGravatar MichalMoskal <unknown>2010-12-10 01:35:46 +0000
commitd67cdef612efcfc6fbd27f14db712357b24552ba (patch)
tree9563ff2042c900e444ea3cb8479f3e1b86df0a80 /Source/Provers/Z3api/ProverLayer.cs
parent46f541d6063ca72008e009a7af5517aca5cf3789 (diff)
Don't crash in Context.Lookup when the namer has never seen the name. This happens when the name is never used in the VC (e.g. it gets peep-hole optimized).
Diffstat (limited to 'Source/Provers/Z3api/ProverLayer.cs')
-rw-r--r--Source/Provers/Z3api/ProverLayer.cs2
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/Provers/Z3api/ProverLayer.cs b/Source/Provers/Z3api/ProverLayer.cs
index 2f2f03ce..3d58652a 100644
--- a/Source/Provers/Z3api/ProverLayer.cs
+++ b/Source/Provers/Z3api/ProverLayer.cs
@@ -259,7 +259,7 @@ namespace Microsoft.Boogie.Z3
public override string Lookup(VCExprVar var)
{
- return cm.Namer.Lookup(var);
+ return cm.Namer.GetLocalName(var, var.Name);
}
}
}