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 /Source/Provers/SMTLib/SMTLibLineariser.cs | |
| parent | 1df6082c95bc87167c28d1ec7ada4ad0db1edd4e (diff) | |
Remove workaround for Z3 scanner problems (fixed now); fix one comment
Diffstat (limited to 'Source/Provers/SMTLib/SMTLibLineariser.cs')
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibLineariser.cs | 3 |
1 files changed, 1 insertions, 2 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);
|