diff options
author | MichalMoskal <unknown> | 2011-02-23 03:54:29 +0000 |
---|---|---|
committer | MichalMoskal <unknown> | 2011-02-23 03:54:29 +0000 |
commit | 8e1c309880067303b9fa847184338db682dc78de (patch) | |
tree | a1fb543a73d40da25a97c06a8c55b09bbf86583e /Source/Provers/SMTLib | |
parent | b6618257258966608b131756a2a0f8751a666bbe (diff) |
Strip (= 0) and (!= 0) from patterns (we used to allow that with anyNeq thing in Simplify frontend)
Diffstat (limited to 'Source/Provers/SMTLib')
-rw-r--r-- | Source/Provers/SMTLib/SMTLibLineariser.cs | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index 563dec8f..9f16eb5b 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -298,7 +298,15 @@ namespace Microsoft.Boogie.SMTLib foreach (VCExpr e in vcTrig.Exprs) {
Contract.Assert(e != null);
wr.Write(" ");
- Linearise(e, options);
+ var subPat = e;
+ var nary = e as VCExprNAry;
+ if (nary != null && (nary.Op == VCExpressionGenerator.NeqOp || nary.Op == VCExpressionGenerator.EqOp)) {
+ if (nary[0] is VCExprLiteral)
+ subPat = nary[1];
+ else if (nary[1] is VCExprLiteral)
+ subPat = nary[0];
+ }
+ Linearise(subPat, options);
}
wr.Write(")\n");
}
|