summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
authorGravatar Dan Liew <daniel.liew@imperial.ac.uk>2015-04-26 12:57:16 +0100
committerGravatar Dan Liew <daniel.liew@imperial.ac.uk>2015-04-26 12:59:56 +0100
commitbed8d4a027c635a146911a2ce973046f02a8e719 (patch)
tree7a9727ea29cbcfebe8786db31ee499e0620e044d /Source
parent9af64efeb4a057f853bb08cfc0fa8cbdc4a166b2 (diff)
Try to fix the emission of invalid SMT-LIBv2 queries when Boogie has a
variable that begins with a ``.``. This was't an issue for Z3 which ignores this but CVC4 is stricter and will emit an error
Diffstat (limited to 'Source')
-rw-r--r--Source/Provers/SMTLib/SMTLibNamer.cs15
1 files changed, 10 insertions, 5 deletions
diff --git a/Source/Provers/SMTLib/SMTLibNamer.cs b/Source/Provers/SMTLib/SMTLibNamer.cs
index 3ef2039b..40007ab9 100644
--- a/Source/Provers/SMTLib/SMTLibNamer.cs
+++ b/Source/Provers/SMTLib/SMTLibNamer.cs
@@ -98,9 +98,14 @@ namespace Microsoft.Boogie.SMTLib
return "|" + s + "|";
}
- static string NonKeyword(string s)
+ static string FilterReserved(string s)
{
- if (reservedSmtWords.Contains(s) || char.IsDigit(s[0]))
+ // Note symbols starting with ``.`` and ``@`` are reserved for internal
+ // solver use in SMT-LIBv2 however if we check for the first character
+ // being ``@`` then Boogie's tests fail spectacularly because they are
+ // used for labels so we don't check for it here. It hopefully won't matter
+ // in practice because ``@`` cannot be legally used in Boogie identifiers.
+ if (reservedSmtWords.Contains(s) || char.IsDigit(s[0]) || s[0] == '.')
s = "q@" + s;
// | and \ are illegal even in quoted identifiers
@@ -120,17 +125,17 @@ namespace Microsoft.Boogie.SMTLib
public static string QuoteId(string s)
{
- return AddQuotes(NonKeyword(s));
+ return AddQuotes(FilterReserved(s));
}
public override string GetQuotedLocalName(object thingie, string inherentName)
{
- return AddQuotes(base.GetLocalName(thingie, NonKeyword(inherentName)));
+ return AddQuotes(base.GetLocalName(thingie, FilterReserved(inherentName)));
}
public override string GetQuotedName(object thingie, string inherentName)
{
- return AddQuotes(base.GetName(thingie, NonKeyword(inherentName)));
+ return AddQuotes(base.GetName(thingie, FilterReserved(inherentName)));
}
public SMTLibNamer()