From 8e1c309880067303b9fa847184338db682dc78de Mon Sep 17 00:00:00 2001
From: MichalMoskal <unknown>
Date: Wed, 23 Feb 2011 03:54:29 +0000
Subject: Strip (= 0) and (!= 0) from patterns (we used to allow that with
 anyNeq thing in Simplify frontend)

---
 Source/Provers/SMTLib/SMTLibLineariser.cs | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

(limited to 'Source/Provers/SMTLib/SMTLibLineariser.cs')

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");
           }
-- 
cgit v1.2.3