diff options
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibNamer.cs | 15 | ||||
| -rw-r--r-- | Test/prover/usedot.bpl | 9 |
2 files changed, 19 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()
diff --git a/Test/prover/usedot.bpl b/Test/prover/usedot.bpl new file mode 100644 index 00000000..5815236e --- /dev/null +++ b/Test/prover/usedot.bpl @@ -0,0 +1,9 @@ +// RUN: %boogie -typeEncoding:m -proverLog:"%t.smt2" "%s" +// RUN: %OutputCheck "%s" --file-to-check="%t.smt2" +procedure foo() { + // . is an illegal starting character in SMT-LIBv2 + // so test that we don't emit it as a symbol name. + // CHECK-L:(declare-fun q@.x () Int) + var .x:int; + assert .x == 0; +} |