summaryrefslogtreecommitdiff
path: root/Source/Provers
diff options
context:
space:
mode:
authorGravatar MichalMoskal <unknown>2010-12-10 03:00:48 +0000
committerGravatar MichalMoskal <unknown>2010-12-10 03:00:48 +0000
commitfb350c313ff20b5a6de330e23d2c4577907070d7 (patch)
treec8f17e6c5a04b8b8a607127a15d5af88897ba168 /Source/Provers
parentd67cdef612efcfc6fbd27f14db712357b24552ba (diff)
Use a made-up name when Context.Lookup() cannot find a name
Diffstat (limited to 'Source/Provers')
-rw-r--r--Source/Provers/Simplify/ProverInterface.cs2
-rw-r--r--Source/Provers/Z3/ProverInterface.cs2
-rw-r--r--Source/Provers/Z3api/ProverLayer.cs2
3 files changed, 3 insertions, 3 deletions
diff --git a/Source/Provers/Simplify/ProverInterface.cs b/Source/Provers/Simplify/ProverInterface.cs
index 13e381c5..d747d3fd 100644
--- a/Source/Provers/Simplify/ProverInterface.cs
+++ b/Source/Provers/Simplify/ProverInterface.cs
@@ -761,7 +761,7 @@ namespace Microsoft.Boogie.Simplify {
if (v != null) {
var = v;
}
- return Namer.GetLocalName(var, var.Name);
+ return Namer.Lookup(var);
}
public override string translate(VCExpr expr, int polarity) {
diff --git a/Source/Provers/Z3/ProverInterface.cs b/Source/Provers/Z3/ProverInterface.cs
index 41d2338d..af9668d4 100644
--- a/Source/Provers/Z3/ProverInterface.cs
+++ b/Source/Provers/Z3/ProverInterface.cs
@@ -299,7 +299,7 @@ REVERSE_IMPLIES=<bool> Encode P==>Q as Q||!P.
if (v != null) {
var = v;
}
- return Namer.GetLocalName(var, var.Name);
+ return Namer.Lookup(var);
}
public override string translate(VCExpr expr, int polarity) {
diff --git a/Source/Provers/Z3api/ProverLayer.cs b/Source/Provers/Z3api/ProverLayer.cs
index 3d58652a..2f2f03ce 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.GetLocalName(var, var.Name);
+ return cm.Namer.Lookup(var);
}
}
}