diff options
| author |  MichalMoskal <unknown> | 2011-02-18 01:02:33 +0000 |
|---|---|---|
| committer | MichalMoskal <unknown> | 2011-02-18 01:02:33 +0000 |
| commit | 47c9277bbc5d96e0a12b50186de9a55671784661 (patch) | |
| tree | e25dee202317ba97751f67075e5260b9c3863445 | |
| parent | 1df6082c95bc87167c28d1ec7ada4ad0db1edd4e (diff) | |
Remove workaround for Z3 scanner problems (fixed now); fix one comment
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibLineariser.cs | 3 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibNamer.cs | 7 |
2 files changed, 4 insertions, 6 deletions
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index a8297583..f7a682ad 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -159,10 +159,9 @@ namespace Microsoft.Boogie.SMTLib else if (node == VCExpressionGenerator.False)
wr.Write("false");
else if (node is VCExprIntLit) {
- // some SMT-solvers do not understand negative literals
- // (e.g., yices)
BigNum lit = ((VCExprIntLit)node).Val;
if (lit.IsNegative)
+ // In SMT2 "-42" is an identifier (SMT2, Sect. 3.2 "Symbols")
wr.Write("(- 0 {0})", lit.Abs);
else
wr.Write(lit);
diff --git a/Source/Provers/SMTLib/SMTLibNamer.cs b/Source/Provers/SMTLib/SMTLibNamer.cs index 8a40bd84..600d6e51 100644 --- a/Source/Provers/SMTLib/SMTLibNamer.cs +++ b/Source/Provers/SMTLib/SMTLibNamer.cs @@ -8,9 +8,8 @@ namespace Microsoft.Boogie.SMTLib {
public class SMTLibNamer : UniqueNamer
{
- // The following Boogie ID characters are not SMT ID characters: `'\#
- // Accomodate Z3 SMT2 lexer bug - it doesn't like @ and such in identifiers
- const string idCharacters = "_"; // "~!@$%^&*_-+=<>.?/";
+ // The following Boogie ID characters are not SMT ID characters: `'\#
+ const string idCharacters = "~!@$%^&*_-+=<>.?/";
static string[] reservedSmtWordsList =
@@ -118,7 +117,7 @@ namespace Microsoft.Boogie.SMTLib public SMTLibNamer()
{
- this.Spacer = "__";
+ this.Spacer = "@@";
InitSymbolLists();
}
}
|